The DPLL/Davis-Putnam-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. Backtracking is a strategy for finding solutions to constraint satisfaction problems. ... Flowcharts are often used to represent algorithms. ... The Boolean satisfiability problem (SAT) is a decision problem considered in complexity theory. ... A propositional calculus is a formal, deduction system, or proof theory for reasoning with propositional formulas as symbolic logic. ... In Boolean logic, Conjunctive Normal Form (CNF) is a method of standardizing and normalizing logical formulas. ...

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 referred to as the “Davis-Putnam method” or the “DP algorithm”. Other common names that maintain the distinction are DLL and DPLL. 1962 (MCMLXII) was a common year starting on Monday (link will take you to calendar). ... Martin Davis, (born 1926, New York City) is an American mathematician, known for his work on Hilberts tenth problem. ... Hilary Whitehall Putnam (born July 31, 1926) is a key figure in the philosophy of mind during the 20th century. ... The Davis-Putnam algorithm is an algorithm for checking the satisfiability of formulae in conjunctive normal form, i. ... The word resolution has several meanings, depending on context. ... 1960 (MCMLX) was a leap year starting on Friday (link will take you to calendar). ...

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. Automated theorem proving (currently the most important subfield of automated reasoning) is the proving of mathematical theorems by a computer program. ... First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as there exists an x such that. ...

The algorithm

The basic backtracking algorithm runs by choosing a literal, assigning a truth value to it, simplifying the formula and then recursively checking if the simplified formula is satisfiable; if this is the case, the original formula is satisfiable; otherwise, the same recursive check is done assuming the opposite truth value. This is known as the splitting rule, as it splits the problem into two simpler sub-problems. The simplification step essentially removes all clauses which become true under the assignment from the formula, and all literals that become false from the remaining clauses.

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

Unit propagation 

If a clause is a unit clause, i.e. it contains only a single unassigned literal, this clause can only be satisfied by assigning the necessary value to make this literal true. Thus, no choice is necessary. In practice, this often leads to deterministic cascades of units, thus avoiding a large part of the naive search space.

Pure literal elimination 

If a propositional variable occurs with only one polarity in the formula, it is called pure. Pure literals can always be assigned in a way that makes all clauses containing them true. Thus, these clauses do not constrain the search anymore and can be deleted. While this optimization is part of the original DPLL algorithm, most current implementations omit it, as the effect for efficient implementations now is negligible or, due to the overhead for detecting purity, even negative.

Unsatisfiability of a given partial assignment is detected if one clause becomes empty, i.e. if all its variables have been assigned in a way that makes the corresponding literals false. Satisfiability of the formula is detected either when all variables are assigned without generating the empty clause, or, in modern implementations, if all clauses are satisfied. Unsatisfiability of the complete formula can only be detected after exhaustive search. Unit propagation is a procedure of automated theorem proving that can simplify a set of (usually propositional) clauses. ...

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 choosing the branching literal. Efficiency is strongly 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 choosing the branching literals; defining new data structures to make the algorithm faster, especially the part on unit propagation; and defining variants of the basic 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. A clause is a group of words consisting of a subject and a predicate, although, in non-finite clauses, the subject is often not explicitly given. ...

See also

• Davis-Putnam algorithm
• Chaff algorithm

The Davis-Putnam algorithm is an algorithm for checking the satisfiability of formulae in conjunctive normal form, i. ... Chaff is an algorithm for solving instances of the boolean satisfiability problem. ...

References

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