How CDCL Works — and How to Measure Without Fooling Yourself

What a SAT solver is asked

A formula in conjunctive normal form is a list of clauses; a clause is a list of literals, each a variable or its negation. The formula is satisfied if every clause has at least one true literal. The question is whether such an assignment exists.

One rule does almost all of the work in practice: unit propagation. If all literals of a clause but one are false, the last one must be true. Setting one variable can force another, which forces a third — a chain reaction that costs nothing to follow.

DPLL: guess, propagate, undo

The classic procedure (Davis–Putnam–Logemann–Loveland, 1962) repeats three steps: pick an unassigned variable and guess a value, propagate, and if some clause ends up with all literals false — a conflict — undo the most recent guess and try the other value. That last step, undoing only the latest guess, is called chronological backtracking.

Its weakness: the reason for a conflict often lies several guesses back. DPLL does not know that, so it rediscovers the same conflict in every branch below the guess that actually caused it.

CDCL: learn from every conflict

Conflict-driven clause learning keeps DPLL's loop and adds a memory. Its building blocks:

1 · The implication graph. Every propagated literal remembers the clause that forced it — its reason. When a conflict occurs, these reasons form a graph back to the guesses responsible.

2 · Conflict analysis (1UIP). Start from the conflicting clause and repeatedly resolve it with the reason of its most recently assigned literal. Resolution merges two clauses that disagree on one variable into a clause implied by both — so the result follows from the formula and is safe to add. Stop as soon as only one literal from the current decision level remains: the first unique implication point. The clause found is the learned clause.

3 · Non-chronological backjumping. Jump back to the second-highest decision level among the learned clause's literals. There the learned clause has exactly one unassigned literal, so propagation immediately forces the other way. Guesses that had nothing to do with the conflict are skipped.

4 · VSIDS. Variables that appear in recent conflicts get their score raised; all scores decay over time. The solver guesses on the highest score — it keeps working where the conflicts are.

5 · Restarts, phase saving, clause deletion. Occasionally throw away all guesses but keep learned clauses and scores (restart); when re-guessing a variable, reuse its last value (phase saving); regularly delete learned clauses that look useless, judged by how many decision levels they span (LBD).

6 · Watched literals. Each clause watches two of its literals and is only looked at when one of those becomes false. That makes propagation cheap enough to run millions of times per second.

One run, step by step

A small unsatisfiable formula with 5 variables and 10 clauses. The solver below guesses the lowest unassigned variable and tries false first. The run was produced by a traced solver (lehrseite/mini_cdcl.py) that agrees with brute force on 3,000 random formulas.

The analysis at step 7. Three guesses have been made; at level 3, propagation forced two literals, and clause c3 became false. Resolving backwards through the reasons:

start with the conflict clause           (x3 ∨ x4 ∨ ¬x5)
resolve on x5 with its reason c2 (x3 ∨ x5)      →  (x3 ∨ x4)
resolve on x4 with its reason c1 (x3 ∨ ¬x4)     →  (x3)
only one literal of the current level is left: that is the 1UIP clause

The learned clause is (x3) — a single literal. None of the first two guesses played a role, so the solver jumps from level 3 straight to level 0 and sets x3 permanently. At level 0, propagation alone now runs into a conflict: the formula is unsatisfiable, proven with one learned clause. DPLL, undoing one guess at a time, would have revisited the guesses at levels 2 and 1 first.

What each building block buys — measured

From the ablation in this project: the in-house CDCL solver with individual components switched off, on 150 unsatisfiable random 3-SAT instances each at the threshold. Median conflicts per instance (median over 21 seeds; for the backtracking variant, 41).

On these instances phase saving buys nothing and restarts little. Learning and adaptive branching each buy roughly a factor of 4 at n = 100 and 7–9 at n = 130; removing both costs a factor of about 80. The two are largely redundant — either one recovers most of the benefit. On industrial instances the picture differs; this is one family, two sizes.

Null measurements: how a number looks when nothing is there

Every measurement mixes signal with the effects of noise, selection and the measuring procedure itself. A null measurement runs the complete pipeline on a case where the true effect is known to be zero, and shows how large an “effect” the pipeline produces on its own. Only what clearly exceeds that is a finding.

The rules below each stopped a concrete wrong result in this project.

In everyday programming

None of this needs statistics software. It needs a habit.

1 · Before believing a speed-up: measure A against A

Run the old code against itself with the same harness. The spread you see is what “no change” looks like. A new version counts as faster only if it lands clearly outside that spread. Interleave the runs (old, new, old, new) so that background load hits both equally, and use medians.

import statistics, time

def runtime(f, x):
    t = time.perf_counter(); f(x); return time.perf_counter() - t

def ratios(old, new, inputs, rounds=15):
    """Per input: median(new) / median(old), measured interleaved."""
    out = []
    for x in inputs:
        a, b = [], []
        for _ in range(rounds):
            a.append(runtime(old, x))
            b.append(runtime(new, x))          # interleaved, not all old runs first
        out.append(statistics.median(b) / statistics.median(a))
    return out

null = ratios(sort, sort, inputs)          # A against A: no real difference
real = ratios(sort, sort_new, inputs)      # A against B
print("'effect' produced by noise alone:", min(null), "to", max(null))
print("measured effect:", statistics.median(real))

2 · An answer must not depend on names

Shuffle ids, reorder inputs, rename keys — anything that should not matter. If the result changes, it is a bug. If the runtime changes a lot, your benchmark measures tie-breaking and hash order, not your algorithm.

import random

def test_answer_does_not_depend_on_names(algo, graph, trials=50):
    expected = algo(graph)
    for _ in range(trials):
        new = list(graph.nodes); random.shuffle(new)
        renamed = graph.rename(dict(zip(graph.nodes, new)))
        # holds for results that contain no names themselves (count, length, yes/no);
        # otherwise translate the result back first
        assert algo(renamed) == expected
        # and if the RUNTIME varies a lot: the benchmark measures tie-breaking,
        # not the input -- know this before benchmarking

3 · Positive controls: can the code find what is known to be there?

Test against brute force on small inputs, and against inputs with a planted answer. A test suite that only ever checks “no exception” is a probe without a positive control.

# positive control 1: against brute force on small inputs
for _ in range(10_000):
    x = small_random_input()
    assert fast(x) == brute_force(x), x

# positive control 2: an input with a known, planted answer
x, answer = input_with_planted_solution()
assert fast(x) == answer

4 · Ablation instead of guessing which part helps

When an optimisation consists of several ideas, put each behind a switch. First check that all switches on reproduce the old behaviour exactly. Then turn off one at a time. You will regularly find that one idea carries everything and another does nothing — or that two are redundant, as learning and VSIDS are above.

from dataclasses import dataclass, replace

@dataclass(frozen=True)
class Switches:
    cache: bool = True
    early_exit: bool = True
    heuristic: bool = True

def algo(x, s=Switches()):
    ...

# 1. default switches must reproduce the old behaviour exactly (else you measure the refactor)
assert all(algo(x) == algo_before(x) for x in test_cases)

# 2. remove one building block at a time and measure against the full version
for name in ("cache", "early_exit", "heuristic"):
    without = replace(Switches(), **{name: False})
    print(name, statistics.median(ratios(algo, lambda x: algo(x, without), inputs)))

5 · Regression to the mean in performance work

“My change helped the slowest benchmarks most” is what you see even without a change: the cases that were slowest in one measurement are, on average, less slow in the next. Re-run the unchanged code and look at the same plot before drawing that conclusion.

6 · The best of fifty settings is optimistic

Tuning a parameter on one benchmark set and reporting the best value overstates the gain, because the maximum of noisy numbers is biased upwards. Choose on one set, report on another.