Fix the three definitions before you write anything: a literal is a nonzero i32 (+v/-v), a clause is an OR (Vec<i32>), a formula is an AND (Vec<Vec<i32>>). The two edge cases fall straight out of the logic — an empty clause is a disjunction of nothing, hence false; the empty formula is a conjunction of nothing, hence true — and evaluate must honour both.
Parse token-by-token, not line-by-line: whitespace (spaces, tabs, newlines) is the only separator, so a clause can wrap lines or share one. Track a single Option<(num_vars, num_clauses)> header and a current: Vec<i32> you flush into clauses each time you hit a 0. Every malformed input in the lesson — no/duplicate header, data before header, non-integer token, out-of-range literal, unterminated final clause, wrong clause count — must return Err(String), so check each condition explicitly.
In evaluate, a clause holds iff clause.iter().any(...) where a literal is true when if lit > 0 { assignment[(lit.unsigned_abs()-1) as usize] } else { !assignment[...] }, and the formula holds iff clauses.iter().all(...). Flush current with std::mem::take(&mut current) on each 0; after the loop, a non-empty current means "unterminated final clause" and clauses.len() != num_clauses is the count mismatch. assert! the assignment covers num_vars so incomplete assignments panic rather than silently mis-evaluate.
The one inference rule is the unit clause rule: if a clause has no true literal and exactly one unassigned literal, that literal is logically forced. Applying it to a fixed point is sound — it only ever assigns forced values — so it never removes a model; two outcomes matter, a clause going all-false (conflict) or reaching a fixed point (some literals forced).
Use an outer loop with a changed flag; each pass scans every clause and classifies it by walking its literals and counting how many are unassigned while watching for a true one. Skip satisfied clauses, force units, and return Conflict the instant a clause has zero unassigned literals and none true. Record forced literals into a Vec<i32> in assignment order and respect pre-assigned variables (never overwrite).
A helper literal_value(lit, assignment) -> Option<bool> = assignment[(lit.unsigned_abs()-1) as usize].map(|v| if lit > 0 { v } else { !v }) keeps the scan clean. Per clause track satisfied, unassigned: usize, and the last unassigned unit: Option<i32>; then match unassigned { 0 => return Propagation::Conflict, 1 => { assign unit true, forced.push(unit), changed = true } _ => {} }. When a full pass sets nothing, return Propagation::Implied(forced) — that is why a second call yields Implied(vec![]).
DPLL = inference plus a two-way guess with backtracking (Algorithm 7.2.2.2D). It is complete because unit propagation preserves the model set and each branch tries both truth values of the chosen variable, so None means genuinely UNSAT; termination holds because every branch fixes one more variable.
Write a recursive kernel that first snapshotsassignment.clone(), then unit_propagate; on Conflict restore the snapshot and return false. On a fixed point, find the first unsatisfied clause's first unassigned literal to branch on — if none exists, every clause is satisfied, so return true. The snapshot is the crux of backtracking: it undoes not just the guess but everything propagation forced after it (lesson §5, D7).
Branch as: assignment[var-1] = Some(lit > 0); if dpll(...) { return true }; then *assignment = snapshot.clone(); assignment[var-1] = Some(lit < 0); if dpll(...) { return true }; else restore and return false. solve seeds vec![None; num_vars], calls the kernel, and maps leftover None to false. For the formula families, pigeonhole_cnf adds an at-least-one clause per pigeon plus (¬x[p][h] ∨ ¬x[q][h]) per hole-and-pair; waerden_cnf adds (0..j).map(|t| -((a+t*d) as i32)) for every red AP and the positive version for every blue k-AP, breaking the a loop once a+(len-1)*d > n.
Every encoding is built from cardinality constraints on literals. "At most one" in the pairwise (binomial) encoding is one clause (¬ℓi ∨ ¬ℓj) per pair — C(n,2) clauses, zero new variables — and adding the single at-least-one clause gives exactly-one. Always validate a decoded solution against the problem's own rules, never against a fixed model.
exactly_one(vars) returns vec![vars.to_vec()] (at least one) followed by every pairwise (¬a ∨ ¬b); on the empty slice it yields the single empty clause, correctly UNSAT. Index a grid with a closure like |r, c| (r*n + c + 1) as i32; a decoder just finds the first true variable in each row/vertex block.
For queens_cnf(n): exactly-one per row, at-most-one per column, and at-most-one per diagonal — squares (r1,c1),(r2,c2) with r1 < r2 attack diagonally iff |c1 - c2| == r2 - r1, so emit (¬var(r1,c1) ∨ ¬var(r2,c1±(r2-r1))) when the target column is in range. For coloring_cnf, exactly-one colour per vertex plus (¬x[u][c] ∨ ¬x[w][c]) for every edge (u,w) and colour c. Decoders: (0..n).find(|&c| model[block*width + c]).expect(...).