160 Chapter 7 Propositional Satisfiability Techniques
●
Local-Search-SAT selects a random total assignment first. Let us suppose the
assignment is µ ={D, A, B}. Under this assignment, the only unsatisfied
clause is (¬D ∨¬A ∨¬B), and therefore Cost(µ,) = 1. There is no µ
such
that |µ − µ
|=1 and Cost(µ,) < 1. Local-Search-SAT terminates execution
with failure. It behaves differently if the initial guess is different, for instance,
if µ ={¬D, A, ¬B}, then it finds the model in one iteration step.
●
Basic-GSAT selects a random total assignment. Let us suppose it starts also with
the initial guess µ ={D, A, B}. Different than Local-Search-SAT, Basic-GSAT
has two alternatives. It can flip either variable D or B because the correspond-
ing cost is 1 (flipping