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

TL;DR

This paper establishes exponential lower bounds for bounded-depth resolution over parities proofs of the bit pigeonhole principle and its generalizations, advancing understanding of proof complexity in this domain.

Contribution

It proves new exponential lower bounds for Res(⊕) proofs of BPHP and its variants at certain depths, and introduces a lifting theorem connecting decision tree hardness to proof complexity.

Findings

Res(⊕) proofs of BPHP require exponential size at certain depths.

Generalized BPHP variants also require exponential size in Res(⊕).

A new lifting theorem relates decision tree hardness to proof complexity.

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 $\epsilon>0$, we prove that any depth $N^{1.5 - \epsilon}$ 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-\epsilon}$ 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-\epsilon}$ 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 $\Omega(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 $(\Omega(n), \Omega(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-\epsilon}$ Res$(\oplus)$ proof requires size $\exp(\Omega(N^\epsilon))$. Previously no superpolynomial lower bounds were known for Res$(\oplus)$ proofs when the depth is superlinear in the size of the formula.