GridSAT and SwitchGridSAT

Here we discuss classes of propositional satisfiability (SAT) that have a more realistic structure than the usual Random 3SAT, and that also have more parameters and a wider range of interesting behaviors.

Definitions

Motivations

planar grid with local interactions between sensors
axes that can be taken to correspond to "time vs. resources" and so correspond roughly with structure of scheduling problems (SNAP motivated)

Definition: grid(H,L,h,l;c)

Propositional variables are taken to correspond to the points on a H x L grid: v(x,y)
Each of the c clauses is randomly generated in such a way that neighboring variables in a clause are at most a grid distance (h,l) apart.

Example 1

The case H=h, L=l, gives no restrictions on the clauses and so corresponds to standard Random 3SAT.

Example 2

The case h=1, l=l, gives local clauses. This is also similar to the "crystallographic instances" used in Ginsberg's "Dynamic Backtracking" (and which motivated in part the gridSAT construction).

Definition: switchgrid(H,L,h,l;c;s )

Initial clauses are generated as for grid(H,L,h,l;c). However, we also introduce propositional switch variables s_i. Each clause is then activated by a randomly selected switch variable, e.g. giving a clause such as

s₂₃ -> ( v(1,3) or -v(1,5) or v(2,3) )

This allows us to define an optimization problem, namely, to find the largest set of switches such that the activated set of clauses still remains satisfiable.

In the limit of large s then each clause will have a different switch and the problem becomes that of MAXSAT

Phase Transitions (PTs)

For gridSAT the total number of variables is just HL, and so the usual clause/variable ratio is c/(HL). However, the shape of the grid also affects the phase transitions observed.

Coarse thresholds

Consider, long narrow grids (and with local clauses) such as with grid(10n,10,1,-1,c)

These problems seem to exhibit coarse thresholds, that is, even in the limit of large problems, the probability of a problem being satisfiable does not abruptly change from almost 0 to almost 1, but instead changes smoothly. A physical analogy it that of glass slowly softening as we increase temperature, in contrast to the sharp change of ice changing into water.

Coarse Thresholds and Predicting Locations of Computational Cliffs

Note that the coarseness of a PT refers to the average behavior over a large number of instances. It does not necessarily mean that the individual instances also exhibit a smooth behavior. It is quite possible that each instance has its own computational cliff, but that the location of the cliff varies widely between instances. In such a case we believe that it will be impossible to use the "average over instances" approach in order to predict the behavior of search, and so instead will need to use other properties of the instances that emerge as they are being solved. This is major part of the motivation for our focus on derived constraints (no-goods) that can be generated as part of the search process.

Search: One-samp and iterative sampling

Many algorithms are based on doing a sampling of the search space by doing a number of constructive "greedy" probes. Each probe starts from an empty solution and attempts to build a solution. Heuristics are greedy in that they just take the seeming best choice, and do not, because it would take too much time, do a deeper lookahead.

The simplest case is a single greedy probe, or "sample", that we call "one-samp".

As a simple example consider the following one-samp method for switchGridSAT:

ONE-SAMP(simple):
put all switches s to false
   loop: 
       if ( all switches are irrevocably valued ) 
           return current switch values
       else
          select a switch s
          if ( the theory is still satisfiable with s=true )
             s := true   (irrevocably)
          else 
             s := false  (irrevocably)

this attempts to maximize the number of switches set true.

Example

Instance switchgrid(10,10,1,10;800;50)

10 x 10 grid with 1 x 10 clause bounds
800 clauses
50 switches

The time taken on doing such a search is mostly spent finding out whether the theory is still satisfiable when trying to set a switch to true. The picture below gives an example of the cumulative time spent before each success, that is, to add a new switch. (We will return to the other line, regarding UPIs, shortly).

Times and UPIS for a 1-samp probe
x-axis is number of successful switches
y axis is either time taken, or the number of UPIs after turning on those switches

Landmarks on the success/time curves

The phase transition (PT) grid(10,10,1,-1;c) is at about c=417 clauses.

So, if switches were selected randomly, we would expect the start to seem failures when about 417 clauses are active. With 800 clauses and 50 switches, each switch activates roughly 16 clauses. Hence, knowledge of the PT predicts we should first see failures at about 417/16, about 26, switches. Which is in good agreement with the experiment.

After seeing the first failure, it is still possible that some of the switches are acceptable, though some will fail. The failures are very costly in time, and this is why the times increase rapidly.

More generally we can define a number of landmarks

first-failure point number of clauses/constraints/switches that first cause a new switch to be rejected.
final-failure point number of switches beyond which we no longer see any successes.
optimal final-failure point the final fail point for a probe that makes all the best decisions

In fact the switches are ordered heuristically, so that switches that activate the fewest new clauses are put first (a standard least-constraining first approach). So for the instance of the graph we had

first-failure point at 386 clauses. In terms of the PT this corresponds to the point when about 20% of the instances will be unsatisfiable.
final-failure point at 441 clauses. In the PT about 80% of the instances are unsatisfiable here.
optimal final-failure point the best case would be 38 switches, corresponding to about 600 clauses. Note that this would be in the deep unsatisfiable region of the PT. However, this is not a contradiction because the set of switches are carefully selected for the optimal, whereas the PT refers to average properties.

It seems that knowledge of the PT can be used to give reasonable predictions of the first-failure and final-failure points of the one-samp probe. However, it does mean that the naive use of PT to predict optimal solution will be incorrect ; though the PT does seem to be reasonable predictor of the likely "easily-accessible" solutions

One-SAMP and UPIs

A "Unary Prime Implicate" (UPI) is a special case of a derived constraint; the case that a variable is forced to have a single value. If x is a UPI then all satisfying solutions contain x set to true, but never set to false.

As the theory approaches optimality then it is natural that it becomes more constrained, and the number of UPIs increases. In fact, as we saw above, and is well-known, the number of UPIs is zero until we are close to the phase transition region.

Our goal is to use the appearance of derived constraints, such as UPIs, to detect when we are approaching a computational cliff. Their potential usage can be seen above; the number of UPIs becomes non-zero just a little before the times start to increase more rapidly.

Derived constraints are properties of the single instance, rather than a average property of a large collection of instances, and hence have more potential for flexible usage, than direct usage of phase transition information.

The project will be developing methods to cheaply create and monitor derived constraints (no-goods) in order to detect imminent computational cliffs, and also to guide coalition formation, and re-formation, within distributed search systems.