From 7143f42868dcfa385ccbd029e8a640dadd789b47 Mon Sep 17 00:00:00 2001 From: InauguralPhysicist Date: Wed, 29 Jul 2026 20:37:26 -0500 Subject: [PATCH] bench: bank the Tseitin ladder outcome -- axis separation measured 4x5 closed at 551,098 resolutions in 6,285s, which is the measurement the night was reallocated to get. Predictions are unedited; this appends an outcome section and copies banked.log into the repo. PREDICTION 2 -- band missed, core claim CONFIRMED. Predicted 1.3x-5x per fixed-expansion step with ~20x as the falsification threshold; measured 4x4 -> 4x5 = 5.77x. The narrow band is wrong at the margin, but 5.77x is nowhere near the 20x that would mean the rectangular axis is also exponential. The axis separation is now measured on both sides with closed cases: expansion (min(r,c) grows) 3x3 -> 4x4 x48.4 fixed-expansion (formula grows) 4x4 -> 4x5 x5.77 The expansion axis is 8.4x steeper per step. That is the ladder's central result and it holds. Practical consequence recorded in CLAUDE.md: scale the square dimension for hardness, the rectangular one for a bigger formula at constant hardness. PREDICTION 3 -- CONFIRMED. size/space (resolutions/peak_learnts) climbs 14 -> 115 -> 340 across 3x3/4x4/4x5, so learnt-DB reduction bounds clause space rather than letting it track proof size. PREDICTION 4 -- correct, 5x5 exceeded its cap and the trajectory bounded it from below as designed. PREDICTION 1 -- still open. 5x5 needs >=~1.9M resolutions to confirm and the 6h attempt reached 1,194,575 without closing. Relaunched with an 8.5h cap. Note the asymmetry: a timeout can confirm this prediction but cannot falsify it; only a closed 5x5 can. A 5x5 closing BELOW ~1.9M would falsify it and would be the more interesting outcome, since it would mean the expansion-axis multiplier is decreasing (48.4x then under 20x) against the rising-multiplier pattern pigeonhole shows. CALIBRATION LESSON. 4x5 closed at 6,285s against an original 5,400s cap -- missed by 884 seconds, under 15 minutes, and banked nothing but a bound. A case that nearly closes banks exactly as little as one that never started. Budget caps with real margin, and prefer one case with headroom over several that each nearly finish. Co-Authored-By: Claude Opus 5 (1M context) --- CLAUDE.md | 28 +++++++++++--- benchmarks/TSEITIN_LADDER.md | 72 ++++++++++++++++++++++++++++++++++++ 2 files changed, 95 insertions(+), 5 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index b1294b7..411517b 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -156,11 +156,29 @@ The solver doubles as a proof-complexity instrument, because a CDCL refutation are broken, not that the theorem is wrong. That makes the bench 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 3x3 = 1974 - resolutions; 4x4 = 95516 (x48 for one step of the expansion axis, ~450s). - The square axis is the real hardness axis, and it goes intractable - immediately under the interpreter — hence the odd/even control pair at 3x3 - instead of a square ladder. + 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. +- **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 + started. Prefer one case with generous headroom over several that each nearly + finish. Honest ceiling: measurement bounds proof size from *above*. Every result that matters in proof complexity is a lower bound, and those are theorems. This diff --git a/benchmarks/TSEITIN_LADDER.md b/benchmarks/TSEITIN_LADDER.md index 6fdd243..650a590 100644 --- a/benchmarks/TSEITIN_LADDER.md +++ b/benchmarks/TSEITIN_LADDER.md @@ -170,3 +170,75 @@ same single-case plan. expansion-axis multiplier is *decreasing*, which contradicts the rising- multiplier pattern pigeonhole shows. This ladder cannot settle that on this hardware — it needs either much more time or a faster runtime. + +# Outcome + +Banked 2026-07-29 20:40 CDT. Written after the predictions above, which are +unedited. **5x5 is still running** — see the open item at the end. + +## Measurements (closed cases only) + +| case | vars | clauses | resolutions | conflicts | learnt_lits | peak_learnts | max_level | wall | +|---|---|---|---|---|---|---|---|---| +| 3x3 | 18 | 72 | 1,974 | 673 | 3,557 | 143 | 11 | 1.7s | +| 4x4 | 32 | 128 | 95,516 | 27,388 | 208,781 | 832 | 20 | 429s | +| 4x5 | 40 | 160 | 551,098 | 135,285 | 1,109,225 | 1,619 | 27 | 6,285s | + +## Prediction 2 — band missed, core claim CONFIRMED + +Predicted 1.3x-5x per fixed-expansion step, with ~20x as the falsification +threshold. **Measured 4x4 -> 4x5 = 5.77x.** + +The narrow band is missed (5.77 > 5), so the prediction as stated is wrong at +the margin. The claim it was testing survives cleanly: 5.77x is nowhere near +the 20x that would mean the rectangular axis is also exponential. + +**The axis separation is real and now measured on both sides with closed cases:** + +| axis | step | multiplier | +|---|---|---| +| expansion (`min(r,c)` grows) | 3x3 -> 4x4 | **x48.4** | +| fixed-expansion (formula grows) | 4x4 -> 4x5 | **x5.77** | + +The expansion axis is **8.4x steeper per step**. That is the ladder's central +result and it holds. + +## Prediction 3 — CONFIRMED + +Space grows far slower than size; the size/space ratio climbs steadily, so +learnt-DB reduction is bounding clause space rather than letting it track proof +size. + +| case | resolutions | peak_learnts | size/space | +|---|---|---|---| +| 3x3 | 1,974 | 143 | 14 | +| 4x4 | 95,516 | 832 | 115 | +| 4x5 | 551,098 | 1,619 | 340 | + +## Prediction 4 — correct + +5x5 did exceed its 6h cap, and the trajectory bounded it from below as designed. + +## Calibration lesson + +4x5 closed at **6,285s** against an original cap of 5,400s — it missed by +**884 seconds, under 15 minutes.** The first cap was within ~15% of sufficient +and still produced nothing but a bound. Two things follow for future long runs +on this box: budget caps with a real margin rather than a point estimate, and +prefer one case with generous headroom over several that each nearly finish. +A case that nearly closes banks exactly as little as one that never starts. + +## Open: prediction 1 + +Unresolved. 5x5 needs `>= ~1.9M` resolutions to confirm; the 6h attempt reached +1,194,575 (`>= 12.5x`) without closing. Relaunched 2026-07-29 20:35 with an +8.5h cap. Outcomes: + +- closes anywhere `>= 1.9M` -> prediction 1 confirmed +- closes below `~1.9M` -> prediction 1 **falsified**, and the expansion-axis + multiplier is *decreasing* (48.4x then under 20x), which would contradict the + rising-multiplier pattern pigeonhole shows and is the more interesting result +- times out again -> bound tightens toward ~18x, still unresolved + +Note the asymmetry: a timeout can confirm this prediction but cannot falsify +it. Only a closed 5x5 can do that.