Walkthrough — Module 14: Conflict-Driven Clause Learning
Read this AFTER a stage is green — it explains how the reference solution is built and why.
Stage 1: Lazy data structures: two watched literals
propagate is the heart, and its structure is chosen so backtracking costs nothing. For each newly-false literal np = -p it does std::mem::take(&mut self.watches[code(np)]) — moving the whole list out so it can push replacement watches into other lists without borrow conflicts — then rebuilds kept for the clauses that still watch np. Each clause is normalized so np sits in slot 1 (swap(0,1) if needed), and the four cases are tried in order: satisfied by slot 0 (keep), a non-false literal in slots 2.. (move the watch, don't keep), slot 0 unassigned (unit: force it), slot 0 false (conflict). The conflict path is careful to splice the unprocessed tail ws[i..] back into the list before returning, so no clause silently loses its watcher — a subtle correctness point a naive rewrite usually drops.
The reason the invariant makes backtracking free is realized in unassign, which is a one-liner: self.values[var-1] = None, with an assertion that the queue is empty. It touches no watch list at all. This works only because callers unassign in strict LIFO order (a trail suffix); the lesson proves that turning false literals back to unassigned, newest-first, cannot violate the invariant. add_clause deserves a look too: it moves up to two non-false literals into slots 0/1 and then classifies the arrival (dead-on-arrival conflict, immediately-unit, or fine), which is exactly what lets a learned clause assert its literal the moment it is installed after a backjump. check_watch_invariant implements both the structural check (each length-≥2 clause in exactly its two slot lists) and the semantic one, and is worth running in your own debugging — it catches almost every propagation bug.
Stage 2: The trail: decisions, levels, reasons
The representation is three parallel arrays doing one job: lits is the assignment order, level_start marks where each decision level begins (so decision_level() is just level_start.len() - 1), and info[v-1] holds (level, reason) while variable v is assigned. Keeping the reason in the trail rather than in a separate implication-graph structure is the key economy — the trail and its reasons together are the implication graph, which is all stage 3 needs to walk backward. push centralizes the "not already assigned" assertion and stamps the current level, so decide (open a level, then push with None) and enqueue (push at the current level with a reason) stay tiny.
backjump is the operation the whole design is built around. It computes cut = level_start[level+1], does lits.split_off(cut) to get the popped suffix, reverse()s it to newest-first, clears each popped variable's info, and truncates level_start. Returning the literals newest-first is not a convenience — it is the exact order stage 4 must feed to ClauseDb::unassign for the watch invariant to survive. The early-out if level == decision_level() { return Vec::new() } handles the common "learned clause backjumps to the current level" case without touching anything. assignments_at_level slices between consecutive level_start boundaries (using .get(level+1) to fall back to the trail end for the top level), which is how the tests read off a level's literals in order.
Stage 3: Conflict analysis: learning from failure
The reference never materializes intermediate resolvent clauses; it tracks membership with seen: Vec<bool> and a single counter open of how many current-level literals are still in the resolvent. That is the idiom to steal: resolution "backward along the trail" becomes a scan where the reason clauses are merged in and the trail order tells you which literal to resolve next. Each round merges a reason's literals — skipping the pivot and already-seen variables — classifying each by level: current level bumps open, a lower positive level is pushed straight into learned, and level 0 is dropped because those literals are false in every solution. Then it walks i backward over trail.literals() to the next seen literal, decrements open, and either stops (UIP found) or resolves on that literal's reason.
Correctness hinges on two facts the code relies on implicitly. First, when it walks back to the next seen literal, that literal is guaranteed to be at the current level — lower-level members lie deeper in the trail than every current-level one, and open > 0 on entry — so it never resolves the wrong pivot. Second, the loop must terminate at the decision at the latest: the decision has no reason, but by the time it's reached it is the only current-level literal left (open == 1), so the UIP break fires first. After finding the UIP, learned[0] = -uip (the asserting literal) and a second pass finds the highest level in learned[1..] as the backjump target, swapping a literal of that level into slot 1 — pre-arranging exactly the watch order add_clause wants, so stage 4 can install the clause blindly. brute_force_implies is the soundness oracle: it confirms the learned clause is genuinely entailed, not an artifact.
Stage 4: The complete CDCL solver
solve is a clean transcription of Algorithm C's control flow (steps labeled C1–C8 in the comments) with the three previous stages as black boxes. The initialization cleans each input clause — sort_unstable, dedup, and a binary_search(&-l) tautology check — because the watch discipline assumes distinct variables per clause; skipping tautologies is safe (they're true everywhere) and merging duplicates is necessary. The loop then alternates: propagate, drain take_implications onto the trail, and branch on conflict-or-not. On conflict at level 0 it returns None (UNSAT); otherwise analyze, bump activities, backjump (saving phases as it unassigns newest-first), and add_clause(learned) — whose asserting property means the next propagate immediately continues from the forced literal.
The decision heuristic is deliberately documented in-code (the tests require it) and kept deterministic: integer VSIDS with activity bumped per learned-clause literal, a halving decay every 128 conflicts so recent conflicts dominate, and max_by_key(|&v| (activity[v], Reverse(v))) to pick the most active unassigned variable with a stable tie-break, assigned at its saved phase. The completeness argument is quietly encoded in C7: if no variable is unassigned and propagation found no conflict, every clause must be satisfied (watched propagation never misses a falsified clause), so the collected values are a model. The two generators are the payoff: pigeonhole_cnf builds Haken's provably-exponential family (so CDCL cannot make it easy, and the tests confirm UNSAT on PHP(5,4) and PHP(6,5)), while waerden_cnf reproduces Knuth's running example with W(3,3) = 9 as the SAT/UNSAT boundary.