Res($\oplus$) is the simplest fragment of $\text{AC}^0[2]\text{-Frege}$ for which no super-polynomial lower bounds on the size of proofs are known. Bhattacharya and Chattopadhyay [BC25] recently proved lower bounds of the form $\exp(\tilde\Omega(N^{\varepsilon}))$ on the size of Res($\oplus$) proofs whose depth is upper bounded by $O(N^{2 - \varepsilon})$, where $N$ is the number of variables in the unsatisfiable CNF formula. Their proof employs the ``random walk with restarts'' technique, which is unlikely to be used to prove lower bounds for proofs of depth greater than $N^2$. The next natural step would be to prove a lower bound for proofs of depth polynomial in the number of variables. In this work, we address this issue by proposing a new method for proving bounded-depth lower bounds.
We introduce a natural extension of the Bit Pigeon Hole Principle called the Constrained Bit Pigeon Hole Principle (CBPHP, for short), for which we will prove the following lower bounds:
- Under some natural combinatorial assumption, for any constant $k$, there is a collection of instances of CBPHP such that any Res$(\oplus)$ proof of CBPHP of depth $N^k$ requires size $\exp(N^{\Omega(1)})$.
- Unconditionally, for any constant $k$, there is a collection of instances of CBPHP such that any RevRes$(\oplus)$ proof of CBPHP of depth $N^k$ requires size $\exp(N^{\Omega(1)})$, where RevRes$(\oplus)$ is the fragment of Res$(\oplus)$ defined similarly to RevRes (See G\"{o}\"{o}s et. al [GHJ+24]).
- Unconditionally, for any small enough $\varepsilon > 0$ there is a collection of instances of CBPHP such that any Res$(\oplus)$ proof of CBPHP of depth $N^{2 - \varepsilon}$ requires size $\exp(N^{\Omega(\varepsilon)})$.