bench: 5x5 unresolved — bank the result and the estimation post-mortem - #72
Merged
Conversation
5x5 timed out again at the 8.5h cap: 1,549,543 resolutions = 16.22x, short
of the >=20x threshold by 360,777. Prediction 1 is neither confirmed nor
falsified. Two attempts (6h + 8.5h = 14.5h) produced only a lower bound, and
with no single-solve resume the second re-derived the first's entire
trajectory before adding anything.
ROOT CAUSE of every bad estimate this run: the rate decays. Measured on
attempt 2, resolutions/s halves over the run as the learnt DB grows --
76 -> 65 -> 52 -> 45 -> 39 -> 35. Every projection extrapolated an
early-phase rate and overshot, three times, same direction, same reason.
Any cap or ETA for this workload must assume a decaying rate; a linear
extrapolation from hour one is worthless. If 5x5's true size is near the 48x
that 3x3 -> 4x4 showed (~4.6M), the interpreter needs on the order of 40h.
What should have been done first, recorded so it is not repeated:
1. Probe before scheduling -- 10 minutes measuring rate AND decay would
have shown 5x5 was unreachable and collapsed a five-case ladder into
one decision, instead of extrapolating from a single data point.
2. Check that a timeout is recoverable before relying on timeouts. The
design leaned on "a capped case still yields a trajectory", which is
true but nearly worthless without resume -- the trajectory can only be
re-derived, so cap sizing was a bet-the-run decision sized as a hedge.
3. Question the runtime instead of accepting it. "Intractable under the
interpreter" was recorded as a finding and then a night was spent
confirming it, while ouroboros/aot exists. Fix the instrument before
spending nights measuring around it.
Recommended before any further 5x5 attempt: an AOT feasibility probe, or
serializable CDCL session state (cdcl_begin/cdcl_step is already a
checkpoint mechanism except that it cannot be written to disk and reloaded).
The ladder's central result -- axis separation, x48.4 expansion vs x5.77
fixed-expansion, both from closed cases -- does not depend on 5x5 and stands.
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.
5×5 timed out again: 1,549,543 resolutions = 16.22×, short of the
≥20×threshold by 360,777. Prediction 1 is neither confirmed nor falsified.14.5h of compute for a lower bound — and with no single-solve resume, attempt 2 re-derived attempt 1's entire trajectory before adding anything.
Root cause of every bad estimate: the rate decays
Rate halves over the run as the learnt DB grows. Every projection I made extrapolated an early-phase rate and overshot — three times, same direction, same reason. A linear extrapolation from hour one is worthless here. If 5×5's true size is near the 48× that 3×3→4×4 showed (~4.6M), the interpreter needs on the order of 40h.
What should have been done first
ouroboros/aotexists. Fix the instrument before spending nights measuring around it.Recommended before any further 5×5 attempt
ouroboros/aot) — can the solver compile, and what is the real speedup on this workload?cdcl_begin/cdcl_stepis already a checkpoint mechanism in every respect except that the session can't be written to disk and reloaded.The ladder's central result — axis separation, ×48.4 expansion vs ×5.77 fixed-expansion, both from closed cases — does not depend on 5×5 and stands.
🤖 Generated with Claude Code