Lower Bounds for Bit Pigeonhole Principles in Bounded-Depth Resolution over Parities

TL;DR

This work establishes exponential-size lower bounds for Res$(\oplus)$ proofs of the bit pigeonhole principle and its generalizations at depth regimes up to near-quadratic in the formula size, by developing a robust framework of affine DAGs, safe closures, and parity Decision-Tree (PDT) analysis. The authors introduce a lifting theorem that transfers lower bounds from bounded-depth Res$(\oplus)$ proofs to larger-depth lifted formulas using constant-size stifling gadgets, enabling superlinear depth lower bounds for complex constructions such as lifted PHP and Tseitin over expanders. They also prove NP-hard–looking lower bounds for multicollision-finding and collision-finding problems under randomized parity decision trees, yielding depth lower bounds that are tight up to polylog factors in constant-error regimes. By combining these PDT-hardness results with the lifting framework and existing DT-hardness results for expander-based Tseitin contradictions, they produce new size-depth lower bounds for Res$(\oplus)$ that are previously inaccessible, significantly advancing understanding of the power and limits of parity-based proof systems. Overall, the paper binds together PDT analyses, affine restriction techniques, and lifting to deliver robust exponential lower bounds for a broad family of pigeonhole-like CNF formulas, with implications for algorithmic search problems in TFNP and related complexity landscapes.

Abstract

We prove lower bounds for proofs of the bit pigeonhole principle (BPHP) and its generalizations in bounded-depth resolution over parities (Res$(\oplus)$). For weak BPHP$_n^m$ with $m = cn$ pigeons (for any constant $c>1$) and $n$ holes, for all $ε>0$, we prove that any depth $N^{1.5 - ε}$ proof in Res$(\oplus)$ must have exponential size, where $N = cn\log n$ is the number of variables. Inspired by recent work in TFNP on multicollision-finding, we consider a generalization of the bit pigeonhole principle, denoted $t$-BPHP$_n^m$, asserting that there is a map from $[m]$ to $[n]$ ($m > (t-1)n$) such that each $i \in [n]$ has fewer than $t$ preimages. We prove that any depth $N^{2-1/t-ε}$ proof in Res$(\oplus)$ of $t$-BPHP$_n^{ctn}$ (for any constant $c \geq 1$) must have exponential size. For the usual bit pigeonhole principle, we show that any depth $N^{2-ε}$ Res$(\oplus)$ proof of BPHP$_n^{n+1}$ must have exponential size. As a byproduct of our proof, we obtain that any randomized parity decision tree for the collision-finding problem with $n+1$ pigeons and $n$ holes must have depth $Ω(n)$, which matches the upper bound coming from a deterministic decision tree. We also prove a lifting theorem for bounded-depth Res$(\oplus)$ with a constant size gadget which lifts from $(p, q)$-DT-hardness, recently defined by Bhattacharya and Chattopadhyay. By combining our lifting theorem with the $(Ω(n), Ω(n))$-DT-hardness of the $n$-variate Tseitin contradiction over a suitable expander, proved by Bhattacharya and Chattopadhyay, we obtain an $N$-variate constant-width unsatisfiable CNF formula with $O(N)$ clauses for which any depth $N^{2-ε}$ Res$(\oplus)$ proof requires size $\exp(Ω(N^ε))$. Previously no superpolynomial lower bounds were known for Res$(\oplus)$ proofs when the depth is superlinear in the size of the formula.

Theorems & Definitions (81)

• Theorem 1.1
• Theorem 1.2
• Theorem 1.3
• Theorem 1.4
• Remark 1.5
• Theorem 1.6
• Corollary 1.7
• Theorem 3.1: egi24
• Lemma 3.2: egi24
• Lemma 3.3