Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR25-106 | 30th July 2025 20:06

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

RSS-Feed




TR25-106
Authors: Sreejata Bhattacharya, Arkadev Chattopadhyay
Publication: 30th July 2025 22:22
Downloads: 96
Keywords: 


Abstract:

Itsykson and Sokolov 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, Efremenko and Itsykson 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 provide a significant improvement by proving a lower bound on size of the form $\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$. Our hard formula is again Tseitin on an expander graph, albeit lifted with a different type of gadget. Our gadget needs to have small correlation with all parities.

An important ingredient in our work is to show that arbitrary distributions \emph{lifted} with such gadgets fool \emph{safe} affine spaces, an idea which originates in the earlier work of Bhattacharya, Chattopadhyay and Dvorak.



ISSN 1433-8092 | Imprint