A solver that carries its own proof, and knows which shape of hardness it's looking at.
Headless. No web UI. No trust-me.
A λ-logic middleware for Boolean satisfiability that verifies every verdict it emits — SAT by model replay, UNSAT by an independent DRAT proof or a sound algebraic frame. On top of the solver sits a research program on the intrinsic shape of SAT hardness: three sound algebraic frames, a hyperbolic map of instance-space, and a game-theoretic dispatcher that reads an instance before it searches.
Kissat is a tool here, not an authority. A wrong answer is caught, not believed.
Two halves, one discipline.
The solver — a typed λ-DSL over sound frames and certified CDCL. Every result carries a checkable certificate.
The ladder — an honest study of where hardness lives, each claim bound to a test.
The stance is written down in docs/CHARTER.md. A name is not a proof.
Read it first.
An instance is described before it is solved. The description — laws (conserved invariants), relations (frame couplings), motions (its place on the hyperbolic fabric) — tells the actor which move to play.
flowchart TD
F([formula]) --> C{"critic — does frame<br/>+ geometry suffice?"}
C -->|"yes · structured island"| FR["<b>frame</b><br/>2-SAT · GF(2) · counting<br/>~0 ms · sound by construction"]
C -->|"no · tunnel"| H{"critic —<br/>heavy tail?"}
H -->|"light"| S["<b>single arm</b><br/>one engine · no swarm"]
H -->|"heavy"| P["<b>portfolio</b><br/>cores-sized · seed-diversified<br/>first certified arm wins"]
FR --> V([verdict])
S --> V
P --> V
V --> Z["<b>certified</b><br/>frame-sound · DRAT · model replay"]
Structure is decided instantly and for free — the frame is the certificate. Only the structureless tail reaches a solver, and even then the answer is re-checked.
Each obstruction has one sound, engine-independent frame. What escapes all three is not a failure of the map — it is a different region, and the map says so.
flowchart LR
subgraph ISLAND["island · structured"]
direction TB
I1["a <b>dominant strategy</b> exists"]
I2["the owning frame wins ~0 ms<br/>2-SAT · parity · counting"]
end
subgraph TUNNEL["tunnel · unstructured"]
direction TB
T1["<b>no</b> strategy dominates"]
T2["heavy-tailed runtime"]
T3["→ a <b>mixed strategy</b> (portfolio)"]
end
ISLAND -. "the decidability fold<br/>(a measured catastrophe wall)" .-> TUNNEL
The fold is not a metaphor — it is a Fisher–Rao metric singularity, measured in the natural
coordinate (docs/ladder/FABRIC_NOTE.md). It is also the line
where game theory flips: on the island a pure strategy dominates; on the tunnel you must
mix. Same boundary, two languages.
Every layer is the same operator seen at a different scale. Fractal, self-similar, and each verdict certified all the way down.
flowchart TD
ACAF["<b>ACAF</b> · adaptive actor-critic-ambigator-fuzzer"] --> META["<b>metasolver</b> · description-driven dispatch"]
ACAF --> MM["<b>meta-metasolver</b> · fractal seed-portfolio"]
META --> FR["<b>frame router</b> · 3 sound frames + Nelson-Oppen coupling"]
MM --> FR
META --> K["certified CDCL · Kissat / CaDiCaL"]
MM --> K
FR --> OBS(["<b>observer</b> — certify every verdict"])
K --> OBS
DESC["<b>the view from outside</b><br/>dynamics · fabric · hyperbolic model"] -.reads.-> ACAF
- 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 ak×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. - meta-metasolver (
metametasolver.py) — seed-diversified CDCL portfolio for the heavy-tailed random-3SAT band; measured in the repo's scoped benchmark, with CPU cost reported. - 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. This is a certified middleware and a research harness, not a claim of a generally faster SAT solver. For exact measured/proven/speculative status, readPUBLIC_RESEARCH_CLAIMS.mdandREPRODUCIBILITY.mdbefore citing benchmark numbers.
Kissat is not in the trusted base. The trusted core is small and independent:
- DIMACS parser · Tseitin transform
- model checker — replays SAT assignments against the original formula
- DRAT checker (
drat-trim) — replays UNSAT proofs with an independent tool
The three frames are sound by construction — no external checker, the derivation is
the proof. Only the CDCL fallback's UNSAT certificate needs drat-trim. Full
proven / measured / speculative ledger in
PUBLIC_RESEARCH_CLAIMS.md.
python -m pip install --upgrade pip
pip install -e .[dev]
# install Kissat + drat-trim for strict external certification; see BACKEND_README.md
python -m backend.cli examples/simple_sat.cnf --heuristic aggressive
python -m pytest backend/tests/ -qStrict certification smoke tests:
python -m backend.cli examples/simple_sat.cnf --mode strict
python -m backend.cli examples/simple_unsat.cnf --mode strictCLI install path:
lambda-sat examples/simple_sat.cnf --mode strictfrom backend.acaf import acaf_solve # the adaptive game-player
r = acaf_solve(formula) # frame · single · or portfolio
assert r.certified # every verdict carries its proofbackend/
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)
dynamics.py laws · relations · motions (the view from outside)
fabric.py the instance as a woven tapestry
fabric_model.py the family distributions, hyperbolic (Poincaré ball)
observer.py the adjudicator — certify, don't trust
lambda_sat.py λ ⊗ SAT fusion (β-reduce → CNF + remainder → decide)
{binary_clause,xor_extraction,cardinality}_check.py the three frames
complexity/ intrinsic hardness invariants + contracts
tests/ the full suite
docs/
CHARTER.md stance & claim discipline (read first)
ladder/ the research index, notes, and benchmarks
Research index: docs/ladder/README.md.
Per-invariant promises: docs/ladder/CONTRACTS.md.
Reproduction guide: REPRODUCIBILITY.md.
- Kissat · CaDiCaL — Armin Biere · CryptoMiniSat — Mate Soos
- DRAT / LRAT — certified UNSAT proof formats
- Gomes–Selman — heavy-tailed runtime & portfolios · von Neumann — the minimax theorem
- Ben-Sasson–Wigderson (width ↔ size) · Clegg–Edmonds–Impagliazzo (polynomial calculus) — the ladder's anchors
See LICENSE.