Klim Efremenko

Strong lower bounds of the form 2(1-ϵ)n, where n is the number of variables and ϵ>0 is arbitrarily small (i.e., bounds consistent with the Strong ETH), are exceptionally rare in proof complexity. The seminal work of Beck and Impagliazzo (STOC 2013) achieved such a bound for regular resolution, and the strongest extension known prior to our work was proved for O(ϵ)-regular resolution by Bonacina and Talebanfard (Algorithmica, 2017). We establish similar lower bounds for a significantly stronger proof system - a fragment of resolution over parities (Res(⊕)). This fragment captures Depth-n Res(⊕), and thus our result implies SETH-type lower bounds for both tree-like and regular Res(⊕). The core of our approach is a lossless lifting achieved by assigning distinct, randomly chosen gadgets to each variable. Our result also yields a SETH-type lower bound for Depth-n resolution - a result that was previously unknown. We additionally provide a direct and simplified proof for this special case, which may be of independent interest.