CDCL: Conflict-Driven Clause Learning

Recall how unit propagation works: every decision at a given level ripples through the formula, forcing other variables. In the padlock example, the cascade was benign — it found the solution. But consider a harder formula where the cascade ends in two clauses that both become empty simultaneously. That is a conflict.

DPLL’s answer: shrug, undo B=True, try B=False. But that ignores the real cause. CDCL’s answer: build an implication graph and read the cause directly from its structure.

The implication graph makes visible something that plain backtracking ignores: the causal structure of a conflict. Not every node in the graph contributed to the conflict — only those that have a path to the conflict node. CDCL exploits this to learn something precise.

What to learn from a conflict. The conflict happened because a set of assignments jointly falsified some clause. If we could add a new clause to the formula that prevents exactly that combination of assignments, future search will never walk into the same dead end. This new clause is called the learned clause (or conflict clause).

How do we extract it? By drawing a cut across the implication graph that separates the decision nodes (reason side) from the conflict node (conflict side). Every edge crossing the cut corresponds to a literal whose assignment contributed to the conflict. The negations of those literals form the learned clause.

Among all possible cuts, CDCL modern solvers universally use the first-UIP cut. Understanding why requires the concept of a Unique Implication Point (UIP).

Intuitively, the first UIP is the “bottleneck” through which all blame at the current level flows. Cutting just below the first UIP gives the tightest, most compact learned clause — and guarantees the clause will be asserting: at the backjump level, exactly one literal in the learned clause is unset, making it immediately unit-propagate. ^{[GRASP: A Search Algorithm for Propositional Satisfiability]}

Once we have the learned clause, we know exactly how far back to jump. The asserting level is the second-highest decision level among the literals in the learned clause — the highest level at which all but the UIP literal are already determined (to False). At that level, the UIP literal is immediately forced by unit propagation.

This is the mechanism that makes CDCL vastly superior to DPLL on industrial instances. ^{[Chaff: Engineering an Efficient SAT Solver]}

Putting all four pieces together gives the CDCL algorithm that runs inside every modern SAT solver — including CP-SAT’s Boolean layer.

flowchart TD
  A([Start: CNF + empty assignment]) --> B[Unit Propagation]
  B --> C{Conflict?}
  C -- No --> D{All vars assigned?}
  D -- Yes --> SAT([Return SAT])
  D -- No --> E[Pick variable, branch
VSIDS heuristic]
  E --> B
  C -- Yes --> F{At decision
level 0?}
  F -- Yes --> UNSAT([Return UNSAT])
  F -- No --> G[Conflict analysis:
build implication graph]
  G --> H[Derive first-UIP
learned clause]
  H --> I[Add learned clause
to formula]
  I --> J[Backjump to
asserting level]
  J --> B

VSIDS (Variable State Independent Decaying Sum) deserves a brief mention. Each variable has an activity score that is bumped every time it appears in a conflict. When CDCL needs to branch, it picks the highest-activity unassigned variable. Activity decays geometrically over time, so the solver naturally focuses on variables involved in recent conflicts — the ones most likely to be entangled in the current hard region of the search space. ^{[Chaff: Engineering an Efficient SAT Solver]}