next up previous
Next: 3.2 Random SAT Problems Up: 3 The Satisfiability Problem Previous: 3 The Satisfiability Problem

3.1 Highly Constrained SAT Problems 

In general, SAT problems are difficult to solve. However, in a few simple cases the very regular structure of the search space allows much more effective algorithms. One example is given by 1-SAT problems. In this case, each clause eliminates one value for a single variable allowing classical algorithms to examine the variables independently, giving an overall search cost of O(n) in spite of the exponentially large number of assignments. A 1-SAT problem has a solution if and only if each of the m clauses involves a distinct variable. Otherwise, both values for some variable will be in conflict, i.e., making a clause false, resulting in no solutions.

This simple structure allows for rapid search. SAT problems with larger clauses have a more complicated structure. Nevertheless, when the k-SAT problems are highly constrained, their structure is close to that of 1-SAT. To see this, consider a soluble k-SAT problem. With respect to a particular solution of that problem, define the good value for each variable as the value (true or false) it is assigned in that solution, while the opposite value is the bad one for that variable. For k-SAT problems with many constraints, the number of bad values in an assignment can usually be determined rapidly from its number of conflicts, even though determining exactly which variables have incorrect assigned values requires first finding the solution. In such cases, using the number of bad values results in a tractable algorithm as long as a priori knowledge of the solution is not assumed.

For example, consider soluble problems with the largest possible number of constraints. For k-SAT, these maximally constrained soluble problems have tex2html_wrap_inline1782 where

  equation142

i.e., the single solution precludes any clause that conflicts with it.

An assignment with j bad values contains tex2html_wrap_inline1786 sets of k variables all of which have the same values as the solution. Each of the remaining sets conflicts with at least one clause in the problem. Thus each assignment with j bad values has

  equation147

conflicts. This quantity grows strictly monotonically with j for tex2html_wrap_inline1794 , so in these cases j is directly determined by the number of conflicts. Assignments with tex2html_wrap_inline1798 are not distinguishable.

Assignments with j=n-k+1 can also be corrrectly determined by including neighborhood information. To see this, consider an assignment s with j bad values, and its n neighbors, i.e., assignments at Hamming distance one from s. Of these neighbors, j have j-1 bad values, and the remaining n-j have j+1 bad values. For tex2html_wrap_inline1794 , s has j neighbors with fewer conflicts and n-j with more. Thus for these assignments, examining the number of conflicts in the neighbors readily determines the value of j. When j=n-k+1, the assignment continues to have j neighbors with fewer conflicts, but now the remaining k-1 neighbors have the same number of conflicts since the additional bad value does not increase the number of conflicts. Finally, the neighbors of assignments with tex2html_wrap_inline1834 all have the same number of conflicts. Thus examining the number of conflicts in an assignment's neighbors determines the value of j, with the exception that assignments with tex2html_wrap_inline1834 are not distinguishable.

The value of j is the number of conflicts that s would have in the maximally constrained 1-SAT problem with the same solution as the given maximally constrained k-SAT problem. Thus for a maximally constrained k-SAT problem let

  equation153

The value of tex2html_wrap_inline1850 can be determined rapidly, in much the same way that a classical local search method checks the number of conflicts among neighbors of its current state to determine which assignment to move to next [42, 47]. Thus tex2html_wrap_inline1852 is a computationally tractable approximation to the number of conflicts each assignment would have in the corresponding 1-SAT problem. Except for a few assignments with many conflicts, tex2html_wrap_inline1852 gives the correct value. Specifically, only assignments with at least n-k+3 bad values are given an incorrect value of j by this approximation. In particular, the approximation is completely correct for k=2.

While classical searches use the number of conflicts in an assignment and its neighbors, another possibility for maximally constrained problems is to use the number of conflicts in the assignment and its complement (i.e., the assignment with opposite values for all the variables). If the assignment has j bad values, its complement will have n-j. As described above, the number of conflicts in an assignment uniquely determines the corresponding value of j provided tex2html_wrap_inline1868 . On the other hand, the number of conflicts in the complement assignment uniquely determines j when tex2html_wrap_inline1872 , or tex2html_wrap_inline1874 . Thus, as long as n;SPMgt;2k, at least one of these conditions will be true for all tex2html_wrap_inline1878 and the correct value of j can be determined.


next up previous
Next: 3.2 Random SAT Problems Up: 3 The Satisfiability Problem Previous: 3 The Satisfiability Problem

Tad Hogg
Feb. 1999