A backtracking SAT solver can spend years, in machine time, being politely wrong.

It chooses a variable, propagates the consequences, chooses again, propagates again, and eventually walks into a contradiction. The naive move is to undo the last choice and try the other branch. That is honest, but forgetful. It treats the contradiction as a local inconvenience rather than evidence.

Conflict-driven clause learning, or CDCL, changed the status of failure. A conflict became a proof object in miniature: the solver records why each forced assignment happened, resolves those reasons backward from the contradiction, learns a new clause, and jumps to the earliest level where that clause can immediately propagate.12

The useful sentence is:

do not merely retreat from a bad branch; explain why the branch was bad

That explanation is just another clause. Once learned, it joins the formula and prevents the solver from reconstructing the same doomed partial assignment.

The Trail Is A Stack Of Reasons

The Davis-Putnam-Logemann-Loveland procedure gave the classic recursive shape: simplify by unit propagation, split on a literal, and backtrack when a branch cannot satisfy the formula.3 CDCL keeps that shape but annotates it.

Every assigned literal on the trail has one of two origins:

decision:  the solver guessed it at a new level
implied:   a clause became unit and forced it

For an implied literal, the solver stores the clause that forced it. If

(~a OR x)

forces x after a is true, that binary clause is the reason for x. In graph language, the falsified literal ~a points toward the forced literal x.

Keep doing this and the trail becomes more than a stack. It is an implication graph whose edges are clauses. When a clause finally becomes false, the graph contains the evidence needed to explain the falsehood.

The important part is not mystical. It is resolution:

(A OR  p)    reason for p
(B OR ~p)    current conflict clause mentions ~p
-----------------------------------------------
(A OR B)     p has been explained away

The pivot variable disappears. The new clause is still a logical consequence of the original formula. Repeat this on current-level implied literals and the conflict clause becomes less like a symptom and more like a diagnosis.

The First Gate Back To The Decision

A decision level can contain many implications. In the implication graph, every path from the current decision to the final conflict must pass through certain cut points called unique implication points, or UIPs. The first-UIP learning scheme stops resolution at the first such gate when walking backward from the conflict. Operationally, it is simple:

start with the falsified conflict clause
while the clause contains more than one literal from the current decision level:
    choose the latest assigned current-level literal that has a reason
    resolve it with its reason clause
learn the remaining clause

When only one current-level literal remains, the clause is assertive. That means after the solver backjumps to the second-highest decision level appearing in the learned clause, all other literals in the learned clause are already false, and the remaining literal becomes unit.

The solver does not just go back. It lands somewhere where the new clause has a job to do.

This is why first-UIP clauses are so convenient in practice. They are local enough to derive cheaply, but sharp enough to force a different continuation. The SAT Handbook’s CDCL chapter describes first-UIP as the dominant conflict analysis scheme in modern CDCL solvers; MiniSat’s system descriptions then show how much subsequent engineering went into making those learned clauses smaller and cheaper to keep.24

Lab: Make The Failure Explain Itself

The lab below builds a small formula with a deliberate conflict. The formula has two real support decisions, then a configurable number of irrelevant detour decision levels, then one final bad decision.

The final conflict depends on x, y, and c, but not on the detours:

a -> x
b -> y
c -> z
c -> w
x and z -> p1
y and p1 -> p2
...
last p and w -> conflict

The simulator runs actual unit propagation over the generated clauses. Then it performs first-UIP-style resolution over the recorded reason clauses. In the default case it learns:

(~x OR ~y OR ~c)

Since x and y were caused by earlier decisions, this clause tells the solver to jump back before the detours and force ~c. The detour decisions were real levels on the trail. The learned clause simply proves they were irrelevant to this failure.

decision implied support detour asserting literal

The Resolution step slider is intentionally a little strange: it lets you pause the proof, not the search. Step 0 is the raw conflict clause. Each later row resolves one recently implied current-level variable with the clause that forced it. When the ledger says 1 current, the learned clause has become assertive.

Push Detour levels upward. The trail grows, but the learned clause does not. The backjump skips exactly those irrelevant levels because the final clause has no literal from them. Push Implication chain upward and the proof gets longer; more current-level implications must be explained away before the same small learned clause appears.

This is not a benchmark. It is a glass-box instance whose point is auditability. The JavaScript lab exports a 2,987-check verifier over all 30 generated formulas in the slider grid:

6 chain lengths * 5 detour counts

For every case, it checks that each implied assignment was forced by a unit reason at the moment it entered the trail, every resolution row uses opposite pivot literals and equals the computed resolvent, the learned clause is exactly (~x OR ~y OR ~c), and after the computed backjump the clause is unit and asserts ~c. That is the contract conflict analysis must satisfy. Without it, a learned clause is just a story.

Why The Learned Clause Is Allowed

The learned clause is not a heuristic memo. It is an implicate of the original formula.

Every resolution step combines clauses that are already known consequences: original reason clauses plus the current conflict clause or its resolvents. Resolution preserves entailment. So adding the final clause cannot remove a valid satisfying assignment. It only removes assignments that were impossible anyway.

That distinction matters because CDCL solvers learn enormous numbers of clauses. If learning were merely a cache of observed bad branches, correctness would be fragile. Instead, the learned database is a growing proof trace. Modern SAT solving is search mixed with proof construction.

The backjump level follows from the same clause. Suppose the learned clause is

(~x OR ~y OR ~c)

and the current trail has x true at level 1, y true at level 2, and c true at level 5. Backjump to level 2. Then ~x and ~y are false, while c is unassigned. The clause becomes unit and forces ~c. Levels 3 and 4 were not chronologically undone because they were the last choices. They were undone because the proof no longer mentions them.

This is nonchronological backtracking in one line:

return to the highest remaining reason, not to yesterday's decision

The Machinery Around The Idea

The tiny algorithm above is not a modern solver by itself.

Chaff’s leap was not only learning. It paired clause learning with extremely efficient Boolean constraint propagation, two watched literals, and low-overhead branching machinery.5 MiniSat later became a reference implementation because it made a compact CDCL architecture easy to study and modify, including learned-clause minimization.4

Production solvers also need restarts, variable activity scores, phase saving, clause deletion, preprocessing, inprocessing, proof logging, and careful memory layout. Those systems-level choices decide whether the beautiful little clause above arrives fast enough to matter.

But the heart is still visible in the lab:

propagation creates reasons
reasons create a conflict graph
resolution creates a learned clause
the learned clause chooses the backjump
the backjump makes the clause assert

SAT is NP-complete, so no clever clause makes the worst case disappear. The surprise is that many industrial instances are full of repeated structure. CDCL survives by turning local mistakes into reusable lemmas. A branch fails once, then the formula remembers.

The most useful mental model for CDCL is not “try things faster.” It is “debug the search as it runs.”

The trail is the stack trace. Reason clauses are stack frames. The conflict is the thrown exception. First-UIP analysis walks backward until it finds the smallest current-level explanation that can force a different future.

That is a strong software-engineering idea hiding inside a theorem-proving algorithm:

when a system fails, keep the weakest explanation that prevents repetition

Too weak, and the solver revisits the same contradiction through another door. Too strong, and the learned clause is bloated, expensive to propagate, and likely to be deleted. The first-UIP clause is a practical compromise: local, assertive, and usually small enough to be useful.

Failure is only waste if the solver leaves without a note.

CDCL writes the note as a clause.

  1. Joao P. Marques-Silva and Karem A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability”, IEEE Transactions on Computers, 1999. ↩

  2. Joao Marques-Silva, Ines Lynce, and Sharad Malik, “Conflict-Driven Clause Learning SAT Solvers”, in Handbook of Satisfiability, 2009. ↩ ↩2

  3. Martin Davis, George Logemann, and Donald Loveland, “A Machine Program for Theorem-Proving”, Communications of the ACM, 1962. ↩

  4. Niklas Een and Niklas Sorensson, “MiniSat v1.13 - A SAT Solver with Conflict-Clause Minimization”, SAT Competition 2005 system description. ↩ ↩2

  5. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik, “Chaff: Engineering an Efficient SAT Solver”, DAC 2001. ↩