DPLL algorithm

O(2^n)</math>"},"best-time":{"wt":"<math>O(1)</math> (constant)"},"space":{"wt":"<math>O(n)</math> (basic algorithm)"}},"i":0}}]}'>

DPLL
After 5 fruitless attempts (red), choosing the variable assignment a=1, b=1 leads, after unit propagation (bottom), to success (green): the top left CNF formula is satisfiable.
Class	Boolean satisfiability problem
Data structure	Binary tree
Worst-case performance	O(n) (basic algorithm)

In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search 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 1961 by Martin Davis, 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 Hilary 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.

Algorithm DPLL Input: A set of clauses Φ. Output: A truth value indicating whether Φ is satisfiable. function DPLL(Φ) // unit propagation: while there is a unit clause {l} in Φ do Φ ← unit-propagate(l, Φ); // pure literal elimination: while there is a literal l that occurs pure in Φ do Φ ← pure-literal-assign(l, Φ); // stopping conditions: if Φ is empty then return true; if Φ contains an empty clause then return false; // DPLL procedure: l ← choose-literal(Φ); return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {¬l});

• "←" denotes assignment. For instance, "largest ← item" means that the value of largest changes to the value of item.
• "return" terminates the algorithm and outputs the following value.

In this pseudocode, unit-propagate(l, Φ) and pure-literal-assign(l, Φ) are functions that return the result of applying unit propagation and the pure literal rule, respectively, to the literal l and the formula Φ. In other words, they replace every occurrence of l with "true" and every occurrence of not l with "false" in the formula Φ, and simplify the resulting formula. The or in the return statement is a short-circuiting operator. Φ ∧ {l} denotes the simplified result of substituting "true" for l in Φ.

The algorithm terminates in one of two cases. Either the CNF formula Φ is empty, i.e., it contains no clause. Then it is satisfied by any assignment, as all its clauses are vacuously true. Otherwise, when the formula contains an empty clause, the clause is vacuously false because a disjunction requires at least one member that is true for the overall set to be true. In this case, the existence of such a clause implies that the formula (evaluated as a conjunction of all clauses) cannot evaluate to true and must be unsatisfiable.

The pseudocode DPLL function only returns whether the final assignment satisfies the formula or not. In a real implementation, the partial satisfying assignment typically is also returned on success; this can be derived by keeping track of branching literals and of the literal assignments made during unit propagation and pure literal elimination.

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: there exist instances for which the running time is constant or exponential depending on the choice of the branching literals. Such choice functions are also called heuristic functions or branching heuristics.

The sequent calculus-similar notation can be used to formalize many rewriting algorithms, including DPLL. The following are the 5 rules a DPLL solver can apply in order to either find or fail to find a satisfying assignment, i.e. l in l. This rule represents the idea a currently false clause with only one unset variable left forces that variable to be set in such a way as to make the entire clause true, otherwise the formula will not be satisfied.Φ but its negation ¬l are not in l. This rule represents the idea that if a variable appears only purely positively or purely negatively in a formula, all the instances can be set to true or false to make their corresponding clauses true.Φ and neither A, then decide on the truth value of ∙l. This rule represents the idea that if you aren't forced to do an assignment, you must choose a variable to assign and make note which assignment was a choice so you can go back if the choice didn't result in a satisfying assignment.Φ, and their negations A can be represented as A to {l1,…,ln} is in A, and there is no conflict marker

In 1989-1990, Stålmarck's method for formula verification was presented and patented. It has found some use in industrial applications.

DPLL has been extended for automated theorem proving for fragments of first-order logic by way of the DPLL(T) algorithm.

In the 2010-2019 decade, work on improving the algorithm has found better policies for choosing the branching literals and new data structures to make the algorithm faster, especially the part on unit propagation. However, the main improvement has been a more powerful algorithm, Conflict-Driven Clause Learning (CDCL), which is similar to DPLL but after reaching a conflict "learns" the root causes (assignments to variables) of the conflict, and uses this information to perform non-chronological backtracking (aka backjumping) in order to avoid reaching the same conflict again. Most state-of-the-art SAT solvers are based on the CDCL framework as of 2019.

Runs of DPLL-based algorithms on unsatisfiable instances correspond to tree resolution refutation proofs.

• Proof complexity
• Herbrandization

General

• Davis, Martin; Putnam, Hilary (1960). "A Computing Procedure for Quantification Theory". Journal of the ACM. 7 (3): 201–215. doi:10.1145/321033.321034. S2CID 31888376.
• John Harrison (2009). Handbook of practical logic and automated reasoning. Cambridge University Press. pp. 79–90. ISBN 978-0-521-89957-4.

Specific