Modern Complete SAT Solvers

The efficiency of state-of-the-art complete SAT solvers, extending the basic DPLL approach, relies heavily on various features that have been developed, analyzed, and tested over the last two decades. These include fast unit propagation using watched literals, learning mechanisms, deterministic and randomized restart strategies, nonchronological backtracking, effective constraint database management (clause deletion mechanisms), and smart static and dynamic branching heuristics. We give a flavor of some of these later in this section, referring to [4, 24] for more detailed descriptions.

328

D. Loveland et al.

Algorithm 3: DPLL-WithClauseLearning

Input : A CNF formula

Output: UNSAT, or SAT along with a satisfying assignment begin

decision level — 0

status — UnitPropagate

if status = CONFLICT then return UNSAT

while true do

if no more free variables then

return (SAT, current variable assignment)

DecideNextBranch while true do

status — UnitPropagate if status = CONFLICT then

if decision level = 0 then return UNSAT blevel — AnalyzeConflictAndLearn Backtrack( blevel)

else break

We begin with a variation of Algorithm 2 that mirrors more closely the high level flow of modern day SAT solvers. While fundamentally similar to the recursive formulation of DPLL, this iterative version, outlined in Algorithm 3, makes explicit certain key aspects such as unit propagation, conflict detection and analysis, backtracking to a dynamically computed search tree level, and stopping search on a satisflable formula when all variables have been assigned a value. One important feature that is not included in this pseudocode for simplicity is restarting the solver every so often. The details of various sub-procedures are beyond the scope of this article, but we briefly mention some highlights.

The algorithm maintains a decision level, which starts at zero, is incremented with each branching decision, and decremented (by one or more) upon backtracking. UnitPropagate, as discussed earlier, simplifies the formula by effectively removing true clauses and false literals, setting any resulting unit clauses (i.e., those containing only one active variable) to true, and repeating until no more simplification is possible. This process has a unique fixed point, irrespective of the order in which propagation steps are performed. Algorithm 3 returns UNSAT if it encounters an empty, and hence unsatisfiable, clause during unit propagation at decision level zero. On the other hand, if all variables have been successfully assigned a value without generating the empty clause (a “conflict”), the algorithm returns SAT. Note that this check for satisfiability is different from asking whether the current partial assignment yields a true literal in every clause; this latter test is inefficient when using lazy data structures that will be discussed shortly.

DecideNextBranch heuristically identifies a free variable, assigns it a value, and increments the decision level by one. Again, this is somewhat different from explicitly branching “both ways” on a variable. Instead, clause learning makes the solver implicitly flip the value of the assigned variable upon backtracking. The decision level to which the algorithm backtracks upon encountering a conflict is determined dynamically using a graph-based analysis of the unit propagation steps leading to the conflict. This analysis, performed in AnalyzeConflictAndLearn, also makes the algorithm learn (i.e., add to its set of clauses) a new clause that explains the conflict being analyzed and prevents unnecessary future branching on variables that would lead to a conflict for a similar reason.

With this overall structure in mind, we are ready to explore some of the most prominent features of modern SAT solvers that build upon the DPLL framework. Many of these features directly involve, are guided by, or are necessitated by clause learning.

 
Source
< Prev   CONTENTS   Source   Next >