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.

More generally, we prove the following lifting theorem that requires a gadget $g$ to have sufficiently small correlation with all parities: we introduce a notion of hardness against ordinary decision trees that we call $(p,q)$-DT hardness. We show that if a formula $\Phi$ is $(p,q)$-DT hard, then every $\text{Res}(\oplus)$ refutation of size $s$ of the lifted formula $\Phi \circ g$ must be $\Omega\big(pq/\log(s)\big)$-deep. Our concrete lower bound is obtained by showing that Tseitin formulas on constant degree-expanders are $\big(\Omega(m),\Omega(m))$-hard.

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].

Updated 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.

(i) Proved a general lifting theorem from DT-hardness to PDT-hardness

(ii) Improved constants (gadget size reduced from 500 log(n) to 4 log(n))

(iii) Added intuition in the proof of DT-hardness

(iv) Added more on "recent works" section reflecting latest updates

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.