proofs: DRAT refutations, Tseitin hard family, and a proof-shape bench

[InauguralPhysicist]

CDCL on an UNSAT instance emits a resolution refutation — conflict analysis is resolution and the learnt-clause sequence is the proof. This turns that from an incidental property into three usable things.

1. DRAT emission + an external oracle for UNSAT

--cdcl --proof FILE writes a DRAT refutation; tests/run_proof_check.sh has drat-trim verify it.

This is the first external oracle the UNSAT path has ever had. A SAT answer self-verifies against its model; an UNSAT answer had nothing checking it, so a bug that over-pruned the search would report s UNSATISFIABLE and the whole suite would stay green.

• Additions only, no d deletion lines — withholding deletions leaves the checker a superset of our clauses, which can only make a RUP check succeed, never fail. A proof that always verifies beats a smaller one that can spuriously fail.
• Includes a planted-fault case (lemmas removed from a valid proof) that the checker must reject. Without it, a misconfigured checker passes everything.
• Gate is drat-trim's exit code, not a grep: it prefixes s VERIFIED with a carriage return, so line-anchored patterns silently never match and such a check would pass unconditionally.

2. Tseitin-on-torus — the hard XOR family

The existing xor_triangle_case is the tractable regime (SAT, closes with zero conflicts), which left pigeonhole and complete-graph coloring as the only pressure — and those are the same family. k(n+1) with n colors is pigeonhole relabelled, and --proof-bench shows them producing byte-identical size/space/depth triples.

tseitin_torus_case adds genuine parity + expansion hardness (Urquhart 1987), a different mechanism from pigeonhole's counting. A solver change that helps both is real; one that helps only pigeonhole is exploiting counting structure. The odd/even pair at the same size is the control: same graph, same 72 clauses, charge parity flipped, and the even case closes with zero conflicts.

3. --proof-bench — size / space / depth

New counters peak_learnts (clause-space high-water mark, distinct from the surviving active_learnts) and max_level (deepest decision level). The three axes trade against each other, so a conflicts-only view hides real regressions — at pigeonhole-6-5, geom-saved gives size 1276 / space 56 while geom-negative gives 1605 / 42, and size-only vs space-only pick different winners.

Kept out of run_smoke.sh (seconds per solve on the hard families); runs as its own CI step.

Measured on this box

family	measurement
pigeonhole, n=3..6	resolutions 39 → 210 → 1276 → 12397 (×5.4, ×6.1, ×9.7 — multiplier rising, as Haken 1985 requires)
Tseitin torus	3×3 = 1974 resolutions (~1.7s); 4×4 = 95516 (~450s) — ×48 for one step of the expansion axis

Counters are byte-identical across runs, so counter claims need n=1 — the repo's n=5 rule is a wall-time rule, now stated as such in CLAUDE.md.

Also: CLI dispatch fix

The CLI ran the scan/DPLL solver unconditionally and discarded the result whenever --watched, --persistent, or --cdcl was given. On pigeonhole-6-5 (n=5 medians) that discarded solve was 531ms against 614ms of CDCL, so --cdcl went ~1145ms → 614ms. Counters were never affected (the discarded result was overwritten), so no previously reported measurement changes.

Verification

• tests/run_smoke.sh green, 3.4s → 4.4s
• tests/run_proof_check.sh green — 8 refutations verified, planted fault rejected, SAT case writes no proof
• All 13 existing bench modes green; all 4 solver paths × 3 fixtures correct after the dispatch change
• --lint clean (only the pre-existing W021 parse_args hint)

Honest ceiling

Measurement bounds proof size from above. Every result that matters in proof complexity is a lower bound, and those are theorems. This instrument validates that a family behaves as theory predicts and falsifies "that family is easy" claims — it does not settle anything.

🤖 Generated with Claude Code