When the DPLL algorithm 2.2 is implemented and run on practical problems, the bulk of the running time is spent in unit propagation. As an example, Figure 1 gives the amount of time spent by ZCHAFF on a variety of microprocessor test and verification examples made available by Velev (http://www.ece.cmu.edu/~mvelev).4 As the problems become more difficult, an increasing fraction of the computational resources are devoted to unit propagation. For this reason, much early work on improving the performance of DPLL focused on improving the speed of unit propagation.
Within the unit propagation procedure 2.3, the bulk of the time is spent identifying clauses that propagate; in other words, clauses that are not satisfied by the partial assignment and contain at most one unvalued literal:
Before we go on to examine the techniques that have been used to speed unit propagation in practice, let us remark that other implementations of SAT solvers have similar properties. Nonsystematic solvers such as WSAT [Selman, Kautz, CohenSelman et al.1993], for example, spend the bulk of their time looking for clauses containing no satisfied or unvalued literals (or, equivalently, maintaining the data structures needed to make such search efficient). We can generalize Observation 2.4 to get:
That said, let us describe the series of ideas that have been employed in speeding the process of identifying clauses leading to unit propagations:
In order to keep these counts current when we set a variable to true, we need to increment and decrement for each clause where appears, and to simply decrement for each clause where appears. If we backtrack and unset , we need to reverse these adjustments.
Compared to the previous approach, we need to examine four times as many clauses (those where appears with either sign, and both when is set and unset), but each examination takes constant time instead of time proportional to the clause length. If the average clause length is greater than four, this approach, due to Crawford and Auton Crawford:exp, will be more effective than its predecessor.
It is only when one of the watched literals is set to false that the clause must be examined in detail. If there is another unset (and unwatched) literal, we watch it. If there is a satisfied literal in the clause, we need do nothing. If there is no satisfied literal, the clause is ready to unit propagate.
If the average clause length is , then when we set a variable (say to true), the probability is approximately that we will need to analyze a clause in which appears, and the work involved is proportional to the length of the clause. So the expected amount of work involved is twice the number of clauses in which appears, an improvement on the previous methods. In fact, the approach is somewhat more efficient than this cursory analysis suggests because the adjustment of the watched literals tends to favor watching those that are set deep in the search tree.
Before we move on to discuss learning in Boolean satisfiability, let us remark briefly on the so-called ``pure literal'' rule. To understand the rule itself, suppose that we have a theory and some partial variable assignment . Suppose also that while a literal appears in some of the clauses in that are not yet satisfied by , the negation does not appear in any such clauses. Now while may not be a consequence of the partial assignment , we can clearly set to true without removing any solutions from the portion of the search space that remains.
The pure literal rule is not generally included in implementations of either the DPLL or the unit propagation procedure because it is relatively expensive to work with. Counts of the number of unsatisfied clauses containing variables and their negations must be maintained at all times, and checked to see if a literal has become pure. In addition, we will see in Section 2.3 that many branching heuristics obviate the need for the pure literal rule to be employed.