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

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 $\hat{I}\mu >0$, we prove that any depth $N^{1.5-\hat{I}\mu }$ 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-\hat{I}\mu }$ proof in Res$(\oplus )$ of $t$-BPHP${}_n^{ctn}$ (for any constant $c\ge 1$) must have exponential size. For the usual bit pigeonhole principle, we show that any depth $N^{2-\hat{I}\mu }$ 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 $\hat{I}\text{c◯}(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 $(\hat{I}\text{c◯}(n),\hat{I}\text{c◯}(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-\hat{I}\mu }$ Res$(\oplus )$ proof requires size $\exp (\hat{I}\text{c◯}(N^{\hat{I}}\mu ))$. Previously no superpolynomial lower bounds were known for Res$(\oplus )$ proofs when the depth is superlinear in the size of the formula.

An earlier version containing one of the results appeared as ECCC TR25-118