pub enum ProofRung {
Trivial,
Counting,
Parity,
ModCount {
p: u64,
},
Nullstellensatz {
min_degree: usize,
},
BeyondBudget,
}Expand description
Where an UNSAT instance sits in the proof-complexity landscape, as our certified cuts see it.
This is a ladder of proof systems (Cook–Reckhow): each rung crushes families the cheaper ones are
blind to. Counting and Parity are incomparable narrow detectors — pigeonhole needs counting
and is invisible to GF(2); Tseitin needs GF(2) and is invisible to counting — while
Nullstellensatz{min_degree} is the universal algebraic height over GF(2), complete at degree n.
The honest face of the wall: an instance whose narrow cuts are silent and whose minimum NS degree is
large sits at the top of this ladder, and the cost at that height is exponential. We can locate an
instance on the ladder; we cannot prove the top rung is unavoidable for a family — that lower bound is
exactly P vs NP, and it stays open.
Variants§
Trivial
Closed by unit propagation / carving alone — no real refutation needed.
Counting
A counting / Hall (pigeonhole) cut crushes it. Resolution-exponential families like PHP live here;
incomparable to Parity.
Parity
A GF(2) parity (Gaussian-elimination) cut crushes it. Tseitin / XOR families live here;
incomparable to Counting.
ModCount
A certified mod-p Gaussian cut crushes it — Parity carried to the odd prime p: the CNF is a
recognized one-hot encoding of a GF(p) linear system whose refutation re-checks. One rung per
characteristic, each incomparable to the others and to Counting/Parity (the prime
incomparability of polycalc_gfp). Reported only by the extended cascade
(weakest_crushing_rung_with_char); the legacy cascade predates the characteristic axis.
Nullstellensatz
No narrow cut fires; refuted only by Nullstellensatz / Polynomial Calculus over GF(2) at this minimum degree — the universal algebraic height. The rigid residue lives here.
BeyondBudget
No cut and no NS refutation within the degree budget — the wall as our detectors perceive it.