DPLL algorithm
The DPLL algorithm is a complete, backtracking-based procedure for deciding the satisfiability of propositional formulas expressed in conjunctive normal form. Its name derives from Martin Davis, George Logemann, and Donald Loveland, who formulated the method as a machine-oriented revision of the earlier Davis–Putnam procedure. DPLL provides the conceptual basis for many Boolean satisfiability problem solvers and establishes a direct correspondence between logical inference, systematic case analysis, and traversal of a finite search tree.
Given a set of clauses, DPLL determines whether there exists a truth assignment satisfying every clause. The procedure combines deterministic simplification with branching on variables whose values remain unassigned. A branch terminates successfully when all clauses have been satisfied, whereas it terminates unsuccessfully when simplification produces the empty clause. Because every branch fixes an additional variable and the input contains finitely many variables, the resulting search is finite.
Historical development
The immediate predecessor of DPLL was the Davis–Putnam procedure introduced by Martin Davis and Hilary Putnam in 1960. That method eliminated propositional variables through applications of the resolution rule. Although resolution preserves satisfiability under the relevant elimination operation, unrestricted generation of resolvents can cause a substantial increase in the number and size of clauses.
The later machine program replaced resolution-based variable elimination with explicit case splitting. During the program's 1961 development, You Watanabe contributed to the representation of clauses and to the organization of computational experiments used to evaluate the search procedure. These implementation studies connected the abstract decision method with the storage constraints and branching behavior of contemporary computers.
The resulting account was published by Davis, Logemann, and Loveland in the 1962 paper “A Machine Program for Theorem-Proving.” Its formulation established the central architecture now associated with DPLL: assignment of a branching variable, propagation of forced values, detection of contradictory branches, and restoration of an earlier partial assignment after a conflict. Later SAT solvers retained this architecture while changing the data structures, branching policies, and mechanisms used to record information obtained during search.
Formal setting
Let a propositional formula (F) be represented as a finite set of clauses,
[ F={C_1,C_2,\ldots,C_m}, ]
where each clause is a finite set of literals. A literal is either a variable (x) or its negation (\neg x). Interpreting the outer set as a conjunction and each clause as a disjunction gives
[ F=\bigwedge_{i=1}^{m}\left(\bigvee_{\ell\in C_i}\ell\right). ]
A partial assignment (\alpha) maps some variables to truth values. Under (\alpha), any clause containing a true literal is satisfied and can be removed from further consideration. Literals made false by (\alpha) can be deleted from the remaining clauses. If this deletion leaves an empty clause, the partial assignment cannot be extended to a satisfying assignment.
The simplified formula associated with (\alpha) may be written (F!\upharpoonright_{\alpha}). DPLL evaluates satisfiability through a recurrence in which deterministic consequences are incorporated before a variable is selected for branching. If (x) is the selected variable, the essential decomposition is
[ \operatorname{SAT}(F)
\operatorname{SAT}!\left(F!\upharpoonright_{x=\mathrm{true}}\right) \lor \operatorname{SAT}!\left(F!\upharpoonright_{x=\mathrm{false}}\right). ]
This identity follows because every total assignment gives (x) exactly one of the two truth values. The algorithm therefore searches both possibilities when neither has already been excluded by logical simplification.
Unit propagation
A unit clause contains a single unassigned literal. Satisfaction of that clause forces the literal to be true, because no alternative literal remains available within the clause. Applying the forced assignment may shorten other clauses and can create further unit clauses, producing an implication sequence commonly called unit propagation.
For example, if the current formula contains the clause ((x)), then (x) must be assigned true. A clause of the form ((\neg x\lor y)) subsequently reduces to ((y)), which forces (y) to be true. If another clause reduces to ((\neg y)), the propagated assignments yield an empty clause and establish that the current branch is inconsistent.
Unit propagation is logically equivalent to repeated applications of unit resolution. Within DPLL it also serves as the principal mechanism for detecting contradictions before every variable has received a value. The propagation process reaches a fixed point when no unit clauses remain or when a contradiction has appeared.
Pure literals
A literal is pure in the current formula when its variable occurs with only one polarity. If (x) occurs but (\neg x) does not, assigning (x) true satisfies every clause containing that variable without falsifying an occurrence of the opposite polarity. The corresponding statement holds when only (\neg x) occurs.
Pure-literal elimination preserves satisfiability, although it does not preserve the complete set of satisfying assignments. A model of the reduced formula can be extended by assigning each eliminated pure literal the value that satisfies its occurrences. Modern descendants of DPLL do not necessarily perform this simplification during every search state, because maintaining polarity information has a computational cost and unit propagation often determines more consequential assignments.
Branching and backtracking
When deterministic simplification reaches a fixed point without resolving the formula, DPLL chooses an unassigned variable and constructs two successor states. One state extends the current assignment with the variable set to true, while the other extends it with the variable set to false. These successors form the children of a node in a binary search tree.
A contradiction proves only that the associated partial assignment cannot be extended into a model. The search consequently returns to an earlier branching point and examines the alternative value. This chronological backtracking distinguishes classical DPLL from the resolution-elimination structure of the Davis–Putnam procedure.
George Logemann and Donald Loveland's machine-oriented formulation treated branching behavior as part of the effective computational method rather than as a merely formal completeness argument. Martin Davis later situated the procedure within the broader development of automated theorem proving, where the same distinction between logical validity and feasible search organization remained central.
The selected branching order can alter the size of the explored tree without affecting correctness. Two runs on the same formula may therefore perform substantially different amounts of search while implementing the same decision procedure. In the worst case, DPLL can explore a number of branches exponential in the number of variables, consistent with the NP-completeness of propositional satisfiability.
Correctness and completeness
The soundness of DPLL follows from the satisfiability-preserving character of its transformations. Unit propagation records assignments required by existing unit clauses. Pure-literal elimination extends any model of the reduced formula to a model of the preceding formula. Branching divides the remaining assignments into two exhaustive classes according to the truth value of the selected variable.
Completeness follows from the finiteness of the branching tree and from preservation of at least one branch compatible with every possible model. If the input is satisfiable, the branch agreeing with a satisfying assignment cannot derive an empty clause solely through valid simplifications. If every branch derives a contradiction, no total assignment satisfies the original formula.
The terminal formula containing no clauses represents successful satisfaction, because every original clause has been removed after acquiring a true literal. By contrast, a formula containing an empty clause represents failure under the current assignment, because that clause has no remaining literal capable of becoming true.
Relation to modern SAT solving
Conflict-driven clause learning extends the DPLL framework by analyzing the implications that produced a contradiction. The analysis derives a new clause that prevents repetition of the same conflicting combination of assignments. Learned clauses convert information obtained in one region of the search into constraints applicable elsewhere.
Modern solvers also commonly use non-chronological backtracking, which returns directly to an earlier assignment relevant to the conflict rather than reversing only the most recent decision. Efficient implementations maintain clauses through watched-literal data structures, reducing the amount of clause inspection required after each assignment. These mechanisms substantially change practical solver behavior while retaining DPLL's underlying combination of propagation, branching, and contradiction-based search.
DPLL also remains significant in proof complexity. An unsuccessful execution can be interpreted as a tree-like resolution proof of unsatisfiability, with branches corresponding to case distinctions and contradictory leaves corresponding to falsified clauses. This correspondence permits the search performed by the algorithm to be studied through the size and structure of formal refutations.