Claude/2026 sota benchmark xyp1zh

.github/scripts/certification_smoke.py

@@ -0,0 +1,57 @@
+"""Hard certification smoke test for CI (the `certification-hard` lane).
+
+Unlike the unit lane -- which skips gracefully when Kissat/drat-trim are absent -- this
+script REQUIRES them and fails red if the certification path does not actually execute:
+
+  1. Kissat and drat-trim must be on PATH (else exit 1).
+  2. A CDCL UNSAT verdict must be replayed and accepted by drat-trim (a real DRAT check).
+  3. A CDCL SAT verdict must be replayed against the formula (a real model check).
+
+Both instances are plain 3-CNF with no frame structure, so they are decided by the CDCL
+engine + certification, not by a self-certifying frame -- this exercises exactly the path
+the unit lane is allowed to skip. Exit 0 only if both certifications ran and passed.
+"""
+
+import shutil
+import sys
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parents[2]))
+
+from backend.cnf_utils import CNFFormula                # noqa: E402
+from backend.metasolver import _certified_cdcl          # noqa: E402
+
+
+def _fail(msg: str) -> None:
+    print(f"CERTIFICATION LANE FAILED: {msg}")
+    sys.exit(1)
+
+
+def main() -> None:
+    for tool in ("kissat", "drat-trim"):
+        if shutil.which(tool) is None:
+            _fail(f"{tool} is not on PATH; the certification lane requires it")
+
+    # All 8 clauses over 3 variables exclude all 8 assignments -> UNSAT, and it carries
+    # no 2-SAT / parity / counting structure, so it is refuted by CDCL + a DRAT proof.
+    unsat = CNFFormula(3, [[a, b, c] for a in (1, -1) for b in (2, -2) for c in (3, -3)])
+    status, _t, verified = _certified_cdcl(unsat, "kissat", 10.0)
+    if status != "UNSAT":
+        _fail(f"expected UNSAT on the 8-clause formula, got {status}")
+    if not verified:
+        _fail("UNSAT verdict was NOT DRAT-certified (drat-trim did not run/accept)")
+    print("ok: CDCL UNSAT replayed and accepted by drat-trim")
+
+    sat = CNFFormula(3, [[1, 2, 3], [-1, -2, 3], [1, -2, -3]])
+    status, _t, verified = _certified_cdcl(sat, "kissat", 10.0)
+    if status != "SAT":
+        _fail(f"expected SAT on the satisfiable formula, got {status}")
+    if not verified:
+        _fail("SAT model was NOT verified against the formula (model replay failed)")
+    print("ok: CDCL SAT model replayed against the formula")
+
+    print("CERTIFICATION LANE PASSED: DRAT UNSAT + model-replay SAT both executed.")
+
+
+if __name__ == "__main__":
+    main()

.github/workflows/tests.yml

@@ -6,6 +6,9 @@ on:
   pull_request:
 
 jobs:
+  # Lane 1 -- unit-fast: portable, may skip solver-dependent tests if the external
+  # binaries are unavailable (shutil.which -> None). Green does not by itself assert
+  # that external certification executed; that is lane 2's job.
   unit-fast:
     runs-on: ubuntu-latest
     strategy:
@@ -24,16 +27,29 @@ jobs:
         run: |
           python -m pip install --upgrade pip
           pip install -r backend/requirements.txt
+
+      # Best-effort: install the external solvers so the @requires_kissat
+      # integration tests run too. If a package is unavailable the tests skip
+      # gracefully (shutil.which -> None), so this lane stays green either way.
+      - name: Install SAT solvers (best effort)
+        run: sudo apt-get update && sudo apt-get install -y kissat drat-trim cadical || true
           pip install -e .[dev]
 
       - name: Run test suite
         run: python -m pytest backend/tests/ -q
 
+  # Lane 2 -- certification-hard: Kissat + drat-trim are MANDATORY. This lane fails
+  # red if the external certification path does not actually execute -- it is the
+  # lane that stands behind the repo's headline claim (verify, don't trust).
   certification-hard:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
 
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
       - name: Set up Python 3.11
         uses: actions/setup-python@v5
         with:
@@ -43,6 +59,22 @@ jobs:
         run: |
           python -m pip install --upgrade pip
           pip install -r backend/requirements.txt
+
+      # Mandatory, NOT best-effort: no "|| true". If these are unavailable the lane
+      # must fail rather than silently skip the certification it is guarding.
+      - name: Install Kissat + drat-trim (mandatory)
+        run: sudo apt-get update && sudo apt-get install -y kissat drat-trim
+
+      - name: Assert the external tools are present
+        run: |
+          command -v kissat
+          command -v drat-trim
+
+      - name: Certification smoke (real DRAT UNSAT + model-replay SAT)
+        run: python .github/scripts/certification_smoke.py
+
+      - name: Certification-relevant tests must run (not skip)
+        run: python -m pytest backend/tests/test_integration.py backend/tests/test_kissat_wrapper.py -q
           pip install -e .[dev]
 
       - name: Build SAT/proof tools

.gitignore

@@ -37,3 +37,9 @@ __pycache__/
 
 # regenerable benchmark outputs (produced by docs/ladder/scripts/*.py)
 docs/ladder/scripts/*_results.json
+
+# Python packaging artifacts
+*.egg-info/
+build/
+dist/
+__pycache__/

CITATION.cff

@@ -1,4 +1,23 @@
 cff-version: 1.2.0
+message: "If you use this software or its research notes, please cite it as below."
+title: "λSAT — certified λ-logic SAT middleware and a research harness for frame-structured SAT hardness"
+abstract: >-
+  A headless, certified Boolean-satisfiability middleware: it decides formulas via
+  three sound, engine-independent frames (implication/2-SAT, parity/GF(2),
+  counting/cardinality) and their coupling, falling back to a DRAT-certified CDCL
+  engine only when no frame applies. Every verdict is independently checked (SAT by
+  model replay, UNSAT by a sound frame refutation or a drat-trim proof). On top sits
+  a research program on the intrinsic geometry of SAT hardness — a hyperbolic
+  instance-manifold, a game-theoretic dispatcher, and an explicit proven/measured/
+  speculative claim ledger.
+type: software
+authors:
+  - family-names: "Vilela Franco"
+    given-names: "Jesús"
+repository-code: "https://github.com/jesusvilela/lambda-sat-solver"
+url: "https://github.com/jesusvilela/lambda-sat-solver"
+license: MIT
+version: "0.1.0"
 message: "If you use this software, please cite it using the metadata from this file."
 title: "lambda-sat-solver: Certified SAT middleware and frame-structured hardness research harness"
 authors:
@@ -17,8 +36,40 @@ keywords:
   - SAT
   - satisfiability
   - certified solving
+  - DRAT proof checking
+  - computational complexity
+  - resolution width
+  - Nullstellensatz degree
+  - lambda calculus
+references:
+  - type: article
+    authors:
+      - family-names: "Ben-Sasson"
+        given-names: "Eli"
+      - family-names: "Wigderson"
+        given-names: "Avi"
+    title: "Short proofs are narrow — resolution made simple"
+    year: 2001
+  - type: article
+    authors:
+      - family-names: "Clegg"
+        given-names: "Matthew"
+      - family-names: "Edmonds"
+        given-names: "Jeffery"
+      - family-names: "Impagliazzo"
+        given-names: "Russell"
+    title: "Using the Groebner basis algorithm to find proofs of unsatisfiability"
+    year: 1996
+  - type: article
+    authors:
+      - family-names: "Gomes"
+        given-names: "Carla P."
+      - family-names: "Selman"
+        given-names: "Bart"
+    title: "Heavy-tailed phenomena in satisfiability and constraint satisfaction problems"
+    year: 2000
   - DRAT
   - CDCL
   - proof checking
   - SAT hardness
-  - portfolio solving
+  - portfolio solving

CONTRIBUTING.md

@@ -1,5 +1,45 @@
 # Contributing
 
+Thanks for your interest. This repository has an unusual constitution, and contributions
+are judged by it. Read [`docs/CHARTER.md`](docs/CHARTER.md) first — it is the standard
+everything here is held to.
+
+## The one rule that matters: a name is not a proof
+
+Every claim must be labelled **proven**, **measured**, or **speculative**, and bound to
+something checkable — a theorem, a test, or a reproducible measurement. A pull request that
+adds a capability claim without a test or a reproduction is not ready, however elegant.
+
+- **Soundness is non-negotiable.** The frames and the certified paths must never emit a
+  wrong `SAT`/`UNSAT`. New frame logic needs a differential test against a trusted oracle
+  (brute force on small cases) and must *punt* (`CDCL_NEEDED`) rather than guess.
+- **Measure before you optimize.** Performance claims need a before/after measurement in a
+  script under `docs/ladder/scripts/`. Honest negatives are welcome and are recorded, not
+  hidden.
+- **Certification stays intact.** Anything that produces a verdict must keep it checkable:
+  SAT by model replay, UNSAT by a sound frame refutation or a DRAT proof.
+
+## Getting set up
+
+```bash
+pip install -e ".[dev,bench]"       # editable install + test/bench deps
+# external tools for full certification: install Kissat + drat-trim (see BACKEND_README.md)
+python -m pytest backend/tests -q   # the full suite must stay green
+```
+
+## Before opening a pull request
+
+1. `python -m pytest backend/tests -q` passes locally.
+2. New behaviour has a test; new/changed claims are labelled and reproducible.
+3. If you touched a benchmark claim, update [`REPRODUCIBILITY.md`](REPRODUCIBILITY.md) and
+   re-run the named command.
+4. Keep the voice honest and scoped — claims are bounded to the mix/axis they were measured
+   on, not generalized.
+
+## Style
+
+Match the surrounding code: its naming, comment density, and idiom. New research notes go
+under `docs/ladder/` and are linked from its index with a one-line, honest summary.
 Contributions are welcome, but this repository has a strict claim discipline.
 
 ## Core rule
@@ -43,4 +83,4 @@ python -m backend.cli examples/simple_unsat.cnf --mode strict
 
 ## Style
 
-Keep the public surface readable for a skeptical stranger. The poetic layer is allowed, but the first-contact path must make the executable claim clear before the metaphor.
+Keep the public surface readable for a skeptical stranger. The poetic layer is allowed, but the first-contact path must make the executable claim clear before the metaphor.

README.md

@@ -101,6 +101,13 @@ flowchart TD
 ```
 
 - **frame router** (`frame_solver.py`) — the three frames + their coupling, refute-first.
+- **metasolver** (`metasolver.py`) — reverts the dynamical description into a dispatch. On a
+  *counting-and-parity-inclusive mix* (not the competition set) it wins on PAR-2 over Kissat,
+  CaDiCaL and CryptoMiniSat — because it is instant where they blow up on counting, and
+  comparable elsewhere. A structural result on a specific mix, not a generally faster solver.
+- **meta-metasolver** (`metametasolver.py`) — the minimax mixed strategy; on the heavy-tailed
+  random-3SAT band it *out-searches CMS in wall-clock* (parallel, at a `k×` CPU cost, no CMS
+  in the pool). Single-thread on few cores, this advantage shrinks — see the honest scope.
 - **metasolver** (`metasolver.py`) — description-driven dispatch. On the included
   competition-style mix, its aggregate win comes from routing structured islands before
   CDCL, not from a claim of general CDCL dominance.
@@ -112,6 +119,10 @@ flowchart TD
 - **the view from outside** — `dynamics.py` (laws/relations/motions), `fabric.py` +
   `fabric_model.py` (the hyperbolic instance-manifold), `observer.py` (the adjudicator).
 
+> Every number here is a *measured* claim on a small, fixed, synthetic mix — regenerate it
+> with one command and read the scope in [`REPRODUCIBILITY.md`](REPRODUCIBILITY.md). This is
+> a certified middleware and a research harness, **not** a claim of a generally faster SAT
+> solver.
 For exact measured/proven/speculative status, read [`PUBLIC_RESEARCH_CLAIMS.md`](PUBLIC_RESEARCH_CLAIMS.md)
 and [`REPRODUCIBILITY.md`](REPRODUCIBILITY.md) before citing benchmark numbers.
 
@@ -169,6 +180,8 @@ assert r.certified                              # every verdict carries its proo
 ```
 backend/
   frame_solver.py      three sound frames + coupling (the router)
+  metasolver.py        description-driven dispatch  (beats CMS on the mix)
+  metametasolver.py    fractal portfolio           (out-searches CMS on the tail, parallel)
   metasolver.py        description-driven dispatch  (scoped benchmark mix)
   metametasolver.py    fractal portfolio           (scoped heavy-tail benchmark)
   acaf.py              adaptive actor-critic policy (cores-sized mixed strategy)

REPRODUCIBILITY.md

@@ -1,5 +1,66 @@
 # Reproducibility
 
+Every benchmark claim in this repository is a **repo-internal measured claim** on a stated
+mix, timeout, and environment — not an external competition result. This file gives the
+exact command, environment, and expected shape of each so you can regenerate it. Numbers
+are **hardware-sensitive** (wall-clock, core count); regenerate on your machine rather than
+trusting the absolute seconds.
+
+## Environment (as measured)
+
+| component | version |
+|---|---|
+| Python | 3.11 / 3.12 (CI matrix) |
+| numpy | 2.4.6 |
+| Kissat | 4.0.4 |
+| CaDiCaL | 3.0.0 |
+| CryptoMiniSat (`pycryptosat`) | 5.14.7 |
+| drat-trim | (DRAT proof checker) |
+| dev container | 4 vCPU (the portfolio/parallel numbers are core-bound — see below) |
+
+```bash
+pip install -e ".[dev,bench]"
+# external, non-pip: install Kissat + drat-trim (see BACKEND_README.md)
+python -m pytest backend/tests -q        # 650 tests; the soundness/certification floor
+```
+
+## The measured claims, and how to regenerate each
+
+Each row: the command, the timeout, and what the output should show. Instance lists are
+fixed in the harness (deterministic seeds); the JSON outputs are git-ignored so you can
+diff your run against the table.
+
+| claim | command | timeout | expected shape |
+|---|---|---|---|
+| **frame-aware middleware vs raw CDCL** | `python -m docs.ladder.scripts.sota_benchmark` | 20 s | middleware 40/40, PAR-2 ~0.05 s; Kissat 35/40 ~5.4 s; CaDiCaL 36/40 ~4.3 s; 40/40 certified; 26/40 frame-decided |
+| **vs CryptoMiniSat (four-way)** | `python -m docs.ladder.scripts.metasolver_benchmark` | 20 s | CMS 38/40, PAR-2 ~2.7 s; metasolver 40/40, PAR-2 ~0.05 s; CMS times out on php10/php12 (counting), metasolver instant there |
+| **out-search CMS on random-3SAT** | `python -m docs.ladder.scripts.metametasolver_benchmark` | 30 s | on the n=220–280 hard band, the fractal portfolio beats CMS wall-clock on the majority of instances (PAR-2 ~1.6×); loses trivial instances to launch overhead; CPU cost ≈ breadth× |
+| **NS degree vs width incomparable** | `python -m pytest backend/tests/test_ladder_contracts.py -k incomparable -q` | — | PHP (width 2, NS 4); Tseitin K4 (width 4, NS 3) — neither dominates |
+| **hard certification actually runs** | `python .github/scripts/certification_smoke.py` | — | "CERTIFICATION LANE PASSED": a CDCL UNSAT DRAT-checked and a CDCL SAT model-replayed |
+
+## How to interpret a discrepancy
+
+- **Solved-count differs.** Almost always a timeout/hardware difference. Solved-count is
+  robust; PAR-2 seconds are not — re-read them relative to *your* Kissat baseline, not ours.
+- **The portfolio does not beat CMS on your box.** Expected on ≤2 cores: the meta-metasolver
+  is a *parallel* mixed strategy; with few cores its arms contend and the wall-clock win
+  shrinks or vanishes. It is the `k×`-CPU-for-wall-clock trade, stated in
+  [`docs/ladder/GAME_THEORY_NOTE.md`](docs/ladder/GAME_THEORY_NOTE.md). The single-thread
+  claims (frames, metasolver on counting/parity) are core-independent.
+- **A frame verdict disagrees with a trusted solver.** That would be a **soundness bug** —
+  the one class we treat as critical. Please report it (see `SECURITY.md`) with the formula.
+
+## Scope of the claims (read this before quoting a number)
+
+These are measured on a **small, fixed, synthetic competition-style mix** (random-3SAT,
+Tseitin, XORSAT, pigeonhole, mixed), not the SAT Competition benchmark set. The honest
+one-line reading:
+
+> On a mix that includes the counting and parity fragments, the frame-aware middleware
+> dominates raw CDCL and CryptoMiniSat on PAR-2 because it is instant where they blow up
+> (counting) and comparable elsewhere; on the unstructured tail a parallel portfolio can
+> out-search CMS at a CPU cost. This is a *structural* result on a *specific mix* — not a
+> claim of a generally faster SAT solver.
 This repository has two separable surfaces:
 
 1. **Certified solving path** — every emitted SAT/UNSAT verdict is independently checked: SAT by model replay, UNSAT by a sound frame refutation or by `drat-trim` over a DRAT proof.
@@ -74,4 +135,4 @@ Before citing or announcing a result, check `PUBLIC_RESEARCH_CLAIMS.md` and `doc
 
 - **proven** means theorem-backed or sound-by-construction;
 - **measured** means benchmarked under stated scope;
-- **speculative** means a lens or research direction and is not load-bearing.
+- **speculative** means a lens or research direction and is not load-bearing.