DPLL algorithm

The DPLL/Davis-Logemann-Loveland algorithm is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem.

It was introduced in 1962 by Martin Davis, Hilary Putnam, George Logemann and Donald W. Loveland, and is a refinement of the earlier Davis-Putnam algorithm, which is a resolution-based procedure developed by Davis and Putnam in 1960. Especially in older publications, the Davis-Logemann-Loveland algorithm is often incorrectly referred to as the “Davis-Putnam method” or the “DP algorithm”. Other common, and more correct, names are DLL and DPLL.

DPLL is a highly efficient procedure, and after more that 40 years still forms the basis for most efficient complete SAT solvers, as well as for many theorem provers for fragments of first-order logic.

The algorithm

The basic backtracking algorithm runs by choosing a literal and then recursively checking if the formula conjoined with the literal is satisfiable; if this is the case, the original formula is satisfiable; otherwise, the same recursive check is done by adding the negation of the literal to the original formula.

The DPLL algorithm enhances over the backtracking algorithm by the use of the following rules at each step:

Unit propagation

the clauses containing a single literals are exploited by deleting all other clauses containing the literal and removing the negation of the literal from all other clauses;

Monotone literal elimination

if a variable occurs only positively in the formula, the variable is conjonied with the formula; if it occurs only negatively, its negation is conjoined;

Clause subsumption

if a clause is subsumed (entailed) by another one, it is removed from the formula.

Unsatisfiability is detected as the presence of two opposite unit clauses (clauses with a single literal) in the formula. Satisfiability is detected when the formula contains only unit clauses that are consistent with each other.

The Davis-Logemann-Loveland algorithm depends on the choice of branching literal, which is the literal considered in the backtracking step. As a result, this is not exactly an algorithm, but rather a family of algorithms, one for each possible way of chosing the branching literal. Efficiency is strongy affected by the choice of the branching literal.

Current work

Current work on improving the algorithm has been done on three directions: defining different policies for chosing the branching literals; defining new data structures to make the algorithm faster, especially the part on unit propagation; and defining variants of the basica backtracking algorithm. The latter direction include non-chronological backtracking and clause learning. These refinements describe a method of backtracking after reaching a conflict clause which "learns" the root causes (assignments to variables) of the conflict in order to avoid reaching the same conflict again.

See Also

• Davis-Putnam algorithm
• Chaff algorithm

References

• A Computing Procedure for Quantification Theory, M. Davis and H. Putnam, Journal of the ACM 7(1), 1960.
• A Machine Program for Theorem Proving, M. Davis and G. Logemann and D. Loveland, Communications of the ACM 5, 1962.