# What is CDCL?

> CDCL is how modern SAT solvers work: unit propagation, learning a clause from each conflict, backjumping and restarts. Explained without the jargon.

**CDCL (conflict-driven clause learning)**: Conflict-driven clause learning is the algorithm behind modern SAT solvers: when a partial assignment leads to a contradiction, the solver analyzes why, adds a new clause that rules the cause out, and jumps back.

**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

1. **Decide**: pick an unassigned variable (by an activity score) and give it a value.
2. **Propagate**: any clause with one unassigned literal left forces that literal (unit propagation), found quickly with two watched literals per clause.
3. 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.
4. 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](https://cracked.guide/guide/knuth-w124-0) 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](https://cracked.guide/glossary/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.

---

Source: https://cracked.guide/glossary/cdcl
cracked.guide: A free, dated 145-week path to getting genuinely cracked at programming.