fix: clause_locked deleted in-use reason clauses → unsound learnt clauses

[InauguralPhysicist]

Soundness bug. clause_locked checked only literal position 0. That is MiniSat's invariant, but this solver never swaps literals into slots 0/1 — it tracks watch positions in watch_a/watch_b, propagation moves them to arbitrary indices, and rebuild_watches resets them to 0/1 regardless of which literal is asserting. So position 0 is not reliably the asserting literal of a reason clause.

The chain

1. A learnt clause still serving as a reason looks unlocked
2. reduce_learnt_db deletes it — a flag only, nothing breaks yet
3. compact_deleted_clauses physically removes it and remaps state.reason[v] → -1
4. analyze_conflict_cdcl hits reason_ci < 0 and treats an implied literal as a decision
5. The clause it derives need not be implied → unsound

Confirmed, not theoretical

• drat-trim REJECTED refutations of pigeonhole-7-6 under --compact-policy eager
• and of three random 3-SAT instances found by the new policy fuzzer
• instrumenting the remap showed 7 dangling-reason events on pigeonhole-7-6 (eager) and 1 on pigeonhole-8-7 under the DEFAULT deferred policy — the default path is affected too, it just produced a valid proof by luck there

Why the suite missed it

The answer stayed correct. Pigeonhole is unsatisfiable whether or not the reasoning is sound, so every status assertion passed. Only the DRAT oracle could see it — and the proof-check corpus was all small instances, none of which compact.

That is the deeper finding: 0 of 180 random instances reached compaction, 4 reached clause-DB reduction. The most intricate code had no oracle on it.

Fix

clause_locked scans the clause for a literal whose variable has this clause as its reason. O(width) instead of O(1) — no measurable cost at these sizes, and the only check that is correct in a non-swapping design.

Also in this change

• --model emits DIMACS v-lines, so a SAT answer is externally checkable (previously only UNSAT had an oracle)
• --compact-policy / --restart-policy / --phase-policy on the CLI — the compaction machinery was only reachable from bench code, which is why randomized testing never hit it
• tests/fuzz_differential.py — 6 shape families (tautologies, duplicate literals, unit-heavy, unused vars, dup clauses), all four paths must agree, SAT models checked, UNSAT proofs drat-trim'd
• tests/fuzz_policy.py — same oracle across policies; reports path coverage so "we tested compaction" is measured, not assumed
• Regression: tests/fixtures/pigeonhole_6_5.cnf under eager+luby in run_proof_check.sh — red before (drat-trim exit 1), green after, ~1.3s
• Both fuzzers planted-fault validated: a corrupted model is caught by the model check, a dropped learnt literal by drat-trim and by path disagreement

Consequence for banked numbers

Counters banked before today came from the buggy solver and shift under the fix (more clauses correctly stay locked → different search). Tseitin 3×3 goes 673 → 619 learnt clauses. Re-measure before comparing to any pre-fix number.

🤖 Generated with Claude Code