Stage 1: Lazy data structures: two watched literals
The watched-literal invariant is the whole idea: each clause of length ≥ 2 watches two literals, and whenever a watched literal becomes false, either the other watch is true or the clause has at most one non-false literal (unit or conflicting). The payoff is that only clauses watching the negation of a just-assigned literal can possibly have changed — and the invariant is stable under LIFO unassignment, so backtracking repairs nothing.
Represent watches as watches[code(l)] = Vec<clause index> with code(+v)=2(v-1), code(-v)=2(v-1)+1. Keep clause watches in slots 0 and 1 and swap literals within the clause as watches move. propagate pulls newly-true literals off a FIFO queue; for each, walk the clauses watching its negation and resolve each by the first applicable case: satisfied / move watch / unit / conflict.
In propagate, for literal p newly true, take the list for code(-p), and for each clause put -p in slot 1 (swap if in slot 0). Then: if value(slot0)==Some(true) keep; else scan slots 2.. for a non-false literal and move the watch there; else if slot0 is None force it (set, log implication, enqueue); else (Some(false)) it's a conflict — restore the list, clear the queue, return Some(c). add_clause moves up to two non-false literals to the front and detects unit/conflict on arrival.
The trail is the implication graph stored as one flat array: every currently-true literal in assignment order, cut into decision levels, each propagated literal remembering its reason clause. Decisions have no reason; level 0 holds consequences of the formula alone. Backjumping must pop a suffix (newest first) so the stage-1 watch invariant survives untouched.
Store lits: Vec<i32>, level_start: Vec<usize> (index where each level begins; current level = level_start.len()-1), and per-variable info: Vec<Option<(level, Option<reason>)>>. decide pushes a new level_start boundary then the literal; enqueue records at the current level; backjump(level) splits off everything above and reverses it.
decide(lit): level_start.push(lits.len()); push(lit, None). enqueue(lit, reason): push(lit, reason). backjump(level): if level == decision_level() return empty; else cut = level_start[level+1], popped = lits.split_off(cut), reverse it, clear each popped variable's info, level_start.truncate(level+1), return popped (newest first — exactly the LIFO order for unassign). assignments_at_level slices lits between consecutive level_start boundaries.
Stage 3: Conflict analysis: learning from failure
First-UIP analysis derives the learned clause by backward resolution along the trail. Maintain a resolvent (start: the conflict clause). While it has more than one literal at the current decision level, resolve away the most recently assigned such literal against its reason clause; stop when exactly one current-level literal remains — that variable is the first UIP, and its negation is the asserting literal.
Don't build clauses explicitly; use a seen: Vec<bool> per variable and an open counter of unresolved current-level literals. Merge a reason's literals: skip the pivot and already-seen; current-level ones bump open, lower-level (but > 0) ones go into learned, level-0 ones are dropped (false forever). Then walk the trail backward to the next seen literal to resolve on.
Loop: for each q in the current reason, if v==pivot || seen[v] skip, else mark seen and classify by trail.level_of(v). Walk i backward over trail.literals() to the next seen literal p, open -= 1; if open==0 break (p is the UIP), else pivot = |p|, reason = db.clause(trail.reason_of(pivot)). Set learned[0] = -uip; then find the highest level among learned[1..] as the backjump level and swap a literal of that level into slot 1 for the watch discipline.
The driver is a single loop around stages 1–3: propagate to a fixed point; on a conflict at level 0 return UNSAT, otherwise analyze, backjump, and install the learned clause (which is asserting — it immediately forces its literal at the new level); with no conflict and no unassigned variable, you have a model. First clean input clauses: sort/dedup literals and drop tautologies (they break the distinct-variable precondition).
Keep the pieces in sync: after each propagate, drain take_implications onto the trail with enqueue. On conflict, analyze gives (learned, back); trail.backjump(back) returns literals newest-first, which you db.unassign (saving each phase) before db.add_clause(learned). On no conflict, decide an unassigned variable. Document your decision heuristic — any deterministic complete one passes.
The reference uses integer VSIDS: bump activity[|lit|] for each literal of a learned clause, halve all activities every 128 conflicts, and decide the unassigned variable maximizing (activity[v], Reverse(v)) with its saved phase (initially false). The model-complete test: let Some(v) = decision else { return Some((1..=n).map(|v| db.value(v as i32).unwrap()).collect()) }. For generators, PHP(m,n) has an at-least-one clause per pigeon and a (-x[p][h], -x[q][h]) per hole-pair; waerden(j,k;n) forbids each j-AP (all red) and each k-AP (all blue).