Biomedical Engineering Reference
In-Depth Information
contains a single positive literal, and to satisfy any one of the soft clauses, its corre-
sponding variable needs to be set to its positive literal. However, no more than one of
the three variables can be assigned to their postive litera, while the other two variables
must be assigned to their negative literals in order to satisfy the hard clauses. Of the
soft clauses, ( y ) has the highest w e ight, so the satisfying solution with maximum
weight is ( x , y , z )
=
(0, 1, 0) or xyz , with weight = 7.
1.5.3
SAT Solvers
While several high-performance algorithms exist for solving SAT, the most popular
in logic synthesis and electronic design are conflict driven methods based on the
Davis-Putnam-Logemann-Loveland or DPLL algorithm [ 22 ].
The DPLL algorithm is a complete 2 search process for finding a satisfying assign-
ment by implicitly pruning of the exponentially sized search space. This algorithm
searches for a satisfying assignment through repeated branching and decision steps.
In the branching step, an unassigned variable x is selected in the CNF formula S .
The decision step sets x to 1 or 0, resulting in the CNF formulas S x (which is S
with x replaced by 1) or S x (which is S , with x replaced by 0). The branching and
decision steps are recursively repeated for all remaining unassigned variables in S
until a solution is found, or the search space is exhausted.
The DPLL algorithm performs a depth first traversal of the state space. During
the search, a partial variable assignment list p is recorded. If S p contains an empty
clause (0), for example S p =( ... )
( ... ), then S p is unsatisfiable. In this case,
the DPLL algorithm backtracks and then branches or decides on a different variable
or value. If all variables have been assigned in p and there are no empty clauses in
S p , then S is satisfiable and p is the satisfying assignme nt .
For example, consider the CNF formula S ( a , b , c )
·
(0)
·
c ), where
the variable a is the first to be selected for branching. Also, let us assume that a is s e t
to its negative literal ( a replaced by 0), and the assignment list is updated to p
=
( a
+
b )
·
( a
+
b
+
=
a .
We evaluate S a by setting a
0 and simplifying the formula. We recall that a clause
with a literal evaluating to 1 means the clause is satisfied, and can be removed from
the CNF.
=
S
=
( a
+
b )
·
( a
+
b
+
c )
S a =
(0
+
b )
·
(0
+
b
+
c )
=
( b
+
c )
We continue the example by selecting variable b as the next variable for branching.
Let us assume that b is set to its negative literal, and the assignment list is updated
2 A complete or exact algorithm is one that is guaranteed to find a solution if a solution exists.
 
Search WWH ::




Custom Search