bench: amend Tseitin ladder — give the whole night to 4x5 (mid-run) - #70
Merged
Conversation
No registered prediction is edited; only the remaining schedule changes. State after pass 1: 4x4 DONE at 95,516 resolutions in 429s; 4x5 TIMEOUT at >=452,569 (>=4.74x); 5x5 TIMEOUT at >=1,194,575 (>=12.5x). Both ratio predictions are UNRESOLVED and neither is confirmed -- 5x5 reached only 12.5x against a >=20x prediction, so it did not confirm prediction 1 from below as Amendment 1 hoped. My original time estimates were wrong by roughly 5-10x. Stating that plainly rather than quietly re-tuning: the caps came from a 3x3->4x4 extrapolation that badly underestimated how per-conflict cost grows with formula size. That estimation error, not the hardware, cost this run its headroom. Killed 4x6 mid-run (strictly harder than a 4x5 that could not close in 90 min, so a guaranteed timeout), dropped 4x7, and gave the whole remaining window to 4x5 alone with a 9.5h cap. The @reboot cron resumes the same single-case plan. Why 4x5 over 5x5 with room for only one: a closed case is a measurement and everything else is a bound, 4x5 is likeliest to close, and prediction 2 is the claim most likely to be wrong -- the two-axis framing rests on the rectangular axis being flat and it is already leaving the predicted band. 5x5 would need ~9.25h from scratch just to cross 1.9M, and since the search is deterministic a shorter re-run only re-treads the same trajectory. Left open: 5x5's >=12.5x sits well below the 48x measured for 3x3->4x4. If its true ratio lands near 15-25x the expansion-axis multiplier is DECREASING, contradicting the rising-multiplier pattern pigeonhole shows. This hardware cannot settle that. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Second mid-run amendment. No registered prediction is edited — only the remaining schedule.
State after pass 1
Both ratio predictions are unresolved and neither is confirmed. 5×5 reached only 12.5× against a
≥20×prediction — so it did not confirm prediction 1 from below the way Amendment 1 hoped. It needed ~1.9M and stopped at 1.19M.My estimates were wrong by 5–10×
Stating it plainly rather than quietly re-tuning: the caps came from a 3×3→4×4 extrapolation that badly underestimated how per-conflict cost grows with formula size. That estimation error, not the hardware, is what cost this run its headroom.
Change
Killed 4×6 mid-run (strictly harder than a 4×5 that couldn't close in 90 min — a guaranteed timeout), dropped 4×7, gave the whole remaining window to 4×5 alone with a 9.5h cap (18:50 → 04:20, buffer before the ~05:57 reboot). The
@rebootcron resumes the same single-case plan.Why 4×5 and not 5×5
Room for only one in ~10.9h:
Left open
5×5's ≥12.5× sits well below the 48× measured for 3×3→4×4. If its true ratio lands near 15–25×, the expansion-axis multiplier is decreasing, contradicting the rising-multiplier pattern pigeonhole shows. This ladder can't settle that on this hardware — it needs much more time or a faster runtime.
🤖 Generated with Claude Code