DPLL SAT Solver

How DPLL decides satisfiability

A boolean satisfiability (SAT) problem asks one question: given a formula in conjunctive normal form — an AND of OR-clauses, like (x₁ ∨ ¬x₂) ∧ (x₂ ∨ x₃) ∧ (¬x₁ ∨ ¬x₃) — is there any assignment of true/false to the variables that makes the whole thing true? SAT was the first problem proven NP-complete (Cook, 1971), which means thousands of practical problems — circuit verification, scheduling, package dependency resolution, model checking — reduce to it. Solve SAT fast and you solve all of them.

DPLL is the algorithm that made solving SAT practical decades before anyone proved it should be possible at scale. It is a depth-first search over the space of partial assignments, supercharged by two simplification rules that prune most of that space before you ever branch into it. The loop has four moves:

1. Unit propagation. If a clause has all-but-one literal already false, the last literal is forced true. Assign it, simplify, and repeat. One decision often cascades into dozens of forced assignments.
2. Pure literal elimination. If a variable appears with only one polarity in all remaining clauses, assign it that polarity — it can never hurt.
3. Conflict / satisfaction check. If a clause becomes all-false, this branch is dead — backtrack. If every clause has a true literal, you have a model — return SAT.
4. Decide. Pick an unassigned variable, guess a value, and recurse. If the guess fails, flip it and try the other value.

The genius is the ordering. Propagation and pure-literal elimination are cheap and deterministic, so you exhaust them first. Only when the formula is fully simplified and still undecided do you make an expensive, fallible decision. The decision tree branches, but unit propagation collapses entire subtrees on every step, so the effective branching factor is far below 2.

A worked example

Take (x₁ ∨ x₂) ∧ (¬x₁ ∨ x₃) ∧ (¬x₂ ∨ ¬x₃) ∧ (x₃).

Start.                       clauses: (x1 ∨ x2)(¬x1 ∨ x3)(¬x2 ∨ ¬x3)(x3)
Unit clause (x3)  →  x3 = T
  Propagate into (¬x2 ∨ ¬x3): x3=T kills ¬x3, leaves (¬x2)  → unit!
    x2 = F
  Propagate (x1 ∨ x2): x2=F, leaves (x1)  → unit!
    x1 = T
  Propagate (¬x1 ∨ x3): x1=T kills ¬x1, x3=T satisfies. ✓
All clauses satisfied  →  SAT:  x1=T, x2=F, x3=T

Notice that this formula was decided with zero decisions — pure propagation chained four forced assignments and landed on a model. That is the common case for structured instances: the constraints are tight enough that guessing one variable forces hundreds. Random 3-SAT near the satisfiability threshold (clause-to-variable ratio ≈ 4.27) is the opposite — propagation stalls early and the solver branches deeply.

When DPLL is the right tool

• Decision problems you can encode in CNF — verification, planning, constraint satisfaction, cryptanalysis. If you can phrase "does a valid configuration exist?" as clauses, a SAT solver beats a hand-rolled search almost every time.
• Hard combinatorial instances where you want a complete answer — DPLL is sound and complete, so a "UNSAT" verdict is a proof, not a timeout. Local-search solvers like WalkSAT are faster on some satisfiable instances but can never prove unsatisfiability.
• As the foundation you build on. Almost nobody runs textbook DPLL in production; they run CDCL, which is DPLL plus clause learning. But you must understand DPLL to understand, debug, or extend CDCL.

Reach for something else when the problem has rich numeric structure (use an SMT solver or integer programming), when you only need a solution to a satisfiable instance and don't care about completeness (use WalkSAT/local search), or when the encoding to CNF would explode the formula size beyond what propagation can handle.

DPLL vs other SAT approaches

	DPLL	CDCL	Resolution (DP)	WalkSAT	Look-ahead
Year	1962	1996–2001	1960	1994	1990s
Complete?	Yes	Yes	Yes	No	Yes
Proves UNSAT?	Yes	Yes (+ proof)	Yes	No	Yes
Backtracking	Chronological	Non-chronological backjump	n/a (eliminates vars)	none (restarts)	Chronological
Learns clauses?	No	Yes	No	No	Limited
Memory	O(n + m)	O(n + m + learned)	Exponential	O(n + m)	O(n + m)
Best on	Teaching, small instances	Industrial, millions of vars	Tiny / theory	Random SAT	Hard random / crafted

The lineage matters. Davis–Putnam (1960) did variable elimination by resolution and ran out of memory; Logemann and Loveland (1962) swapped resolution for backtracking search — that is DPLL. CDCL then put learning back on top of DPLL's search, and that combination is why a 2024-era solver like Kissat handles formulas DPLL alone would choke on.

What the numbers actually say

• Unit propagation dominates runtime. Profiling competitive solvers shows 80–90% of CPU time is spent inside the propagation engine. This is why Chaff introduced two-watched-literals: it makes propagation touch only clauses that could possibly become unit, cutting the work per assignment from O(clause size) to amortized O(1) per watch.
• The phase transition is sharp. For random 3-SAT, formulas with a clause/variable ratio below ≈4.27 are almost always satisfiable and easy; above it, almost always unsatisfiable and easy; at 4.27 the hardest instances cluster, and runtime can spike by orders of magnitude for the same number of variables.
• Worst case is genuinely exponential. The pigeonhole principle PHP(n) — fit n+1 pigeons into n holes — forces any DPLL/resolution-based solver into 2^Ω(n) steps; it has no short resolution proof. A 20-hole pigeonhole instance can stall a plain DPLL solver for minutes.
• Industrial scale is enormous. Modern CDCL solvers routinely close hardware-verification instances with 10⁶–10⁷ variables and tens of millions of clauses in seconds to minutes — a testament to how far structure-exploiting heuristics push past the worst case.

JavaScript implementation

A clean recursive DPLL. A clause is an array of integers where 3 means literal x₃ and -3 means ¬x₃. An assignment maps variable → true/false.

// formula: array of clauses; clause: array of signed ints (DIMACS-style)
function dpll(formula, assign = {}) {
  // 1. Unit propagation — repeat until fixpoint
  let changed = true;
  formula = formula.map(c => c.slice());
  assign = { ...assign };
  while (changed) {
    changed = false;
    for (const clause of formula) {
      const unresolved = clause.filter(lit => assign[Math.abs(lit)] === undefined);
      const satisfied = clause.some(lit => assign[Math.abs(lit)] === (lit > 0));
      if (satisfied) continue;
      if (unresolved.length === 0) return null;       // conflict: empty clause
      if (unresolved.length === 1) {                  // unit clause → force it
        const lit = unresolved[0];
        assign[Math.abs(lit)] = lit > 0;
        changed = true;
      }
    }
  }

  // 2. Are all clauses satisfied?
  const allSat = formula.every(c => c.some(lit => assign[Math.abs(lit)] === (lit > 0)));
  if (allSat) return assign;

  // 3. Pick an unassigned variable to branch on
  let v;
  for (const clause of formula) {
    for (const lit of clause) {
      if (assign[Math.abs(lit)] === undefined) { v = Math.abs(lit); break; }
    }
    if (v) break;
  }
  if (v === undefined) return null;

  // 4. Try v = true, then v = false (chronological backtracking)
  return dpll(formula, { ...assign, [v]: true })
      || dpll(formula, { ...assign, [v]: false });
}

// (x1 ∨ x2)(¬x1 ∨ x3)(¬x2 ∨ ¬x3)(x3)
console.log(dpll([[1, 2], [-1, 3], [-2, -3], [3]]));
// → { '3': true, '2': false, '1': true }

This copies the assignment on every recursive call for clarity. Production solvers never do that — they push assignments onto a single trail and pop them on backtrack, so the per-decision cost is O(1) instead of O(n). The copy-on-recurse style above is correct but allocates heavily; fine for teaching, fatal at scale.

Python implementation

The same algorithm, plus the pure-literal rule, in iterative-friendly Python.

def dpll(formula, assign=None):
    assign = dict(assign or {})

    # 1. Unit propagation to fixpoint
    changed = True
    while changed:
        changed = False
        for clause in formula:
            if any(assign.get(abs(l)) == (l > 0) for l in clause):
                continue                                  # already satisfied
            unbound = [l for l in clause if abs(l) not in assign]
            if not unbound:
                return None                               # conflict
            if len(unbound) == 1:                         # unit clause
                lit = unbound[0]
                assign[abs(lit)] = (lit > 0)
                changed = True

    # 2. Pure literal elimination
    counts = {}
    for clause in formula:
        if any(assign.get(abs(l)) == (l > 0) for l in clause):
            continue
        for l in clause:
            if abs(l) not in assign:
                counts.setdefault(abs(l), set()).add(l > 0)
    for var, polarities in counts.items():
        if len(polarities) == 1:                          # pure
            assign[var] = next(iter(polarities))

    # 3. Satisfied?
    if all(any(assign.get(abs(l)) == (l > 0) for l in clause) for clause in formula):
        return assign

    # 4. Branch on the first unassigned variable
    unassigned = next(
        (abs(l) for clause in formula for l in clause if abs(l) not in assign),
        None)
    if unassigned is None:
        return None

    for value in (True, False):
        result = dpll(formula, {**assign, unassigned: value})
        if result is not None:
            return result
    return None


print(dpll([[1, 2], [-1, 3], [-2, -3], [3]]))
# → {3: True, 2: False, 1: True}

One subtlety: pure-literal elimination must re-skip already-satisfied clauses, because a variable that looks pure across all clauses might appear in both polarities once you ignore satisfied ones — or vice versa. Forgetting this gives wrong "pure" verdicts and, occasionally, an incorrect UNSAT.

Variants worth knowing

CDCL — Conflict-Driven Clause Learning. The most important descendant. On every conflict it builds an implication graph, cuts it at the first unique implication point, and learns a clause that forbids the exact combination that caused the dead end. It then backjumps non-chronologically — possibly many decision levels at once. Every solver that wins the annual SAT Competition is CDCL.

Two-watched-literals. Not a different algorithm, but the data-structure trick that makes propagation fast. Each clause "watches" two of its literals; you only re-examine a clause when one of its watched literals becomes false. Backtracking needs no cleanup of watch lists, which is the real win. Introduced in Chaff (2001), standard everywhere since.

VSIDS decision heuristic. Variable State Independent Decaying Sum. Each variable has a score bumped whenever it appears in a learned clause; scores decay over time. The solver always branches on the highest-scoring unassigned variable, so it focuses on the part of the formula currently generating conflicts.

Restarts and clause deletion. CDCL periodically throws away its decisions (keeping learned clauses) and restarts from the top, escaping unlucky early choices. It also deletes low-activity learned clauses to keep memory bounded — Glucose's LBD (literal block distance) metric decides which to keep.

Look-ahead solvers (e.g. march, kcnfs). Spend much more effort per decision — probing each candidate variable with trial propagation to measure its impact — then pick the most constraining branch. Slower per node but powerful on hard random and crafted instances where CDCL's learning gains little.

Common bugs and edge cases

• The empty clause means UNSAT, the empty formula means SAT. A clause with no literals can never be satisfied (conflict); a formula with no clauses is trivially satisfied. Mishandling these base cases is the classic off-by-one of SAT solvers.
• Not reaching a propagation fixpoint. One unit assignment can create another unit clause. You must loop propagation until nothing changes, not do a single pass — otherwise you branch on a variable that was already forced and explore impossible subtrees.
• Pure-literal rule applied to the whole formula instead of the simplified one. A literal is only "pure" relative to the currently unsatisfied clauses. Counting polarities over already-satisfied clauses produces false purity and can flip a SAT result to UNSAT.
• Tautological clauses. A clause containing both x and ¬x is always true and should be dropped at parse time; leaving it in wastes propagation work and confuses pure-literal counting.
• Copy-on-recurse memory blow-up. The teaching implementations above copy the whole assignment per call. On a formula with 10⁵ variables that is gigabytes of garbage. Real solvers use a single mutable trail with push/pop.
• Assuming "UNSAT" is fast. Pigeonhole and parity instances are small but provably force exponential search in any DPLL/resolution solver. A 5-line CNF can run forever; instance size is no guide to difficulty.