Davis-Logemann-Loveland algorithm

The Davis-Logemann-Loveland algorithm is an algorithm for checking the satisfiability or propositional formulae in conjunctive normal form. It is a backtracking algorithm over the space of propositional models enhanced with some rules tailored to the specific problem and aimed at reducing the search space.

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 Davis-Logemann-Loveland 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.

This algorithm is sometimes incorrectely referred to in the scientific literature as the Davis-Putnam algorithm, which is a form of resolution. Other common, and more correct, names are DLL and DPLL.

See also

• Davis-Putnam algorithm
• Chaff algorithm
• Resolution

References

• M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394-397, 1962.

• M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:201-215, 1960.