DPLL

The Davis–Putnam–Logemann–Loveland procedure, DPLL, decides the satisfiability of a formula in conjunctive normal form by backtracking search^[2]. It alternates two activities. Simplification applies rules that cannot lose solutions: unit propagation sets the only unassigned literal of a clause whose other literals are false, and pure literal elimination sets a literal whose negation occurs nowhere. When no rule applies, the procedure splits: it chooses a variable, assigns it a value, and recurses, trying the other value if the first leads to a clause with every literal false. The formula is satisfiable if some branch satisfies every clause and unsatisfiable if every branch ends in conflict. Martin Davis, George Logemann and Donald Loveland published it in 1962 as a variant of the Davis–Putnam procedure of 1960 that needed far less memory^[1][2]. Every modern SAT solver still runs this search, extended by clause learning.

Write $F{|}_{\ell }$ for the formula obtained by making literal $\ell$ true: clauses containing $\ell$ are removed, and $\neg \ell$ is deleted from the rest. Then^[2][3]:

where $\square$ is the empty clause. The unit and pure rules are applied first because they never need to be undone for their own sake: a unit clause leaves no choice, and a pure literal can be made true without falsifying any clause. Only the split introduces a choice point.

(* DPLL on clauses as lists of integer literals. Assigning a literal
   removes the clauses it satisfies and deletes its negation from the
   others; an empty clause is a conflict. *)
let assign l cs =
  List.filter_map (fun c -> if List.mem l c then None else Some (List.filter (( <> ) (-l)) c)) cs
 
let decisions = ref 0
let trace = ref false
let say depth fmt = Printf.ksprintf (fun s -> if !trace then print_endline (String.make (2 * depth) ' ' ^ s)) fmt
 
let rec dpll ?(pure = true) depth cs model =
  if cs = [] then Some model                                  (* every clause satisfied *)
  else if List.mem [] cs then (say depth "conflict"; None)
  else match List.find_opt (fun c -> List.length c = 1) cs with
    | Some [ l ] ->                                           (* unit clause: l is forced *)
      say depth "unit %d" l; dpll ~pure depth (assign l cs) (l :: model)
    | _ ->
      let lits = List.sort_uniq compare (List.concat cs) in
      match (if pure then List.find_opt (fun l -> not (List.mem (-l) lits)) lits else None) with
      | Some l ->                                             (* pure literal: safe to set *)
        say depth "pure %d" l; dpll ~pure depth (assign l cs) (l :: model)
      | None ->
        let v = abs (List.hd lits) in                         (* branch *)
        incr decisions;
        say depth "decide %d" v;
        match dpll ~pure (depth + 1) (assign v cs) (v :: model) with
        | Some m -> Some m
        | None -> say depth "decide %d" (-v); dpll ~pure (depth + 1) (assign (-v) cs) (-v :: model)

open Dpll

decide 3
  decide 2
    unit 1
    conflict
  decide -2
    unit 1
    conflict
decide -3
  decide 2
    unit 1
    conflict
  decide -2
    unit 1
    conflict
UNSAT
--
pure 5
pure 4
decide 3
  unit -2
  unit 1
SAT: 5 4 3 -2 1

In the satisfiable example, the pure literals 5 and 4 are set first, removing two clauses, and a single decision then propagates to a full model. Implementations do not copy the formula at each step as this one does; they keep one assignment, a trail of the literals set so far in order, and undo the trail back to the last decision when they backtrack, which is called chronological backtracking.

The procedure terminates because every step either assigns a variable or ends a branch, and the depth is bounded by the number of variables. It is sound, since a claimed model satisfies every clause, and complete, since the split covers both values of the variable, and the unit and pure rules only discard assignments that cannot lead to a model or that can be modified into one that does not use them. Memory is linear in the size of the formula, which was the point of the 1962 version.

Time is exponential in the worst case. On an unsatisfiable formula, the search tree of DPLL can be read as a tree-like resolution refutation: each leaf is a clause falsified by the branch, and each split resolves the refutations of its two subtrees on the split variable. Lower bounds on tree-like resolution therefore bound DPLL on every branching order^[4][11]. The pigeonhole formulas, which have no short resolution proofs of any kind^[10], make the growth visible.

(* How the search grows: DPLL decisions against CDCL conflicts. *)
let dpll_decisions ~pure (f : Cnf.cnf) =
  Dpll.decisions := 0; ignore (Dpll.dpll ~pure 0 f.clauses []); !Dpll.decisions

pigeonhole  DPLL decisions  (no pure rule)  CDCL conflicts
    3+1                5                8               7
    4+1               23               51              28
    5+1              119              374             154
    6+1              719             3245             758
    7+1             5039            32780            4164
random 3-SAT, 4.5 clauses per variable, medians of 11
    n  DPLL decisions  CDCL conflicts
   20              15              10
   30              25              17
   40              65              31
   50             267              54
   60             923              72
   70            1338             109

On the pigeonhole formulas with $n$ holes, DPLL with the pure literal rule makes exactly $n!-1$ decisions, and without it several times more. Clause learning does not help much here, because the formulas are hard for general resolution, which bounds CDCL as well. On random formulas the gap is large: CDCL's conflicts grow far more slowly than DPLL's decisions.

The choice of the variable to split on, and of the value to try first, determines the size of the tree. Classical DPLL solvers used static measures of the current formula: MOMS heuristics prefer variables with the most occurrences in the shortest clauses, and the Jeroslow–Wang rule weights each occurrence of a literal in a clause of length $k$ by $2^{-k}$^[5]. Lookahead solvers try assigning each candidate variable, propagate, and measure how much the formula shrinks, choosing the variable whose two branches reduce it most^[6][7]. Lookahead remains strong on small hard random formulas; on large structured instances it was overtaken by the cheap, conflict-driven VSIDS heuristic of CDCL solvers.

The 1960 procedure of Davis and Putnam also used unit and pure literal rules, but eliminated variables instead of splitting on them: to remove $x$, it replaced all clauses containing $x$ or $\neg x$ by all their resolvents on $x$^[1]. This is complete, but the number of clauses can grow quadratically at each elimination and exponentially overall. When Logemann and Loveland implemented the method on an IBM 704, the memory ran out, and they replaced elimination by the splitting rule, which only needs a stack^[2][8]. Variable elimination returned decades later as a preprocessing step in CDCL solvers, applied only where it does not increase the number of clauses.

DPLL backtracks chronologically, to the most recent decision, even if that decision had nothing to do with the conflict, and it forgets the reason for the conflict, so the same contradiction can be rediscovered in many branches. Conflict-driven clause learning, introduced by GRASP in 1996, analyzes each conflict to derive a clause that explains it, adds the clause to the formula, and jumps back to the decision that the clause implicates^[9]. Nieuwenhuis, Oliveras and Tinelli described both as transition systems over partial assignments, in which DPLL and CDCL differ only in the backtracking and learning rules, and extended the system to DPLL(T) for SMT^[3]. With learning and restarts, a CDCL solver can simulate general resolution, which is exponentially stronger than the tree-like resolution that bounds DPLL^[4].

Martin Davis and Hilary Putnam published their procedure in 1960 as part of a method for first-order logic based on Herbrand's theorem^[1]. Implementing it at New York University, George Logemann and Donald Loveland replaced resolution-based elimination by splitting, and the three published the resulting program in 1962^[2][8]. The algorithm, often named DPLL after all four authors, was the basis of complete SAT solvers for three decades; heuristics and lookahead refined it through the 1990s^[5][6], and clause learning transformed it into CDCL from 1996^[9].

• CDCLConflict-driven clause learning (CDCL) is the algorithm of modern SAT solvers. It extends DPLL backtracking search with three ideas: when propagation falsifies a clause, conflict analysis derives a new clause that explains the conflict and adds it to the formula; the solver then backjumps non-chronologically to the decision level at which the new clause forces a literal; and branching follows the variables involved in recent conflicts. With watched literals, restarts and clause deletion, CDCL solvers decide industrial formulas with millions of variables, and with restarts they are as strong as general resolution, exponentially stronger than DPLL.
• Unit propagationUnit propagation is the inference rule at the core of SAT solvers: when every literal of a clause is false under the current partial assignment except one unassigned literal, that literal must be true. Applying the rule until nothing changes either extends the assignment or finds a clause with every literal false, a conflict. It decides satisfiability of Horn formulas on its own, it takes most of the running time of a modern CDCL solver, and it is implemented with two watched literals per clause so that only clauses that may have become unit are ever inspected.
• Pure literal eliminationPure literal elimination is a simplification rule for formulas in conjunctive normal form: if a variable occurs in the formula only positively, or only negatively, it can be set so that all its occurrences are true, and every clause containing it can be deleted, without changing whether the formula is satisfiable. It is one of the rules of the DPLL procedure. Modern CDCL solvers do not apply it during search, because detecting pure literals is expensive, but it survives in preprocessing, generalized by autarkies and blocked clause elimination.
• SATThe Boolean satisfiability problem, SAT, asks whether some assignment of true and false to the variables of a propositional formula makes the formula true. It was the first problem shown to be NP-complete, so every problem in NP reduces to it, and no polynomial-time algorithm is known. In practice SAT solvers based on conflict-driven clause learning decide industrial instances with millions of variables, which has made SAT a general-purpose engine for hardware and software verification, planning, scheduling and combinatorics.
• ResolutionResolution is the inference rule that derives, from two clauses containing a variable with opposite signs, the clause of all their other literals: from C ∨ x and D ∨ ¬x, infer C ∨ D. It is sound and refutation complete for propositional logic, so a set of clauses is unsatisfiable exactly when the empty clause can be derived. Resolution is the proof system behind SAT solvers, whose runs on unsatisfiable formulas are resolution refutations, and behind first-order theorem provers and logic programming. Some formulas, such as the pigeonhole formulas, have only exponentially long resolution refutations.
• DPLL(T)DPLL(T) is the architecture of lazy SMT solvers: a CDCL SAT solver searches over the Boolean structure of a formula, treating each theory atom as a propositional variable, and a theory solver for T checks the consistency of the atoms it assigns. When the theory solver finds the assigned literals inconsistent, it returns an explanation, whose negation the SAT solver learns as a clause before backjumping; it may also propagate literals the assignment implies. The approach separates a generic engine from pluggable theory solvers and is used by nearly all SMT solvers, including Z3, cvc5 and Yices.
• 2-SAT2-SAT is Boolean satisfiability restricted to formulas in conjunctive normal form whose clauses have at most two literals. Unlike 3-SAT it is solvable in linear time: each clause (a or b) is a pair of implications, not a implies b and not b implies a, and the formula is unsatisfiable exactly when some variable and its negation lie in the same strongly connected component of the resulting implication graph. A satisfying assignment can be read off a topological order of the components. Random 2-SAT has a sharp satisfiability threshold at one clause per variable.
• Pigeonhole formulaThe pigeonhole formulas PHPⁿ⁺¹ₙ are CNF formulas stating that n + 1 pigeons can be placed in n holes with no two in the same hole. They are unsatisfiable, as the pigeonhole principle says, but Haken proved in 1985 that every resolution refutation of them has exponential size. Since SAT solvers based on DPLL and CDCL produce resolution proofs, they need exponential time on these small formulas, which makes the family the standard example of what resolution cannot do. Proof systems that can count, such as cutting planes and extended resolution, refute them in polynomial size.
• VSIDSVSIDS, Variable State Independent Decaying Sum, is the branching heuristic of conflict-driven SAT solvers. Each variable has an activity score, which is increased whenever the variable takes part in a conflict and decays geometrically over time; when the solver must make a decision, it branches on the unassigned variable with the highest activity. The heuristic is cheap, because it depends on conflicts rather than on the current formula, and it focuses the search on the variables involved in recent conflicts. It was introduced by the Chaff solver in 2001 and, in the exponential form used by MiniSat, remains the default in most solvers.
• Watched literalsThe two-watched-literal scheme is the data structure SAT solvers use to detect unit and conflicting clauses. Each clause of two or more literals watches two of its literals that are not false; a clause is examined only when one of its watched literals becomes false, and then it either finds a replacement watch, becomes unit, or is a conflict. Because the watches remain valid when assignments are undone, backtracking costs nothing, and a clause with many literals is touched only when its watches are hit. Introduced by the Chaff solver in 2001, it made unit propagation, which dominates solver time, several times faster.

1. [1]M. Davis, H. Putnam, “A computing procedure for quantification theory”, Journal of the ACM 7 (1960).
2. [2]M. Davis, G. Logemann, D. Loveland, “A machine program for theorem-proving”, Communications of the ACM 5 (1962).
3. [3]R. Nieuwenhuis, A. Oliveras, C. Tinelli, “Solving SAT and SAT Modulo Theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T)”, Journal of the ACM 53 (2006).
4. [4]P. Beame, H. Kautz, A. Sabharwal, “Towards understanding and harnessing the potential of clause learning”, Journal of Artificial Intelligence Research 22 (2004).
5. [5]R. G. Jeroslow, J. Wang, “Solving propositional satisfiability problems”, Annals of Mathematics and Artificial Intelligence 1 (1990).
6. [6]C. M. Li, Anbulagan, “Heuristics based on unit propagation for satisfiability problems”, IJCAI (1997).
7. [7]M. J. H. Heule, H. van Maaren, “Look-ahead based SAT solvers”, in A. Biere et al. (eds.), Handbook of Satisfiability, IOS Press (2009).
8. [8]M. Davis, “The early history of automated deduction”, in A. Robinson, A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier (2001).
9. [9]J. P. Marques-Silva, K. A. Sakallah, “GRASP: a search algorithm for propositional satisfiability”, IEEE Transactions on Computers 48 (1999).
10. [10]A. Haken, “The intractability of resolution”, Theoretical Computer Science 39 (1985).
11. [11]E. Ben-Sasson, R. Impagliazzo, A. Wigderson, “Near optimal separation of tree-like and general resolution”, Combinatorica 24 (2004).

last updated 28 September 2026