Biomedical Engineering Reference
In-Depth Information
to p = ab . We evaluate S ab
by setting b =
0 and simplifying the formula.
S ab =
(0
+ c )
=
( c )
The last varia ble c is selected. Again, let us assume that c is set to its negative literal,
and p
=
abc . We evaluate S abc .
S abc =
(0)
In this case, the partial assignment p
abc causes the formula evaluates to 0, and
the DPLL algorithm backtracks. Let us assume that the algorithm no w sets c to its
positive literal ( c
=
=
1) and partial assignment is updated to p
=
abc . We evaluate
S abc .
S abc =
(1)
At this point, all clauses have been sati sfie d and all variables have been assigned. We
conclude that S is satisfiable and p
abc is a satisfying assignment.
Modern SAT solvers [ 23 ], [ 24 ], [ 25 ], [ 26 ] augment DPLL with techniques such as
variable selection heuristics, clause learning, and watched literals to greatly improve
SAT solving efficiency. In the following, we briefly describe each of these techniques.
Variable selection heuristics vary widely between SAT solvers. The next vari-
able to branch on has a key role to play in determining solver efficiency. Common
strategies include random selection of a variable, maximum occurrence of variable
in clauses of minimum size, most frequent variable in unsatisfied clauses, or choose
variables based on weights from conflicts.
Watched literals [ 25 ] is an efficient method to identify variables for assignment
that are required to satisfy S i . For example, if a clause consists of one unassigned
literal and all other literals are set to 0 value, then the unassigned literal must be set
to 1 value for the clause to be satisfied. In this situation, the unassigned variable set
to 1 value is an implication. Any time a decision (variable branch or value set) is
made in DPLL, this generates new implications.
In [ 25 ], the method selects (watches) two unassigned literals for each clause not
yet satisfied in the partial assignment. When one of these literals is assigned, the watch
is moved to another un assigned literal in the clause. If such a literal does not exists,
then an implication is generated on the other watched literal of the clause. With
this method, implications are detected without analyzing all clauses, significantly
reducing computation and memory requirements for SAT solving.
For example, during the solution process if a variable x is set 0, all clauses with
watched literal x must find another literal to watch as this implies that the other
watched literal must be set to 1 to be satisfied. Furthermore, for any clauses that are
satisfied when x
=
0, these clauses are no longer watched.
Clause learning [ 25 ], [ 26 ] is a technique which improves efficiency of SAT by
avoiding redundant computation on assignments that are unsatisfiable. The technique
keeps track of clauses that become empty, causing a conflict in the algorithm. The
CNF leading to a conflict is analyzed through its implication graph , to create a
=
Search WWH ::




Custom Search