Repository navigation
Claude/2026 sota benchmark xyp1zh - #30
Merged
Merged
Conversation
Address the readiness blockers from an external review, all Charter-aligned.
1. Correctness contradiction FIXED. docs/ladder/README.md said "NS >= width on
every instance tested"; the code/test say otherwise. Verified against
test_ns_and_width_are_incomparable: PHP (width 2, NS 4) and Tseitin K4
(width 4, NS 3) -- incomparable, both directions. Corrected the two stale
lines to match.
2. Reproducibility. Added REPRODUCIBILITY.md: pinned tool versions (Kissat
4.0.4, CaDiCaL 3.0.0, CryptoMiniSat 5.14.7, numpy 2.4.6), one-command
regeneration for each benchmark, expected output shape, how to read a
discrepancy, and an explicit scope statement.
3. Hard CI certification lane. Split CI into unit-fast (may skip solvers) and
certification-hard (Kissat + drat-trim MANDATORY, no "|| true"): runs a real
DRAT UNSAT check + a model-replay SAT check via .github/scripts/
certification_smoke.py and fails red if certification does not execute.
4. Packaging. pyproject.toml (setuptools, console script lambda-sat =
backend.cli:cli_main, dev/bench extras); added cli_main sync wrapper;
editable install + console script verified. CITATION.cff, CONTRIBUTING.md.
Replaced the generic GitHub-boilerplate SECURITY.md with a project policy
framed on soundness/the TCB. egg-info gitignored.
5. Scope. Damped the first-contact "beats every solver" phrasing in README to
the measured mix and structural axis, with a scope note pointing to
REPRODUCIBILITY.md ("a certified middleware and research harness, not a
generally faster SAT solver").
650 tests pass; certification smoke passes locally.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Gkw2ccXyb4DEtqFo29ouQD
Add a scoped public landing site under docs/, ordered
certification -> frames -> scoped benchmark -> reproducibility -> research
geometry (not geometry -> SOTA -> metaphysics). Plain Markdown, no theatre.
- docs/index.md: the recognizer stated first ("does not replace CDCL; decides
structured islands before it and certifies every verdict"); the TCB; the
three-frame table; a scoped benchmark table (numbers deferred to the
capsule); an explicit "what it does NOT claim" section; reproduce commands
(verified working in strict mode); the research ladder as a map, not a proof.
- docs/technical-note.md: "Structured Islands Before CDCL" -- abstract,
architecture, the three frames (condition/certificate/failure mode), the
certification boundary, a benchmark capsule paragraph, interpretation,
limitations, reproduction.
- docs/benchmark-capsule.md: setup (engines/families/timeout/hardware/metric),
the measured tables, and an honest "what improves / what does not" split.
- docs/assets/architecture.mmd: mermaid source of the router diagram.
- docs/_config.yml: minimal Pages config (serve from /docs on main).
Landing-page headline is the routing + certification, not a speed record;
"49x"/"beats CMS" live only in the lower capsule, scoped to the mix.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Gkw2ccXyb4DEtqFo29ouQD
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
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.
No description provided.