From a80f19c8fcc421146619ce726bbe3b47b31fdf42 Mon Sep 17 00:00:00 2001 From: InauguralPhysicist Date: Thu, 30 Jul 2026 05:26:07 -0500 Subject: [PATCH] review: retract the axis-separation claim and prediction 3 Adversarial review of my own ladder claims. Two are withdrawn, one review hypothesis is refuted, and the generator gets the structural oracle it should have had from the start. F1 RETRACTED -- "the expansion axis is 8.4x steeper". It compared steps with unequal variable increments: 3x3->4x4 adds 14 vars, 4x4->4x5 adds 8. Per variable the growth is 1.319x, 1.245x, then >=1.109x -- decreasing, and indifferent to which axis moved. The only clean single-dimension expansion step in the data (4x5->5x5) is >=2.81x, LOWER than the flat step's 5.77x. Design confound: 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 it is a size-matched pair, 4x6 (48 vars, min=4) vs 5x5 (50 vars, min=5) -- and 4x6 was killed mid-run as "more of the same on the cheap axis", which destroyed the control for the headline claim. Prediction 2's 20x threshold still was not crossed, so nothing shows the rectangular axis IS exponential either. Open question; 4x6 is the cheapest experiment that moves it. F2 WITHDRAWN -- prediction 3 was vacuous. resolutions is cumulative and unbounded while peak_learnts is pinned to the reduction schedule (learnt_limit starts at 4, +2 per reduce run, so peak ~= 4 + 2*runs; the banked 143/832/1619/1842 imply ~70/~414/~808/~919 runs). The climbing ratio restates the DB policy, not a property of the family. F3 REFUTED (a review hypothesis, not a prior claim) -- I suspected the 76->35 res/s decay was an artifact of count_active_learnts being O(total clauses) per conflict. Tested with an incremental counter: 4x4 went 429.2s -> 410.4s, only 4.4%, counters byte-identical. So the decay is not that scan and "5x5 is out of reach under the interpreter" stands. F4 -- and that optimization is a bad trade anyway: it adds an invariant only build_cdcl_state maintains, and the hand-built reduce_state in test_solver.eigs breaks instantly ("cannot compare none and num"). count_active_learnts derives from the arrays and needs no invariant. Both findings recorded in CLAUDE.md so neither is re-attempted. SURVIVES: the generator is genuine -- every edge appears in exactly two vertices' incident lists, every vertex is degree-4 with 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. Promoted to tests/test_tseitin_invariant.eigs in run_smoke.sh, and planted-fault validated (duplicating an incident edge makes it fail). Also surviving: the closed measurements (1,974 / 95,516 / 551,098), the DRAT oracle (single emission site, compaction does not route through it), and pigeonhole == coloring, refined -- the CNFs are not byte-identical but have identical var and clause counts and produce byte-identical counters. Co-Authored-By: Claude Opus 5 (1M context) --- CLAUDE.md | 49 +++++++++++++------- benchmarks/TSEITIN_LADDER.md | 75 +++++++++++++++++++++++++++++++ tests/run_smoke.sh | 1 + tests/test_tseitin_invariant.eigs | 53 ++++++++++++++++++++++ 4 files changed, 161 insertions(+), 17 deletions(-) create mode 100644 tests/test_tseitin_invariant.eigs 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 ==="