Walkthrough — Module 10: Satisfiability

Read this AFTER a stage is green — it explains how the reference solution is built and why.

Stage 1: Conjunctive normal form and DIMACS

The representation is deliberately minimal: Cnf { num_vars: usize, clauses: Vec<Vec<i32>> }, with literals as nonzero i32 in DIMACS convention. The doc note points out this is a trivial re-coding of Knuth's internal 2k + sign literal scheme — the course keeps the human-readable ±v form because the parser and every test speak DIMACS. parse_dimacs is a single pass over input.lines(): blank/c lines are skipped, a p line fills a header: Option<(usize, usize)> (rejecting a second one), and every other line is split on whitespace and parsed token-by-token. The key idiom is std::mem::take(&mut current) to flush the accumulating clause into clauses on each 0 while leaving a fresh empty Vec behind — that is what makes a bare 0 produce a legal empty clause for free, and what lets clauses span or share lines. Errors are all caught in one place: the parse checks range with lit.unsigned_abs() as usize > num_vars, and the post-loop tail rejects an unterminated clause (!current.is_empty()) and a count mismatch (clauses.len() != num_clauses).

The invariant that makes it correct is that the header is authoritative: nothing is accepted before it, no literal may exceed its num_vars, and the final count must match — so the round trip parse_dimacs(&c.to_dimacs()) == Ok(c) is lossless by construction. evaluate encodes the two logical edge cases structurally rather than by special-casing them: clauses.iter().all(|c| c.iter().any(|&lit| ...)) makes the empty clause false (an empty any is false) and the empty formula true (an empty all is true) with no extra code. The assert!(assignment.len() >= num_vars) is not defensive noise — it enforces that evaluate only ever sees a complete assignment, which is precisely the contract that separates it from stage 2's partial Vec<Option<bool>>. A naive parser that reads line-by-line would break on clauses that wrap lines; this one never even notices line boundaries.

Stage 2: Unit propagation

unit_propagate(cnf, assignment: &mut Vec<Option<bool>>) -> Propagation is the inference engine, and its shape mirrors Knuth's fixed-point reasoning directly: an outer loop with a changed flag, an inner scan of every clause. Each clause is classified in one walk of its literals via the literal_value helper (assignment[idx].map(|v| if lit > 0 { v } else { !v })), tracking three facts — is any literal true (satisfied, short-circuit break), how many are unassigned, and which one was the last unassigned (unit). The decision then reduces to match unassigned { 0 => Conflict, 1 => force it, _ => nothing }. Forcing means writing Some(lit > 0) into the slot and pushing lit onto forced; setting changed = true guarantees another full pass, because that assignment may have turned some other clause into a unit. When a whole pass changes nothing, the fixed point is reached and it returns Implied(forced).

Two design choices carry the correctness. First, Conflict is returned the instant a clause has zero unassigned literals and none true — the caller (DPLL) is told the branch is dead immediately, and the literals forced before the conflict remain in assignment on purpose, because the Propagation doc spells out that callers who need to undo them snapshot first. Second, the loop respects pre-assigned variables (it only ever writes None slots) and records forced in assignment order, which is what makes idempotence hold: at a fixed point every clause is satisfied or has ≥2 unassigned literals, so a re-run forces nothing and yields Implied(vec![]). The Propagation enum is matched by value in the tests, so returning the exact variants matters. The honest tradeoff, stated in the doc comment: this repeated-scan approach is quadratic where Knuth's Algorithm D uses two watched literals to touch only clauses that could change status — correct and clear at lab scale, not competition-fast.

Stage 3: A DPLL solver

solve is a thin wrapper: seed assignment = vec![None; num_vars] (step D1), call the recursive dpll kernel, and on success map every leftover None to false (any completion works because every clause already holds a true literal). The kernel dpll(cnf, assignment) -> bool is where Algorithm 7.2.2.2D lives, and the step labels are in the code: let snapshot = assignment.clone() captures the state on entry; unit_propagate is D3/D6, and on == Propagation::Conflict it restores snapshot and returns false (D7). If propagation survives, it scans for the first unsatisfied clause and takes its first unassigned literal as the branch variable — if no such clause exists (branch stays None), every clause is satisfied and it returns true (D2, success). The one idiom worth stealing is the 'clauses: labelled loop with continue 'clauses to skip a clause the moment a true literal is seen, so candidate only ever holds a genuinely unassigned literal from a genuinely unsatisfied clause.

The subtle bug this structure avoids is under-backtracking. The two-way branch (D4) sets assignment[var-1] = Some(lit > 0) and recurses; on failure it does *assignment = snapshot.clone() before trying Some(lit < 0), and on double failure restores snapshot and returns false (D8). Because the snapshot predates propagation, restoring it undoes not just the guess but every literal propagation forced after the guess — the exact point the lesson's §5 trace hammers on (you must undo x2, x3, not just x1). A version that unassigned only the branch variable would leave stale forced literals behind and report wrong answers. Completeness follows because unit propagation only assigns forced values (preserving the model set) and each node tries both polarities; termination because each branch fixes one more variable. solve_brute is the deliberate cross-check — it counts 0..2^num_vars, treating variable 1 as the least-significant bit, and returns the first assignment evaluate accepts, capped by assert!(num_vars <= 25). The formula builders are direct transcriptions: pigeonhole_cnf uses var = |p, h| p*holes + h + 1 with an at-least-one clause per pigeon and (¬x[p][h] ∨ ¬x[q][h]) per hole and pair p < q; waerden_cnf emits a negative-literal clause for each j-term red AP and a positive one for each k-term blue AP, using if a + (len-1)*d > n { break } to stop the a loop early. The tests confirm PHP(4,3) UNSAT, waerden(3,3;8) SAT and (3,3;9) UNSAT — with solve and solve_brute agreeing.

Stage 4: Encoding problems into SAT

Everything here is assembled from one primitive, exactly_one(vars: &[i32]) -> Vec<Vec<i32>>, which returns the at-least-one clause vars.to_vec() followed by a pairwise (¬vars[i] ∨ ¬vars[j]) for every i < j. This is the binomial encoding: C(n,2) clauses, zero auxiliary variables. The reference notes the tradeoff explicitly — §7.2.2.2's sequential/commander encodings buy O(n) clauses with O(n) new variables — but at lab sizes pairwise wins on clarity. A quietly correct touch: exactly_one(&[]) returns the single empty clause, so "exactly one of nothing" is UNSAT exactly as the logic demands. The recurring idiom is the grid-indexing closure, e.g. var = |r, c| (r*n + c + 1) as i32, which flattens a 2-D problem into contiguous DIMACS variable numbers and is inverted by each decoder.

queens_cnf layers three constraint kinds: exactly_one per row, at-most-one per column, and at-most-one per diagonal. The clever economy is in the comment — with n rows each forced to hold exactly one queen, the columns are forced to hold at most one each, so column and diagonal constraints need only the at-most-one (pairwise) half, not full exactly-one. The diagonal test (r1,c1),(r2,c2) attack iff |c1-c2| == r2-r1 becomes two guarded pushes for c1+d and c1-d when in range. coloring_cnf is exactly_one colour per vertex plus (¬x[u][c] ∨ ¬x[w][c]) for every edge and colour, forbidding equal colours on adjacent vertices. The decoders decode_queens/decode_coloring just find the first true variable in each row/vertex block and .expect(...) a well-formed model. The whole-module discipline the tests enforce is semantic validation: a decoded queens placement is checked for no two queens attacking, a decoded colouring for no monochromatic edge — never compared to a blessed model, because a formula has many equally-correct models and only the problem's own rules are ground truth.