Glossary
What is CDCL?
CDCL, conflict-driven clause learning, is the core algorithm of nearly every competitive SAT solver. It guesses values for variables, propagates the consequences, and when it hits a contradiction it works out a short reason, records that reason as a new learned clause, and backjumps to the decision that caused it.
The loop
- Decide: pick an unassigned variable (by an activity score) and give it a value.
- Propagate: any clause with one unassigned literal left forces that literal (unit propagation), found quickly with two watched literals per clause.
- On a conflict, analyze the implication graph back to a cut, learn the clause that forbids that combination, and jump back to the level where the learned clause becomes unit.
- Every so often restart and forget some learned clauses so the clause database stays manageable.
Learning is what makes it powerful: the solver never makes the same mistake twice.
Where it is taught
Knuth builds it up across §7.2.2.2 in Volume 4B: first simple backtracking solvers, then lookahead, then Algorithm C, a full CDCL solver with a trail, watched literals, activity scores, purging and restarts. The section ends the path. See also WalkSAT, the local search alternative.
Questions
Who invented CDCL?
Clause learning came from the GRASP solver (Marques-Silva and Sakallah, 1996); Chaff (2001) added watched literals and activity-based decisions that made it fast.