Boolean Satisfiability and DPLL: The Core Algorithm

Picture a padlock with three numbered dials: A, B, C. Each dial is binary — it can only point to 0 (False) or 1 (True). The lock opens only when a specific combination satisfies a set of rules written on the back of the box:

• Rule 1: At least one of A or B must be True.
• Rule 2: If A is True, then C must be True.
• Rule 3: B and C cannot both be True.

Can you open the lock? If so, what combination works?

This is Boolean Satisfiability (SAT): given a set of Boolean variables and a set of constraints (clauses) over them, find an assignment of True/False to each variable that satisfies every clause — or determine that none exists.

CNF is the universal language. Every Boolean constraint can be rewritten as a conjunction of clauses. A literal is either a variable (positive literal, e.g. A) or its negation (negative literal, e.g. ¬A). A clause is an OR of literals. The whole formula is an AND of clauses.

Our padlock rules above translate directly:

This is a 3-clause CNF over three variables. Any assignment that makes all three clauses True simultaneously is a satisfying assignment.

In the previous lesson you encoded the 4-Queens problem as a CSP: variables Q1–Q4 (column of each queen), domain 4, and binary not-attack constraints. How does that become SAT?

The key idea: replace each (variable, value) pair with a Boolean indicator variable, then write clauses that enforce the original CSP semantics.

This encoding is called the direct/naive encoding. Modern SAT-based CSP solvers use more compact encodings (commander encoding, ladder encoding), but the principle is the same: every domain value becomes a Boolean, every constraint becomes a clause set. ^{[Handbook of Satisfiability (2nd ed.)]}

Named after Davis, Putnam, Logemann, and Loveland (1960–62), DPLL is a systematic backtracking search over truth assignments, accelerated by two powerful inference rules that collapse large parts of the search tree before you even branch. ^{[A Machine Program for Theorem-Proving (DPLL original paper)]}

DPLL has three interlocking rules:

Rule 1 — Unit Propagation (UP): If a clause contains exactly one unassigned literal (a unit clause), that literal must be True (otherwise the clause is immediately falsified). Assign it and simplify. This often cascades — one forced assignment creates new unit clauses.

Rule 2 — Pure Literal Elimination (PLE): If a variable appears in the formula with only one polarity (always positive, or always negative, across all remaining unsatisfied clauses), assigning it to satisfy those clauses can only help, never hurt. Assign it to make those clauses true.

Rule 3 — Splitting (Branching): If neither rule fires, pick an unassigned variable and branch: try True in one recursive call, False in the other. If the True branch fails, backtrack and try False.

flowchart TD
  A([Start: CNF formula F, assignment α]) --> B{All clauses satisfied?}
  B -- Yes --> SAT([Return SAT with α])
  B -- No --> C{Any clause empty?}
  C -- Yes --> UNSAT([Return UNSAT — backtrack])
  C -- No --> D{Unit clause exists?}
  D -- Yes --> E[Unit Propagation: force literal l, simplify F]
  E --> A
  D -- No --> F{Pure literal exists?}
  F -- Yes --> G[Pure Literal Elimination: assign variable, simplify F]
  G --> A
  F -- No --> H[Pick unassigned variable x]
  H --> I[Try x = True → recurse]
  I -- SAT --> SAT
  I -- UNSAT --> J[Try x = False → recurse]
  J --> A

function DPLL(F, α):
  if all clauses in F are satisfied by α:  return SAT(α)
  if some clause in F is empty:            return UNSAT
  if F has a unit clause {l}:
    return DPLL(simplify(F, l), α ∪ {lit(l) = True})
  if F has a pure literal l:
    return DPLL(simplify(F, l), α ∪ {lit(l) = True})
  x ← pick_unassigned_variable(F)
  if DPLL(simplify(F, x), α ∪ {x = T}) = SAT: return SAT
  return DPLL(simplify(F, ¬x), α ∪ {x = F})

Let us trace DPLL on our padlock formula from the opening section:

Step 0 — Initial state. Three clauses, no assignments. No unit clause (each clause has 2 literals). Check for pure literals: A appears positive and negative (in clauses 1 and 2), B appears positive and negative (clauses 1 and 3), C appears positive and negative (clauses 2 and 3). No pure literal either. We must split.

Step 1 — Split on A = True. Simplify:

• (A ∨ B): contains A (True) → satisfied, remove.
• (¬A ∨ C): ¬A is False, remove it → remaining clause: (C) — a unit clause!
• (¬B ∨ ¬C): unchanged.

Remaining formula: (C) ∧ (¬B ∨ ¬C)

Step 2 — Unit propagation: C = True. (C) is a unit clause, force C = True. Simplify:

• (C): satisfied, remove.
• (¬B ∨ ¬C): ¬C is False, remove it → remaining: (¬B) — another unit clause!

Remaining formula: (¬B)

Step 3 — Unit propagation: B = False. (¬B) forces B = False. All clauses are now satisfied.

Result: SAT with A = True, C = True, B = False. ✓

Now step through the algorithm yourself on several different formulas using the interactive widget below.

DPLL from 1962 is not, by itself, the solver inside CP-SAT. But it is the architectural skeleton on which every modern SAT solver is built. Understanding DPLL gives you the vocabulary to understand everything that came after.

1. 1960

   Davis–Putnam procedure

   Resolution-based procedure. Exponential memory; rarely used today.

2. 1962

   DPLL

   Davis, Logemann, Loveland replace resolution with backtracking + unit propagation. Memory-linear. Still the canonical algorithm.

3. 1996–99

   GRASP / CDCL

   Marques-Silva & Sakallah introduce Conflict-Driven Clause Learning. Each conflict generates a new clause that prevents revisiting the same bad decision. Industrial SAT is born.

4. 2001–05

   MiniSat, zChaff, Glucose

   Modern CDCL solvers dominate SAT competitions. Millions of variables, real-time performance.

5. 2011–now

   CP-SAT (OR-Tools)

   Google's CP-SAT solver uses a CDCL SAT core augmented with CP propagators. Routinely handles scheduling problems with tens of thousands of variables.

The jump from DPLL to industrial CDCL solvers has two key ingredients:

1. Clause learning: when a branch fails, analyse why it failed and add a new clause capturing that conflict. Future searches avoid the same dead end without re-exploring it.
2. Non-chronological backjumping: instead of always undoing the most recent decision, jump back to the earliest decision that actually caused the conflict.