Resolution and CDCL

Symptom

SAT is NP-complete (T027). It is the NP-complete problem, the one everything else reduces to. The textbook conclusion is that you should avoid it.

Meanwhile: a hardware verification team routinely discharges instances with two million variables and ten million clauses in under a minute. Package managers solve dependency resolution with SAT. Every bounded model checker (T049) is a SAT solver with a front end. The planning community abandoned custom search for SAT encodings and got faster.

So either the complexity result is wrong, or it is answering a different question than the one practitioners care about. It is the second, and the gap between them is one of the most useful things to understand about applied complexity theory.

The symptom for you personally: you have an NP-complete subproblem, you assume it is hopeless, and you write a custom heuristic search that is worse than encoding to CNF and calling a solver that thousands of person-years went into.

Statement

Work in conjunctive normal form: a conjunction of clauses, each a disjunction of literals.

Resolution rule. From $(A \vee x)$ and $(B \vee \neg x)$ derive $(A \vee B)$.

Refutation completeness. A CNF formula is unsatisfiable if and only if the empty clause is derivable by resolution.

The pairing is what makes this post a [theorem+empirical]: resolution’s lower bounds say precisely when solvers must fail, and the empirical record says they almost never encounter those cases.

Argument

DPLL, the 1962 baseline. Pick an unassigned variable, guess a value, simplify, recurse; on contradiction, backtrack and try the other value. Two accelerations: unit propagation, where a clause with one unassigned literal forces it, and pure literal elimination. This is chronological backtracking, and it repeats the same mistake in every branch of a subtree.

CDCL adds four things, and their interaction is the result.

1. Clause learning. On conflict, analyze why. Build the implication graph recording which decisions forced which assignments, cut it at the first unique implication point, and derive a new clause capturing the conflict’s cause. That clause is added permanently, so the solver never re-enters that region of the search space by any route. The learned clause is a resolution derivation, and that is the bridge between the theory and the implementation: the solver is constructing a resolution proof, guided by the search rather than blindly.

2. Non-chronological backjumping. With the reason known, jump directly to the decision level that actually caused the conflict rather than undoing one level. Skipping twenty irrelevant levels at once is routine and it discards an entire subtree that DPLL would have enumerated.

3. Watched literals. Unit propagation dominates runtime, historically 80 to 90 percent of it. Rather than checking every clause on every assignment, watch two unassigned literals per clause; a clause can only become unit when one of its two watches is falsified. The data structure requires no work on backtracking at all, which is what makes it dramatically faster than counter-based schemes, and it is arguably the single most important implementation trick in the field.

4. Activity-based branching (VSIDS). Bump a counter for every variable in a learned clause, decay all counters periodically, and always branch on the highest. The effect is to focus on variables involved in recent conflicts, which concentrates the search where the difficulty is. Combined with random restarts that keep learned clauses but discard the assignment trail, this escapes bad early decisions without losing work.

Chaff (2001) put watched literals and VSIDS together and got one to two orders of magnitude over the previous generation, which is the moment SAT became an industrial tool.

Haken’s lower bound, and what it forbids. The pigeonhole formula says $n+1$ pigeons fit into $n$ holes. It is unsatisfiable, obviously and immediately, by an argument a child understands (T001). Resolution requires exponentially many clauses to prove it, because resolution cannot count — it reasons clause by clause, and the pigeonhole fact is global.

Since CDCL is polynomially equivalent to resolution, CDCL cannot solve pigeonhole instances efficiently either, and this is observable: solvers that dispatch two million variables in seconds stall on $\text{PHP}^{12}_{11}$, an instance with 132 variables. A 132-variable formula that defeats a solver handling two million is the cleanest demonstration available that problem size is not the thing that determines difficulty.

The same holds for Tseitin formulas over expander graphs and for random 3-SAT at the satisfiability threshold. The threshold is sharp: at clause-to-variable ratio $m/n \approx 4.267$, random 3-SAT flips from almost surely satisfiable to almost surely unsatisfiable, and instances at the ratio are hard for every known method. Below 4.267 solutions are plentiful and easy to find; above it, unsatisfiability proofs are short. The hardness is a narrow band.

Why industrial instances are easy. They have structure: modularity, small backdoor sets, low treewidth in places, and long chains of implications that propagate rather than requiring decisions. Real formulas encode real systems, and real systems are built compositionally. Random and combinatorial formulas have none of this, which is exactly why benchmark suites include them.

Extended resolution escapes Haken, by allowing new variables defining subformulas, and it proves pigeonhole in polynomial size. Solvers are beginning to exploit related ideas, and DRAT proof logging — now mandatory in the SAT competition — means a solver’s UNSAT answer comes with a machine-checkable certificate rather than a promise.

A worked conflict, because the mechanism is invisible otherwise. Take clauses $(\neg a \vee b)$, $(\neg b \vee c)$, $(\neg b \vee \neg c \vee d)$, and $(\neg d \vee \neg b)$. Suppose the solver decides $a = \text{true}$ at decision level 3.

Unit propagation runs: $a$ forces $b$ from the first clause, $b$ forces $c$ from the second, $b$ and $c$ force $d$ from the third, and now the fourth clause $(\neg d \vee \neg b)$ is falsified — both its literals are false. A conflict at decision level 3.

Conflict analysis resolves backwards from the falsified clause against the reasons for each propagated literal. Resolving $(\neg d \vee \neg b)$ with the reason for $d$, namely $(\neg b \vee \neg c \vee d)$, on the variable $d$, gives $(\neg b \vee \neg c)$. Resolving that with the reason for $c$, which is $(\neg b \vee c)$, on $c$, gives $(\neg b)$. That is a unit clause with a single literal from the current decision level, so it is the first unique implication point and analysis stops.

The solver has learned $(\neg b)$. Note what happened: the learned clause is literally the result of a chain of resolution steps, which is the concrete form of the polynomial-equivalence claim. And it is far stronger than “$a$ was wrong”: it forbids $b$ under every future assignment, by any route, whether or not $a$ is involved. The solver backjumps to level 0 and asserts $\neg b$ permanently. DPLL, by contrast, would have flipped $a$ and been free to rediscover the same conflict through a different variable later.

Forbids

Polynomial-size resolution refutations of the pigeonhole principle. Haken’s bound is unconditional. Any solver limited to resolution inherits it.

CDCL beating resolution asymptotically. The polynomial equivalence closes that door; improving requires a stronger proof system.

A worst-case-efficient SAT solver, unless P = NP.

Trusting an UNSAT answer without a proof. Solvers have bugs, and this was found in competition entries. The field’s response was to require DRAT certificates, which is a model other tool communities could copy.

Does not forbid

It does not mean NP-complete means intractable in practice. This is the misreading that has probably cost more engineering effort than any other in this series. Hardware verification at Intel and AMD, the Linux kernel’s kconfig, Eclipse’s p2, Fedora’s DNF, opam, and Dart’s pub all run SAT solvers on real inputs daily. If your problem reduces to SAT, encoding it and calling MiniSat, CaDiCaL, or Kissat is very often the correct engineering decision.

It does not mean SAT solvers are useless on hard instances. They are used to settle combinatorial questions: the Boolean Pythagorean triples problem was resolved by a SAT solver producing a 200-terabyte proof, later checked by a verified checker, and the Schur number five was determined the same way. A 200 TB proof is an odd artifact and it is a mathematical result.

It does not mean CNF encoding loses too much structure. Cardinality constraints, at-most-one, and pseudo-Boolean constraints have well-studied encodings with known propagation strength. SMT solvers (Z3, CVC5) keep theory structure explicitly and use a SAT solver underneath via DPLL(T), which is the best of both.

It does not mean you should write your own. Twenty years of competition-driven engineering are in the top solvers, and the gap between a competent hand-rolled DPLL and Kissat is several orders of magnitude on real instances.

It does not say the phase transition makes all random instances hard. Only the narrow band at $m/n \approx 4.267$ is. Random instances well away from the ratio are easy in both directions, and this is why “random benchmark” without a stated ratio is a meaningless description.

Boundary

• CNF only. Circuit structure is lost in the Tseitin transformation, which is why circuit-aware solvers and SMT exist.
• Resolution-strength proofs. Anything needing counting or symmetry breaking is exponential without extension. Symmetry-breaking preprocessors help precisely because they add the reasoning resolution lacks.
• Memory grows with learned clauses. Every solver must delete clauses by a usefulness heuristic (LBD is the standard), and deleting the wrong ones costs more than keeping them.
• Incremental solving changes the calculus. Solving a sequence of related formulas while retaining learned clauses, as bounded model checking does, is a different and much better-behaved workload than one-shot solving.
• Parallelism is disappointing. Portfolio approaches running diverse configurations work better than dividing the search space, and the speedups are far from linear.

The lesson to generalize: NP-complete is a statement about the worst case over all inputs, and your inputs are not all inputs. Ask what structure your instances have before assuming the complexity class applies to you.

Read next