CDCL

also: clause learning, backjumping

Conflict-driven clause learning: DPLL plus the observation that a conflict is a proof that some set of decisions is impossible. The solver analyses the implication graph, derives a new clause ruling that set out, adds it to the database, and backjumps possibly many levels at once rather than undoing one decision at a time.

A conflict is not just a dead end, it is a proof that some set of decisions cannot be extended. CDCL records that proof as a new clause, adds it to the database, and jumps back to the level where the new clause becomes informative rather than to the previous decision.

Three changes to DPLL, all following from that:

What each one buys.

learned clause    conflict analysis derives a clause implied by the formula,
                  so the same conflict cannot recur on any other path
 
backjumping       undo to the second-highest level in the learned clause,
                  possibly many levels at once, not one
 
activity heuristic  branch on variables involved in recent conflicts, so the
                  search follows the part of the problem that is actually hard

The learned clauses are logical consequences, so adding them preserves the answer and can only prune. They are also where the memory goes, which is why solvers periodically delete the ones whose measured usefulness is low.

The theoretical content is that CDCL with restarts polynomially simulates general resolution, while plain DPLL corresponds to tree-like resolution, which is exponentially weaker. The speedup is a change in proof system, not a better-tuned search.