Certified frame-first SAT middleware — structured regions before CDCL, certified verdicts after every path.
A narrow, reviewable note: here is the executable claim, here is the certification boundary, here is where CDCL remains sovereign.
λ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.
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.
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.
Each frame has an input condition, a certificate, and a failure mode (it must punt, never guess).
0 = 1 (UNSAT), or a reconstructed, re-verified model. Failure:
parity does not cover the formula / underdetermined → punt.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.
| trusted | not trusted | |
|---|---|---|
| components | DIMACS parser · Tseitin transform · model checker · the three frame refutations · the DRAT-checker invocation | Kissat · CaDiCaL · CryptoMiniSat |
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.
Full detail in the benchmark capsule. 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.
drat-trim).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.
λ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.