23 August 2026
A Proof System Gap, Not a Tuning Trick
Some problems are not hard because a solver is untuned. They are hard because the proof system it works in has no short proof to find. That distinction decides whether an engineering effort is worth making.
A lower bound, not a benchmark
In 1985 Haken proved that resolution proofs of the pigeonhole principle grow exponentially with the number of holes. Not slowly, and not for a particular implementation. Any resolution proof of that family is exponentially large, so no amount of engineering finds a short one, because there is no short one to find.
Nearly every production SAT solver, and every SMT solver built on one, works in resolution or something close to it. That is not a design flaw. It's a proof system with a known ceiling, and these families sit above it.
The numbers
The pigeonhole principle at 16 holes, every solver given the same byte identical input.
| Solver | Time | Artifact |
|---|---|---|
| LOGOS | 13.7 ms | 25 KB certificate |
| SaDiCaL | 56.5 ms | 242 KB proof |
| Z3 | did not finish | 10 s limit |
| Kissat | did not finish | 15 s limit |
| CaDiCaL | did not finish | 15 s limit |
| CryptoMiniSat | did not finish | 15 s limit |
Intel Core i9-14900K, median of five runs, each competing solver writing its proof to disk. Kissat 4.0.4, CaDiCaL 3.0.0, CryptoMiniSat 5.11.21.
Where the advantage comes from
On structured families with symmetry or algebraic content, working in a stronger proof system decides problems that resolution cannot finish at any size. The benchmark set includes random 3-SAT as a control, where there is no structure to exploit.
Why this matters for silicon
A proof obligation is only worth stating if it can be discharged inside a build. A prover that takes seconds on the structured problems verification actually produces is a prover nobody runs on every commit, and an obligation nobody checks is a comment.
Milliseconds with a certificate that is re-checked is what makes proof an ordinary build step rather than an occasional exercise.
Source: Full families and methodology, logicaffeine.com(opens in a new tab)