diff --git a/CLAUDE.md b/CLAUDE.md index 411517b..87b388a 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -157,23 +157,38 @@ The solver doubles as a proof-complexity instrument, because a CDCL refutation self-validating in the way a planted fault validates a checker. - Measured on this box: pigeonhole resolutions 39 -> 210 -> 1276 -> 12397 for n = 3..6 (x5.4, x6.1, x9.7, multiplier rising). -- **Tseitin has two axes and they are NOT the same** (ladder run 2026-07-29, - `benchmarks/TSEITIN_LADDER.md` is the record of record): - - | axis | step | multiplier | - |---|---|---| - | expansion, `min(rows,cols)` grows | 3x3 -> 4x4 | **x48.4** | - | fixed-expansion, formula grows | 4x4 -> 4x5 | **x5.77** | - - Closed cases: 3x3 = 1,974 resolutions (1.7s), 4x4 = 95,516 (429s), - 4x5 = 551,098 (6,285s). The expansion axis is 8.4x steeper per step, so - **scale the square dimension when you want hardness and the rectangular one - when you want a bigger formula at constant hardness.** 5x5 exceeded a 6h cap - at 1.19M resolutions without closing — it is out of reach here. -- Space is bounded, size is not: size/space (`resolutions` / `peak_learnts`) - climbs 14 -> 115 -> 340 across 3x3/4x4/4x5. Learnt-DB reduction is doing its - job; if that ratio ever stops climbing, suspect reduction before suspecting - the family. +- **Tseitin closed measurements** (ladder run 2026-07-29, + `benchmarks/TSEITIN_LADDER.md` is the record of record): 3x3 = 1,974 + resolutions (1.7s), 4x4 = 95,516 (429s), 4x5 = 551,098 (6,285s). 5x5 is out + of reach here — two attempts totalling 14.5h reached only 1,549,543 without + closing. +- **RETRACTED 2026-07-30 (adversarial review): there is no measured "two axis" + separation.** An earlier version of this file claimed the expansion axis was + 8.4x steeper than the fixed-expansion axis and told you to scale the square + dimension for hardness. That compared steps with unequal variable increments + (3x3->4x4 adds 14 vars, 4x4->4x5 adds 8). Normalised per variable the growth + is 1.319x, 1.245x, then `>=`1.109x — *decreasing*, and indifferent to which + axis moved. Worse, the only clean single-dimension expansion step in the data + (4x5 -> 5x5) is `>=`2.81x, which is *lower* than the flat step's 5.77x. The + size-matched control that could settle it is **4x6 (48 vars, min=4) against + 5x5 (50 vars, min=5)** — and 4x6 was killed mid-run as "more of the same on + the cheap axis", destroying the control. Do not repeat the claim without + running 4x6. +- **Do not read `resolutions` / `peak_learnts` as a size-vs-space finding.** + That ratio climbs by construction: `resolutions` is cumulative and unbounded + while `peak_learnts` is pinned to the reduction schedule + (`learnt_limit` starts at 4 and grows +2 per reduce run, so + `peak_learnts ~= 4 + 2 * reduce_runs`). It measures the DB policy, not the + formula family. A real size-vs-space result needs proof space for a *fixed* + refutation, not a policy-capped high-water mark. +- **`count_active_learnts` is O(total clauses) and runs every conflict** (via + `reduce_learnt_db`), but it is NOT the bottleneck: replacing it with an + incrementally maintained counter bought only **4.4%** at 4x4 (429.2s -> + 410.4s, counters byte-identical). Do not "fix" it — the incremental version + adds a state invariant that only `build_cdcl_state` maintains, and the + hand-built `reduce_state` in `tests/test_solver.eigs` breaks immediately + ("cannot compare none and num"). `count_active_learnts` derives from the + arrays and needs no invariant; that robustness is worth 4%. - **Long-run caps need margin, not point estimates.** 4x5 closed at 6,285s against a 5,400s cap — missed by under 15 minutes and banked nothing but a bound. A case that nearly closes banks exactly as little as one that never diff --git a/benchmarks/TSEITIN_LADDER.md b/benchmarks/TSEITIN_LADDER.md index d741d6a..9e9995f 100644 --- a/benchmarks/TSEITIN_LADDER.md +++ b/benchmarks/TSEITIN_LADDER.md @@ -308,3 +308,78 @@ Either of these before any further 5x5 attempt: The ladder's central result (axis separation, x48.4 vs x5.77) does not depend on 5x5 and stands. + +# Adversarial review — 2026-07-30 + +Review of this document's own claims. Two are withdrawn. + +## F1 — RETRACTED: the axis-separation result + +The "expansion axis is 8.4x steeper" headline compared **steps with unequal +variable increments**: 3x3 -> 4x4 adds 14 variables, 4x4 -> 4x5 adds 8. Part of +the x48.4 vs x5.77 gap is simply the bigger jump. + +Normalised per variable: + +| step | axis | +vars | ratio | per-variable | +|---|---|---|---|---| +| 3x3 -> 4x4 | expansion | +14 | x48.39 | 1.319x | +| 4x4 -> 4x5 | flat | +8 | x5.77 | 1.245x | +| 4x5 -> 5x5 | expansion | +10 | `>=`x2.81 | `>=`1.109x | + +Growth per variable is **monotonically decreasing and indifferent to which axis +moved.** And the one clean single-dimension expansion step available +(4x5 -> 5x5, where `min` goes 4 -> 5) is `>=`2.81x — *lower* than the flat +step's 5.77x, i.e. currently the opposite direction. + +Note the design confound: starting from a square torus you cannot raise +`min(r,c)` without adding both a row and a column, so "square cases" bundles +expansion with a double-size jump. The step that breaks the confound is a +**size-matched pair: 4x6 (48 vars, min=4) vs 5x5 (50 vars, min=5)**. 4x6 was +killed mid-run as "more of the same on the cheap axis" — that judgement +destroyed the control for the headline claim. + +**Status: the two-axis story is unsupported by this data.** Prediction 2's +falsification threshold (20x) still was not crossed, so nothing here shows the +rectangular axis *is* exponential either. The question is open, and 4x6 is the +cheapest experiment that would move it. + +## F2 — WITHDRAWN: prediction 3 was vacuous + +"Space grows sub-linearly in size" is true but says nothing about Tseitin. +`resolutions` is cumulative and unbounded; `peak_learnts` is pinned to the +reduction schedule — `learnt_limit` starts at 4 and grows +2 per reduce run, so +`peak_learnts ~= 4 + 2 * reduce_runs` (143, 832, 1619, 1842 imply ~70, ~414, +~808, ~919 reduce runs). The ratio climbing is a restatement of the DB policy. +A real size-vs-space result needs proof space for a *fixed* refutation. + +## F3 — REFUTED (a review hypothesis, not a prior claim) + +Hypothesis: the rate decay (76 -> 35 res/s) is an implementation artifact, +because `count_active_learnts` is O(total clauses) and runs every conflict. +Tested with an incrementally maintained counter: 4x4 went 429.2s -> **410.4s, +just 4.4%**, with byte-identical counters. **Refuted.** The decay is not that +scan, and the conclusion that 5x5 is out of reach under the interpreter stands. + +## F4 — the O(1) counter is a bad trade regardless + +It introduces an invariant only `build_cdcl_state` maintains. The hand-built +`reduce_state` in `tests/test_solver.eigs` broke instantly with "cannot compare +none and num". `count_active_learnts` derives from the arrays and needs no +invariant — worth keeping for 4%, especially with the EigenOS ROM-bundle path +constructing state independently. + +## What survives the review + +- **The generator is genuine.** Every edge appears in exactly two vertices' + incident lists, every vertex has degree 4 with four distinct edges, verified + for 3x3, 3x4, 4x4, 4x5, 5x5, 3x7, 6x4. That incidence-exactly-2 property is + what makes XOR-ing all vertex constraints cancel every edge and leave + `0 = sum(charges)`, so odd charge really does imply UNSAT. +- **The closed measurements**: 3x3 = 1,974, 4x4 = 95,516, 4x5 = 551,098. +- **The DRAT oracle.** Only one `add_cdcl_clause` site emits (learnt=1); + compaction does not route through it, so there is no double-emission. With + drat-trim verification plus the planted-fault rejection, the claim holds. +- **Pigeonhole == coloring**, refined: the CNFs are *not* byte-identical (clause + order differs) but have identical variable and clause counts and produce + byte-identical solver counters. Same principle, as claimed. diff --git a/tests/run_smoke.sh b/tests/run_smoke.sh index ed4569e..1a6d377 100755 --- a/tests/run_smoke.sh +++ b/tests/run_smoke.sh @@ -8,6 +8,7 @@ EIGS="${EIGENSCRIPT_BIN:-$(command -v eigenscript || echo ../EigenScript/src/eig cd "$ROOT" "$EIGS" tests/test_solver.eigs +"$EIGS" tests/test_tseitin_invariant.eigs "$EIGS" minisat.eigs tests/fixtures/simple_sat.cnf "$EIGS" minisat.eigs --watched tests/fixtures/simple_sat.cnf "$EIGS" minisat.eigs --persistent tests/fixtures/simple_sat.cnf diff --git a/tests/test_tseitin_invariant.eigs b/tests/test_tseitin_invariant.eigs new file mode 100644 index 0000000..cf53780 --- /dev/null +++ b/tests/test_tseitin_invariant.eigs @@ -0,0 +1,53 @@ +# Structural oracle for the Tseitin generator: every edge must appear in EXACTLY +# two vertices' incident-edge lists. That is what makes XOR-ing all vertex +# constraints cancel every edge and leave 0 = sum(charges), so odd charge implies +# UNSAT. Cheap (no solving), and it is the check that separates "a genuine Tseitin +# formula" from "some UNSAT CNF that happens to look like one". +load_file of "lib/int_vector.eigs" +load_file of "lib/dimacs.eigs" +load_file of "lib/solver.eigs" +load_file of "lib/bench.eigs" + +# ADVERSARIAL INVARIANT: in a Tseitin formula every edge must appear in EXACTLY +# two vertices' incident-edge lists. That is what makes XOR-ing all vertex +# constraints cancel every edge and leave 0 = sum(charges), which is the whole +# reason odd charge implies UNSAT. If any edge appears 1 or 3 times, the object +# is not a Tseitin formula and every number banked from it is meaningless. +for spec in [[3, 3], [3, 4], [4, 4], [4, 5], [5, 5], [3, 7], [6, 4]]: + rows is spec[0] + cols is spec[1] + counts is int_vector_filled of [(2 * rows * cols) + 1, 0] + degree_ok is 1 + for r in range of rows: + for c in range of cols: + edges is tseitin_vertex_edges of [r, c, rows, cols] + if (len of edges) != 4: + degree_ok is 0 + # distinctness within the vertex + for i in range of 4: + for j in range of 4: + if i < j: + if edges[i] == edges[j]: + degree_ok is 0 + for e in edges: + counts[e] += 1 + bad is 0 + lo is 99 + hi is 0 + for v in range of (2 * rows * cols): + n is counts[v + 1] + if n != 2: + bad += 1 + if n < lo: + lo is n + if n > hi: + hi is n + verdict is "FAIL" + if bad == 0: + if degree_ok == 1: + verdict is "ok" + assert of [bad == 0, f"tseitin edge incidence != 2 for {rows}x{cols}"] + assert of [degree_ok == 1, f"tseitin vertex not degree-4-distinct for {rows}x{cols}"] + print of f"{rows}x{cols}: edges={2 * rows * cols} incidence_min={lo} incidence_max={hi} wrong_incidence={bad} degree4_distinct={degree_ok} -> {verdict}" + +print of "=== Tseitin structural invariant: ok ==="