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.

Feb. 1999