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 , 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 , 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 . We use this maximum likelihood value for j as
instead of Eq. (7) for random soluble k-SAT problems.
This estimate is readily computed from the number of conflicts.