Exponential complexity lower bound proved for bit pigeonhole principle proofs
An exponential lower bound for the bit pigeonhole principle in resolution over parities
Computational ComplexityLogic in Computer Science
Summary
The authors showed that any logical proof method called resolution over parities needs an extremely large number of steps to prove a basic counting puzzle known as the bit pigeonhole principle. This means these proofs cannot be made efficient by restricting their structure. The finding uses advanced math and computer-assisted verification to confirm the result rigorously. Such limits help us understand why some logic puzzles are inherently hard for certain automated reasoning methods.
What this means in practice
- •For proof system developers: Recognize intrinsic inefficiencies in resolution over parities when proving pigeonhole principle variations, guiding design of more efficient proof systems.
- •For automated reasoning engineers: Avoid relying on resolution over parities for problems encoding pigeonhole-like constraints, improving solver performance by selecting more suitable methods.
A theory result. No direct application yet.
Authors
Kamil Braun
Abstract
Resolution over parities, $\mathrm{Res}(\oplus)$, is the characteristic-two version of resolution over linear equations: clauses are disjunctions of affine equations over $\mathbb F_2$. Superpolynomial size lower bounds were previously known only for restricted refutations: tree-like, regular, or of bounded depth. We prove that every DAG-like $\mathrm{Res} (\oplus)$ refutation of the bit pigeonhole principle with $n+1$ pigeons and $n=2^\ell$ holes has more than $\exp(n/(32768\ell^2))=2^{Ω(n/\log^2 n)}$ clauses, for every $\ell\ge32$, with no restriction on regularity or depth. The proof translates an arbitrary refutation with $S$ clauses into a polynomial calculus refutation of degree $O(\log n)$ over $O(S+n^2)$ groups of extension variables in the style of Buss, Impagliazzo, Krajicek, Pudlak, Razborov, and Sgall. One substitution then removes all extension variables at once and leaves a nonzero low-degree polynomial derived from the pigeonhole axioms alone at degree at most $n/2$; a degree lower bound in the style of Razborov, proved through the homology of chessboard complexes, shows that no such derivation exists. The argument also yields a general sufficient condition for $\mathrm{Res}(\oplus)$ size lower bounds. The main theorem, this condition, and all their dependencies are formalized in Lean 4, and every statement links to its formal proof. The proof was developed with substantial AI assistance within an open research framework described in the final section.