Exponential Lower Bounds on the Size of ResLin Proofs of Nearly Quadratic Depth

TL;DR

This paper establishes exponential lower bounds on the size of ResLin proofs of Tseitin formulas with nearly quadratic depth, advancing understanding of proof complexity in resolution over parities.

Contribution

It proves the first super-polynomial lower bounds for Res(igoplus) proofs with depth slightly above linear, specifically for Tseitin formulas on constant-degree expanders.

Findings

Res(igoplus) proofs of Tseitin formulas require exponential size at certain depths.

Arbitrary distributions lifted with Inner-Product gadgets fool safe affine spaces.

The results extend proof complexity lower bounds to nearly quadratic depth.

Abstract

Itsykson and Sokolov [IS14] identified resolution over parities, denoted by $\text{Res}(\oplus)$, as a natural and simple fragment of $\text{AC}^0[2]$-Frege for which no super-polynomial lower bounds on size of proofs are known. Building on a recent line of work ([EGI24], [BCD24], [AI25]), Efremenko and Itsykson [EI25] proved lower bounds of the form $\text{exp}(N^{\Omega(1)})$, on the size of $\text{Res}(\oplus)$ proofs whose depth is upper bounded by $O(N\log N)$, where $N$ is the number of variables of the unsatisfiable CNF formula. The hard formula they used was Tseitin on an appropriately expanding graph, lifted by a $2$-stifling gadget. They posed the natural problem of proving super-polynomial lower bounds on the size of proofs that are $\Omega(N^{1+\epsilon})$ deep, for any constant $\epsilon > 0$. We prove the first such lower bounds. In fact, we show that $\text{Res}(\oplus)$ refutations of Tseitin formulas on constant-degree expanders on $m$ vertices, lifted with Inner-Product gadget of size $O(\log m)$, must have size $\text{exp}(\tilde{\Omega}(N^{\epsilon}))$, as long as the depth of the $\text{Res}(\oplus)$ proofs are $O(N^{2-\epsilon})$, for every $\epsilon > 0$. Here $N=\Theta(m\log m)$ is the number of variables of the lifted formula. An important ingredient in our work is to show that arbitrary distributions lifted with such gadgets fool safe affine spaces, an idea which originates in the earlier work of Bhattacharya, Chattopadhyay and Dvorak [BCD24].