A solution to a SAT problem is an assignment of values to
each of the letters so that every clause in
is satisfied.
None of this should be new. Satisfiability of SAT instances is well-known to be NP-complete [CookCook1971], and the language is a reasonably natural one for encoding real-world problems. As we remarked in the introduction, the classic algorithm for solving these problems is depth-first search augmented with an ability to set variables whose values are forced:
Variables are assigned values in two ways. In the first, unit propagation, the clause set is examined under the existing partial assignment and new consequential assignments are identified. Somewhat more specifically (see below), clauses are found that have no satisfied literals and exactly one unvalued literal. In each such clause, the unvalued literal is valued so as to satisfy the clause. This process is repeated until a contradiction is encountered, a solution is found, or no more clauses meet the necessary conditions. If the unit propagation function terminates without reaching a contradiction or finding a solution, then a variable is selected and assigned a value, and the procedure recurs.
In practice, the choice of branch literal is crucial to the
performance of the algorithm. (Note that by choosing a branch literal
instead of
, we can also select the order in which values
are tried for the underlying variable.) Relatively early work on
DPLL focused on the selection of branch variables that produced as
many unit propagations as possible, thus reducing the size of the residual
problems that had to be solved recursively. As we will see in
Section 2.3, however, more recent ideas appear to be more effective.
Missing from Procedure 2.2, however, is a description of the propagation process. Here it is:
DPLL has a variety of well-known theoretical properties. It is sound and complete in that every candidate solution returned is a solution of the original problem, and such a solution will be returned if one exists (and failure eventually reported if no solution exists).
From a practical point of view, the running time of DPLL is obviously potentially exponential in the size of the problem, since at each iteration, possibly only a single variable is assigned a value before the routine is invoked recursively. In practice, of course, unit propagation can reduce the number of branch points substantially, but the running time remains exponential on difficult instances [Crawford AutonCrawford Auton1996].
We also point out that on difficult problem instances, most of the
running time is necessarily spent exploring portions of the search
space in which there are no solutions. After all, if is a partial
assignment that can be extended to a solution, the algorithm will
never backtrack away from
. (Indeed, it cannot and retain
completeness, since
may be the only variable assignment that
extends to a full solution at this point.) Given that there can be no
backtrack away from a satisfiable partial assignment, and that the
number of backtracks is exponential in the problem size, it is clear
that most of the time spent by the program is indeed in evaluating
unsatisfiable regions of the search space.