Exponential Lower Bounds on the Size of ResLin Proofs of Nearly Quadratic Depth
Sreejata Kishor Bhattacharya, Arkadev Chattopadhyay
TL;DR
The paper establishes the first super-polynomial lower bounds on the size of Res(⊕) refutations for depth bounds up to nearly quadratic in the number of variables. It achieves this by lifting Tseitin contradictions on constant-degree expanders through an Inner-Product gadget, paired with a new Conditional Fooling Lemma and an Equidistribution Lemma for safe lifted spaces. The authors develop a DT-to-PDT hardness framework and a lifting theorem showing that DT-hardness implies PDT-hardness, which in turn yields depth-based size lower bounds for Res(⊕) via lifted distributions and amortized-closure analysis. Their approach substantially extends the depth frontier from O(N log N) to O(N^{2−ε}) and achieves near-quadratic depth lower bounds within the random-walk-with-restart paradigm. These techniques introduce robust tools for lifting and bottleneck counting in lifted affine spaces and are influential for future work on hardness in algebraic proof systems.
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^{Ω(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 $Ω(N^{1+ε})$ deep, for any constant $ε> 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Ω(N^ε))$, as long as the depth of the $\text{Res}(\oplus)$ proofs are $O(N^{2-ε})$, for every $ε> 0$. Here $N=Θ(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].