The resolution wall, measured three ways

The pigeonhole principle — n pigeons into n-1 holes — needs a resolution refutation of size 2^Ω(n) (Haken 1985), and every CDCL solver inherits that wall. We measured it on a byte-identical formula (i9-14900K, release); external solvers run as subprocesses emitting a clausal proof (solve + certify, like ours):

  • PHP(16): ours 14.5 ms (120-step proof) · Z3 timeout · Kissat timeout · SaDiCaL 53 ms (242 KB proof)
  • PHP(28): ours 238 ms (378-step) · Z3 timeout · Kissat timeout · SaDiCaL 977 ms (4.2 MB)
  • PHP(40): ours 1.6 s (780-step) · Z3 timeout · Kissat timeout · SaDiCaL 7.4 s (25 MB)

Z3 (10 s cap) and Kissat (15 s cap) — the CDCL world champion — cannot even finish PHP(16). SaDiCaL, the reference symmetry/PR solver, *does* complete (no timeout inflation) — and there our certified SR (substitution-redundancy) proof is several× faster, with a certificate of exactly n(n-1)/2 steps against SaDiCaL's growing megabytes.

A different proof system, not a faster engine

Resolution (RUP/DRAT) ⊊ PR ⊊ SR. Kissat lives at resolution — exponential on pigeonhole. We live at SR — polynomial. Each SR step deletes a whole symmetry orbit with one certified clause whose witness *is* the symmetry, collapsing the exponential search into a polynomial proof. The certificate is exactly quadratic, every time — you can count it.

Two more families round out the section, each a different collapse:

  • Mutilated chessboard (matching): a colour-count Hall witness in microseconds on sparse, irregular adjacency. By 18×18 *all three* — Z3, Kissat and SaDiCaL — hit the wall; ours stays at 0.24 ms.
  • Tseitin parity on an expander (linear algebra): Gaussian elimination over GF(2), flat at ~10 µs. At n=90 Z3 walls and Kissat/SaDiCaL grind to seconds with multi-megabyte proofs.

SDCL: discover the proof with zero hints

The apex: handed only raw clauses — no symmetry hint, no construction — our SDCL *discovers* the certified proof itself. PHP(5) → 40 self-discovered PR clauses, PHP(6) → 60, PHP(7) → 84, each driving the search to zero conflicts.

Honest boundaries

Random 3-SAT is the control: no structure to exploit, ours tracks Kissat within milliseconds, and SaDiCaL — tuned for structure — fares poorly; we claim no win there. Sub-millisecond comparisons carry external process-startup overhead, so the headline rests on the cases where a competitor takes seconds or hits the wall. Proofs are emitted in DRAT/DPR and accepted by the community checkers (drat-trim / dpr-trim).

It runs in your browser

The proof engine is pure Rust and compiles to WASM unchanged — Z3, Kissat and SaDiCaL are only the comparison oracles in the native benchmark. The Studio's Hardware mode ships a live pigeonhole demo: type pigeons: 6, watch the last pigeon find no home, and read the certified verdict computed in the browser. The benchmark and the demo are the same prover.