next up previous
Next: 3.2.2 Balanced Clauses Up: 3.2 Random SAT Problems Previous: 3.2 Random SAT Problems

3.2.1 Prespecified Solution

The most common use of a prespecified solution is to simply avoid selecting any clauses that conflict with it. Thus, we generate problems by randomly selecting a set of m distinct clauses from among the tex2html_wrap_inline1894 , given by Eq. (5), available clauses [45].

Consider a given soluble k-SAT problem with m clauses, and let the assignment r be one of its solutions. With respect to the solution r, we can define the bad value for each variable. For an assignment with j bad values, the probability it has c conflicts is


where tex2html_wrap_inline1908 , given by Eq. (6), is the largest possible number of conflicts for an assignment with j bad values. The probability that an assignment has j bad values is


From these expressions and the definition of conditional probability, the probability that an assignment with c conflicts has j bad values is


Hence, for a given assignment s with c conflicts, we can estimate the number of bad values it has by picking j that maximizes tex2html_wrap_inline1926 . We use this maximum likelihood value for j as tex2html_wrap_inline1850 instead of Eq. (7) for random soluble k-SAT problems. This estimate is readily computed from the number of conflicts.

Tad Hogg
Feb. 1999