From 8b0a4b3f4860a32fd2ff566eca2c0c43d25e33bf Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 8 Jul 2026 10:32:45 +0000 Subject: [PATCH 1/2] Publication-hardening pass (external review) 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 Claude-Session: https://claude.ai/code/session_01Gkw2ccXyb4DEtqFo29ouQD --- .github/scripts/certification_smoke.py | 57 +++++++++++++++++++++++ .github/workflows/tests.yml | 41 ++++++++++++++++- .gitignore | 6 +++ CITATION.cff | 56 +++++++++++++++++++++++ CONTRIBUTING.md | 42 +++++++++++++++++ README.md | 18 ++++++-- REPRODUCIBILITY.md | 63 ++++++++++++++++++++++++++ SECURITY.md | 45 ++++++++++-------- backend/cli.py | 7 ++- docs/ladder/README.md | 10 ++-- pyproject.toml | 56 +++++++++++++++++++++++ 11 files changed, 369 insertions(+), 32 deletions(-) create mode 100644 .github/scripts/certification_smoke.py create mode 100644 CITATION.cff create mode 100644 CONTRIBUTING.md create mode 100644 REPRODUCIBILITY.md create mode 100644 pyproject.toml diff --git a/.github/scripts/certification_smoke.py b/.github/scripts/certification_smoke.py new file mode 100644 index 0000000..5ec8ea9 --- /dev/null +++ b/.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() diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index aa142c1..1e99ccf 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -6,7 +6,10 @@ on: pull_request: jobs: - test: + # 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: fail-fast: false @@ -27,9 +30,43 @@ jobs: # 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 CI stays green either way. + # 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 - 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: Install Python dependencies + 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 diff --git a/.gitignore b/.gitignore index 984b352..9764ecb 100644 --- a/.gitignore +++ b/.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__/ diff --git a/CITATION.cff b/CITATION.cff new file mode 100644 index 0000000..829850e --- /dev/null +++ b/CITATION.cff @@ -0,0 +1,56 @@ +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" +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 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..fc1f9f4 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,42 @@ +# 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. diff --git a/README.md b/README.md index f635263..1a9c4b5 100644 --- a/README.md +++ b/README.md @@ -101,15 +101,23 @@ flowchart TD ``` - **frame router** (`frame_solver.py`) — the three frames + their coupling, refute-first. -- **metasolver** (`metasolver.py`) — reverts the dynamical description into a dispatch; - beats every single solver, **CryptoMiniSat included**, on a competition mix (49× PAR-2). -- **meta-metasolver** (`metametasolver.py`) — the minimax mixed strategy; **out-searches CMS - on random-3SAT** by collapsing its heavy tail (no CMS in the pool). +- **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. - **ACAF** (`acaf.py`) — sizes the mixed strategy to the cores; wins the structured tier by a constructive certificate, the hard tier by an adaptive portfolio. - **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. + --- ## 証 · certification — the TCB @@ -152,7 +160,7 @@ 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) + metametasolver.py fractal portfolio (out-searches CMS on the tail, parallel) acaf.py adaptive actor-critic policy (cores-sized mixed strategy) dynamics.py laws · relations · motions (the view from outside) fabric.py the instance as a woven tapestry diff --git a/REPRODUCIBILITY.md b/REPRODUCIBILITY.md new file mode 100644 index 0000000..ab148e8 --- /dev/null +++ b/REPRODUCIBILITY.md @@ -0,0 +1,63 @@ +# 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. diff --git a/SECURITY.md b/SECURITY.md index 67a9cbf..70e9b6e 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -1,31 +1,36 @@ -Thanks for helping make GitHub safe for everyone. +# Security policy -# Security +This is a research library and CLI, not a network service. Its security surface is +unusual and worth stating plainly: the project's core promise is **soundness** — that a +verdict it certifies is correct. The most serious class of defect here is therefore not a +memory-safety bug but a **soundness bug**: a formula reported `SAT`/`UNSAT` (with +`certified = True`) whose verdict is wrong. -GitHub takes the security of our software products and services seriously, including all of the open source code repositories managed through our GitHub organizations, such as [GitHub](https://github.com/GitHub). +## Trusted computing base -Even though [open source repositories are outside of the scope of our bug bounty program](https://bounty.github.com/index.html#scope) and therefore not eligible for bounty rewards, we will ensure that your finding gets passed along to the appropriate maintainers for remediation. +By design, the external SAT solver (Kissat) is **not trusted**. Every verdict is +re-checked by a small, independent core: -## Reporting Security Issues +- SAT — the model is replayed against the original formula (`cnf_utils.verify_model`); +- UNSAT via a frame — sound by construction (2-SAT SCC, GF(2) refutation, counting bound); +- UNSAT via CDCL — the DRAT proof is replayed by `drat-trim` (LRAT optional). -If you believe you have found a security vulnerability in any GitHub-owned repository, please report it to us through coordinated disclosure. +A bug in Kissat, CaDiCaL, or CryptoMiniSat that produced a wrong answer would be **caught** +by this core, not trusted. A soundness-relevant bug is therefore one in the trusted core +itself (parser, Tseitin transform, model checker, the frame refutations, or the proof-checker +invocation). -**Please do not report security vulnerabilities through public GitHub issues, discussions, or pull requests.** +## Reporting a vulnerability -Instead, please send an email to opensource-security[@]github.com. +Please report privately rather than in a public issue: -Please include as much of the information listed below as you can to help us better understand and resolve the issue: +- Use **GitHub Security Advisories** ("Report a vulnerability") on this repository, or +- email the maintainer via the address on the GitHub profile of the repository owner. - * The type of issue (e.g., buffer overflow, SQL injection, or cross-site scripting) - * Full paths of source file(s) related to the manifestation of the issue - * The location of the affected source code (tag/branch/commit or direct URL) - * Any special configuration required to reproduce the issue - * Step-by-step instructions to reproduce the issue - * Proof-of-concept or exploit code (if possible) - * Impact of the issue, including how an attacker might exploit the issue +Please include a minimal reproducing formula and the observed vs expected verdict. A +witnessed soundness violation (a certified-but-wrong verdict) will be treated as the +highest priority. -This information will help us triage your report more quickly. +## Supported versions -## Policy - -See [GitHub's Safe Harbor Policy](https://docs.github.com/en/site-policy/security-policies/github-bug-bounty-program-legal-safe-harbor#1-safe-harbor-terms) +The project is pre-1.0; fixes land on the default branch. Pin a commit for reproducibility. diff --git a/backend/cli.py b/backend/cli.py index f116aff..47d9307 100644 --- a/backend/cli.py +++ b/backend/cli.py @@ -194,5 +194,10 @@ async def main(): sys.exit(1) -if __name__ == '__main__': +def cli_main(): + """Synchronous console-script entry point (see pyproject.toml).""" asyncio.run(main()) + + +if __name__ == '__main__': + cli_main() diff --git a/docs/ladder/README.md b/docs/ladder/README.md index 5f7a129..cbf8a44 100644 --- a/docs/ladder/README.md +++ b/docs/ladder/README.md @@ -10,8 +10,9 @@ and every rung says so. - **Two genuine hardness carriers, theorem-backed.** `min_refutation_width` (Ben-Sasson–Wigderson: width lower-bounds resolution size) and `nullstellensatz_degree` (Clegg–Edmonds–Impagliazzo: PC degree lower-bounds - PC size). They track but are *distinct*: NS ≥ width on every instance tested, - and PHP(3→2) separates them (NS 4 vs width 2). Both are exact and + PC size). They are related but **incomparable** — neither dominates: PHP(3→2) + has NS 4 > width 2, while Tseitin K4 has NS 3 < width 4 (measured, both + directions; test `test_ns_and_width_are_incomparable`). Both are exact and exponential — the right object is genuinely expensive. - **A clean, well-measured negative.** No cheap graph-structural scalar (`spectral_gap`, degree entropy, `signed_laplacian_frustration`) carries @@ -32,8 +33,9 @@ and every rung says so. ## What's proven vs open - **Proven / measured:** the two size lower bounds (BSW, CEI) as theorems the - carriers compute against; the Rung-1 negative on our own instances; NS ≥ width - with PHP separation; the char-2 collapse of the naive symmetry channel. + carriers compute against; the Rung-1 negative on our own instances; NS and + width **incomparable** (PHP 4>2, Tseitin K4 3<4); the char-2 collapse of the + naive symmetry channel. - **Open / next:** the ℝ-side **G₂-block-diagonalized moment/SOS matrix** on the same rank-deficiency operator — the one place the exceptional symmetry is a genuine computational lever rather than a name. diff --git a/pyproject.toml b/pyproject.toml new file mode 100644 index 0000000..4d7cdd2 --- /dev/null +++ b/pyproject.toml @@ -0,0 +1,56 @@ +[build-system] +requires = ["setuptools>=61.0", "wheel"] +build-backend = "setuptools.build_meta" + +[project] +name = "lambda-sat-solver" +version = "0.1.0" +description = "Certified λ-logic SAT middleware and a research harness for frame-structured SAT hardness" +readme = "README.md" +requires-python = ">=3.11" +license = { file = "LICENSE" } +authors = [{ name = "Jesús Vilela Franco" }] +keywords = [ + "SAT", "satisfiability", "solver", "certified", "DRAT", "proof-checking", + "Kissat", "CryptoMiniSat", "computational-complexity", "lambda-calculus", +] +classifiers = [ + "Development Status :: 4 - Beta", + "Intended Audience :: Science/Research", + "License :: OSI Approved :: MIT License", + "Programming Language :: Python :: 3.11", + "Programming Language :: Python :: 3.12", + "Topic :: Scientific/Engineering :: Mathematics", +] +dependencies = [ + "numpy>=1.24.0", + "pydantic>=2.0.0", + # CryptoMiniSat baseline used by backend/cms_wrapper.py and the benchmarks. + # It is a *competitor* the metasolver is measured against, not part of the + # certified solve path; kept as a core dep so the test suite runs as shipped. + "pycryptosat>=5.11.0", +] + +[project.optional-dependencies] +dev = ["pytest>=7.4.0", "pytest-asyncio>=0.21.0"] +bench = ["pycryptosat>=5.11.0"] + +[project.scripts] +lambda-sat = "backend.cli:cli_main" + +[project.urls] +Homepage = "https://github.com/jesusvilela/lambda-sat-solver" +Repository = "https://github.com/jesusvilela/lambda-sat-solver" +Issues = "https://github.com/jesusvilela/lambda-sat-solver/issues" + +# External, non-pip tools are required for full certification (not installable via +# pip): the Kissat SAT solver and the drat-trim DRAT checker (LRAT optional). +# The three sound frames are self-certifying and need neither. See BACKEND_README.md. + +[tool.setuptools.packages.find] +where = ["."] +include = ["backend*"] +exclude = ["backend.tests*"] + +[tool.pytest.ini_options] +testpaths = ["backend/tests"] From 3e0bfa211594b044b8021bda62d05278594264ed Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 8 Jul 2026 13:18:42 +0000 Subject: [PATCH 2/2] GitHub Pages front door (austere, certification-first ordering) 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 Claude-Session: https://claude.ai/code/session_01Gkw2ccXyb4DEtqFo29ouQD --- docs/_config.yml | 13 +++ docs/assets/architecture.mmd | 19 +++++ docs/benchmark-capsule.md | 75 +++++++++++++++++ docs/index.md | 151 +++++++++++++++++++++++++++++++++++ docs/technical-note.md | 116 +++++++++++++++++++++++++++ 5 files changed, 374 insertions(+) create mode 100644 docs/_config.yml create mode 100644 docs/assets/architecture.mmd create mode 100644 docs/benchmark-capsule.md create mode 100644 docs/index.md create mode 100644 docs/technical-note.md diff --git a/docs/_config.yml b/docs/_config.yml new file mode 100644 index 0000000..76a8717 --- /dev/null +++ b/docs/_config.yml @@ -0,0 +1,13 @@ +# Minimal GitHub Pages config — austere by intent (plain Markdown, no theatre). +# Serve from /docs on the default branch: Settings → Pages → Source: main /docs. +title: λSAT +description: >- + Certified frame-first SAT middleware — structured regions before CDCL, + certified verdicts after every path. +theme: jekyll-theme-minimal +show_downloads: false + +# Keep the research subtrees out of the built site index (still browsable on GitHub). +exclude: + - vdis/ + - __pycache__/ diff --git a/docs/assets/architecture.mmd b/docs/assets/architecture.mmd new file mode 100644 index 0000000..b638e47 --- /dev/null +++ b/docs/assets/architecture.mmd @@ -0,0 +1,19 @@ +%% λSAT architecture — the certified frame-first router. +%% Source of truth for the diagram; renders on github.com and via mermaid-cli. +flowchart TD + F([formula]) --> R{router} + R -->|"binary clauses"| IMP["implication frame (2-SAT)
SCC contradiction / assignment"] + R -->|"XOR structure"| PAR["parity frame (GF(2))
Gaussian refutation / model"] + R -->|"pigeonhole shape"| CNT["counting frame (ℤ)
k > m magnitude contradiction"] + R -->|"none of the above"| CDCL["CDCL fallback (Kissat)"] + + IMP --> OBS([observer — certify]) + PAR --> OBS + CNT --> OBS + CDCL -->|"UNSAT: DRAT replay
SAT: model replay"| OBS + OBS --> V([certified verdict]) + + classDef frame fill:#eef,stroke:#557; + classDef fallback fill:#fee,stroke:#755; + class IMP,PAR,CNT frame; + class CDCL fallback; diff --git a/docs/benchmark-capsule.md b/docs/benchmark-capsule.md new file mode 100644 index 0000000..e721fe5 --- /dev/null +++ b/docs/benchmark-capsule.md @@ -0,0 +1,75 @@ +--- +title: "Benchmark capsule" +--- + +# Benchmark capsule + +Every number here is a **measured** claim on a small, fixed, synthetic mix — **not** the SAT +Competition set, and **not** a claim of general CDCL dominance. Numbers are hardware-sensitive +(wall-clock, core count); regenerate on your machine. Commands and pinned versions: +[REPRODUCIBILITY.md](https://github.com/jesusvilela/lambda-sat-solver/blob/main/REPRODUCIBILITY.md). + +## Setup + +| | | +|---|---| +| **engines** | Kissat 4.0.4 · CaDiCaL 3.0.0 · CryptoMiniSat 5.14.7 (pycryptosat) | +| **families** | random-3SAT (α≈4.26) · Tseitin/XOR · XORSAT · pigeonhole (PHP) · mixed | +| **timeout** | 20 s (main mix) · 30 s (random-3SAT tail study) | +| **hardware** | 4 vCPU dev container (portfolio numbers are core-bound) | +| **metric** | solved-count and PAR-2 (timeout counts as 2×) | +| **certification** | every middleware verdict: SAT model-replayed, UNSAT frame-sound or DRAT | + +## Main mix — frame-aware middleware vs raw CDCL and CMS + +`python -m docs.ladder.scripts.metasolver_benchmark` · 40 instances · 20 s + +| family | n | Kissat | CaDiCaL | CryptoMiniSat | **middleware** | +|---|---|---|---|---|---| +| random-3SAT | 9 | 9/9 · 0.12 s | 9/9 · 0.13 s | 9/9 · 0.18 s | 9/9 · 0.23 s | +| Tseitin (parity) | 9 | 5/9 · 18.98 s | 5/9 · 18.83 s | 9/9 · 0.95 s | **9/9 · 0.00 s** | +| XORSAT | 12 | 12/12 · 0.00 s | 12/12 · 0.00 s | 12/12 · 0.00 s | 12/12 · 0.00 s | +| PHP (counting) | 4 | 3/4 · 10.77 s | 4/4 · 0.12 s | **2/4 · 24.51 s** | **4/4 · 0.00 s** | +| mixed | 6 | 6/6 · 0.00 s | 6/6 · 0.00 s | 6/6 · 0.00 s | 6/6 · 0.01 s | +| **total** | 40 | 35/40 · 5.38 s | 36/40 · 4.28 s | 38/40 · 2.71 s | **40/40 · 0.05 s** | + +CryptoMiniSat is the strongest baseline (38/40): its Gaussian engine **owns parity** (9/9 +Tseitin, where the raw CDCL engines get 5/9). It carries **no counting engine**, so +pigeonhole is exponential for it (php10/php12 time out) while the counting frame is instant. + +## Random-3SAT tail — the honest tunnel + +`python -m docs.ladder.scripts.metametasolver_benchmark` · n=220–280 · 30 s + +| solver | solved | PAR-2 (wall) | +|---|---|---| +| single Kissat (1 core) | 15/16 | ~5.3 s | +| CryptoMiniSat (1 core) | 14/16 | 10.01 s | +| fractal portfolio (~nproc cores) | 15/16 | 6.22 s — beats CMS wall-clock on 13/16 | + +The portfolio's advantage over CMS is a **parallel, mixed-strategy** effect (heavy-tailed +runtime collapsed by diversified seeds), paid for in `k×` CPU. On few cores it shrinks. It is +**not** a smarter search, and it does **not** beat a single strong Kissat by much on this box. + +## What improves + +- **Counting**: instant certified refutation where CDCL and CMS are exponential (PHP). +- **Parity**: instant certified verdict; even CMS's Gaussian engine is matched or beaten in + wall-clock by the direct GF(2) refutation. +- **Aggregate PAR-2 on this mix**: dominated by the structured families the frames own. + +## What does **not** improve + +- **Random-3SAT**: no exposed frame; the middleware falls to CDCL and is only *comparable* — + CMS is competitive-to-faster there. This is CDCL's territory and stays that way. +- **Single-thread on obfuscated structure**: if the XOR/counting structure is hidden from the + cheap detectors, the frame does not fire. +- **Trivial instances under certification**: the DRAT proof of a trivial CDCL UNSAT can cost + more than the solve — an uncertified solver returns faster. That is the price of proof, and + it is intentional. + +## One-line reading + +> On a mix that includes the counting and parity fragments, certified frame routing decides +> the structured islands instantly and provably, and hands the unstructured tail to CDCL. The +> advantage is structural and scoped — not a generally faster SAT solver. diff --git a/docs/index.md b/docs/index.md new file mode 100644 index 0000000..b462440 --- /dev/null +++ b/docs/index.md @@ -0,0 +1,151 @@ +--- +title: "λSAT — Certified Frame-First SAT Middleware" +description: "Structured regions before CDCL. Certified verdicts after every path." +--- + +# λSAT + +### Certified frame-first SAT middleware + +*Structured regions before CDCL. Certified verdicts after every path.* + +λSAT is a certified SAT middleware. **It does not try to replace CDCL.** It first checks +whether a formula belongs to one of several structured regions with sound algebraic +certificates — implication, parity, or counting — and falls back to CDCL otherwise. Every +emitted verdict is independently checked. + +That is the whole recognizer. The geometry comes later, and only as a map. + +--- + +## 1 · The question + +Modern SAT solvers are extremely strong, but a solver's *output* is not by itself an +*explanation*. λSAT asks a smaller, answerable question: + +> Can some structured SAT regions be recognized and certified **before** search, while the +> unstructured tail is handed honestly to CDCL? + +This deliberately avoids the dangerous claim of "a new solver that beats SOTA." + +--- + +## 2 · Certification — the trusted computing base + +This is the part that matters most. + +- **SAT** is checked by **model replay** against the original formula. +- **UNSAT** is checked by either a **sound frame refutation** (self-certifying) or an + **independent DRAT proof replay** (`drat-trim`). +- **Kissat, CaDiCaL, CryptoMiniSat are tools, not trusted authorities.** + +The middleware can be wrong only if a *checker or a frame* is wrong — never merely because +an external solver said so. A wrong answer from the engine is **caught, not believed.** + +``` +formula + │ + ▼ +router ── implication? ─ yes ─▶ 2-SAT frame ─────┐ + │ parity? ─ yes ─▶ GF(2) frame ─────┤ + │ counting? ─ yes ─▶ counting frame ──┤ sound by construction + │ │ + └── none of the above ─────▶ CDCL (Kissat) ─────┤ DRAT / model replay + ▼ + certified verdict +``` + +--- + +## 3 · The three frames + +Each structured region has one sound, engine-independent frame, with an input condition, a +certificate, and an honest failure mode (it *punts* to CDCL rather than guessing). + +| frame | structure | certificate | +|---|---|---| +| **implication** | 2-SAT / implication graph | SCC contradiction, or an assignment | +| **parity** | GF(2) / XOR structure | linear-algebra refutation or model | +| **counting** | pigeonhole / cardinality | an arithmetic (magnitude) contradiction | +| **fallback** | general SAT | CDCL + model replay / DRAT | + +The contribution is **not** replacing CDCL. It is **deciding structured islands before +CDCL, and certifying every emitted verdict.** + +--- + +## 4 · What the benchmark claims — and doesn't + +The benchmark claim is **scoped to the included mix** (a small, fixed, synthetic set: +2-SAT, Tseitin/XOR, pigeonhole, random-3SAT, mixed). It does **not** imply general CDCL +dominance. + +| family | why hard for CDCL | λSAT route | result shape | +|---|---|---|---| +| 2-SAT / implication | implication closure | implication frame | instant · certified | +| Tseitin / XOR | parity obstruction | GF(2) frame | instant · certified | +| PHP / counting | cardinality obstruction | counting frame | instant · certified | +| random-3SAT | no exposed frame | CDCL / portfolio | **CDCL remains central** | + +Numbers (PAR-2, per-family) live in the [benchmark capsule](benchmark-capsule.md), not on +this page — the headline is the *routing and certification*, not a speed record. + +--- + +## 5 · What it does **not** claim + +- It does **not** solve SAT hardness. +- It does **not** dominate CDCL on arbitrary SAT. +- It does **not** claim CryptoMiniSat is weak on XOR (CMS owns parity; the frame merely + re-derives it with a certificate). +- It does **not** make external solvers trusted. +- The hyperbolic / fabric layer is a **research map**, not part of the minimal certification + claim. + +--- + +## 6 · Reproduce + +```bash +git clone https://github.com/jesusvilela/lambda-sat-solver +cd lambda-sat-solver +pip install -e ".[dev]" +python -m pytest backend/tests/ -q # the soundness / certification floor +``` + +The certified strict path (requires Kissat + `drat-trim`): + +```bash +python -m backend.cli examples/simple_sat.cnf --mode strict # SAT, model-replayed +python -m backend.cli examples/simple_unsat.cnf --mode strict # UNSAT, checked +``` + +Full environment, pinned versions, and per-benchmark commands: +[REPRODUCIBILITY.md](https://github.com/jesusvilela/lambda-sat-solver/blob/main/REPRODUCIBILITY.md). + +--- + +## 7 · The research ladder (a map, not a proof) + +Only after the engineering is clear: the research layer studies *where SAT hardness lives* — +resolution width, Nullstellensatz degree, parity, counting, symmetry, and heavy-tailed +search. Honestly: + +- resolution width and Nullstellensatz degree are **incomparable** (neither dominates); +- cheap graph-structural scalars **failed** to carry random-3SAT hardness; +- the geometry is used as a **routing / modeling lens**, not as proof by metaphor. + +Index: [`docs/ladder/`](ladder/). Claim discipline: [`docs/CHARTER.md`](CHARTER.md). + +--- + +## Links + +- [Repository](https://github.com/jesusvilela/lambda-sat-solver) +- [Technical note](technical-note.md) · [Benchmark capsule](benchmark-capsule.md) +- [Reproducibility](https://github.com/jesusvilela/lambda-sat-solver/blob/main/REPRODUCIBILITY.md) + · [Claim ledger](https://github.com/jesusvilela/lambda-sat-solver/blob/main/PUBLIC_RESEARCH_CLAIMS.md) +- [Security policy](https://github.com/jesusvilela/lambda-sat-solver/blob/main/SECURITY.md) + · [Citation](https://github.com/jesusvilela/lambda-sat-solver/blob/main/CITATION.cff) + +*Route when structure is sufficient. Search when it is not. Verify either way.* diff --git a/docs/technical-note.md b/docs/technical-note.md new file mode 100644 index 0000000..a762d5d --- /dev/null +++ b/docs/technical-note.md @@ -0,0 +1,116 @@ +--- +title: "Structured Islands Before CDCL — A Certified SAT Middleware" +--- + +# Structured Islands Before CDCL + +### A certified SAT middleware + +*A narrow, reviewable note: here is the executable claim, here is the certification +boundary, here is where CDCL remains sovereign.* + +## Abstract + +λSAT is a headless SAT middleware that decides *structured* formulas before search and +hands the rest to CDCL. A router tries three sound, engine-independent frames — +implication (2-SAT), parity (GF(2)/XOR), and counting (pigeonhole/cardinality) — and their +cross-frame coupling; a formula that lives in one is decided with a certificate and no +search. Anything else returns `CDCL_NEEDED` and is solved by Kissat. **Every emitted verdict +is independently checked**: SAT by model replay, UNSAT by a sound frame refutation or a +`drat-trim` DRAT proof. The external solver is never a trusted authority. The benchmark +claim is scoped to a small synthetic mix that includes the counting and parity fragments; +it is a statement about *certified frame routing*, not about generally out-searching CDCL. + +## 1 · Motivation + +SAT solvers are powerful, and getting a formula *solved* is rarely the problem. The problem +addressed here is narrower: some formulas carry structure whose contradiction is decidable +by a short algebraic argument **before** any search, and that argument is its own +certificate. λSAT separates that structured decision from unstructured search, and — the +non-negotiable part — verifies whatever it emits. + +## 2 · Architecture + +``` +formula → router → { implication | parity | counting | coupling } → verdict → observer + └───────────── else: CDCL_NEEDED ──────────→ Kissat → observer +``` + +The router is refute-first (cheap near-linear refutation before any model reconstruction). +The observer is the certification stage: it accepts a verdict only with a checkable +certificate. `strict` mode requires the external tools to be present at startup and turns an +uncertified fallback verdict into an error; `dev`/`research` modes degrade to best-effort. + +## 3 · The three frames + +Each frame has an **input condition**, a **certificate**, and a **failure mode** (it must +punt, never guess). + +- **Implication (2-SAT).** Condition: binary clauses. Certificate: a strongly-connected + component placing a variable and its negation together (a sound UNSAT), or a satisfying + assignment. Failure: no binary contradiction → punt. +- **Parity (GF(2)).** Condition: recoverable XOR constraints. Certificate: Gaussian + elimination reaching `0 = 1` (UNSAT), or a reconstructed, re-verified model. Failure: + parity does not cover the formula / underdetermined → punt. +- **Counting (ℤ).** Condition: pigeonhole-shaped `k` disjoint at-least-one clauses covered + by `m < k` at-most-one cliques. Certificate: the magnitude contradiction `k > m`. Failure: + structure absent → punt. + +The **coupling** exchanges entailed literals across frames to a fixpoint (Nelson–Oppen), so +an instance no single frame decides can still be decided soundly; it too only emits UNSAT via +a channel refutation or SAT via a verified model. + +## 4 · Certification boundary + +| | trusted | not trusted | +|---|---|---| +| components | DIMACS parser · Tseitin transform · model checker · the three frame refutations · the DRAT-checker invocation | Kissat · CaDiCaL · CryptoMiniSat | + +- **SAT** → the assignment is replayed against the original clauses. +- **UNSAT via a frame** → sound by construction (no external checker). +- **UNSAT via CDCL** → the DRAT proof is replayed by `drat-trim` (LRAT optional). + +A CI lane (`certification-hard`) makes Kissat + `drat-trim` mandatory and fails red unless a +real DRAT UNSAT check and a real model-replay SAT check both execute. + +## 5 · Benchmark capsule + +Full detail in the [benchmark capsule](benchmark-capsule.md). In one paragraph: on a fixed +synthetic mix (random-3SAT, Tseitin, XORSAT, pigeonhole, mixed; 20 s timeout), the +frame-aware middleware decides the structured families instantly and certified, while raw +CDCL and CryptoMiniSat spend seconds or time out on the parity/counting families. On the +unstructured random-3SAT tail the middleware falls to CDCL and is **comparable**, not +better. The aggregate PAR-2 advantage is therefore a *structural* effect of the mix, not a +faster search. + +## 6 · Interpretation + +- **Frame-decidable islands** vs the **CDCL tunnel** — a formula either exposes an algebraic + obstruction (decide + certify) or it does not (search). +- A parallel, seed-diversified **portfolio** helps only on the heavy-tailed tail, and only by + spending cores for wall-clock; it is a mixed strategy, not a smarter search. +- **No-Free-Lunch holds.** There is no general dominance here, and none is claimed. + +## 7 · Limitations + +- The benchmark mix is **not** the SAT Competition set. +- Frames fire **only** when structure is exposed; obfuscated structure is missed. +- Random-3SAT is, and remains, **CDCL territory**. +- Strict-mode UNSAT via the fallback still requires external proof tooling (`drat-trim`). + +## 8 · Reproduction + +```bash +pip install -e ".[dev]" +python -m pytest backend/tests/ -q +python .github/scripts/certification_smoke.py # forces a real DRAT + model-replay check +``` + +Pinned versions, per-benchmark commands, and how to read a discrepancy: +[REPRODUCIBILITY.md](https://github.com/jesusvilela/lambda-sat-solver/blob/main/REPRODUCIBILITY.md). + +## 9 · Conclusion + +λSAT is a claim-discipline artifact as much as a solver: **route when structure is +sufficient, search when it is not, verify either way.** The interesting object is the +certified boundary between the two — not a speed record.