2025/07/30 by Sreejata Kishor Bhattacharya, Bhattacharya, Sreejata Kishor, Arkadev Chattopadhyay +1
Computer Science · Engineering · #Advanced Numerical Analysis Techniques #Computational Complexity (cs.CC) #Computational Geometry and Mesh Generation #FOS: Computer and information sciences #Optimization and Packing Problems
paper · pdf · doi:10.48550/arxiv.2507.23008
openalex publication_date 2025/07/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Itsykson and Sokolov [IS14] identified resolution over parities, denoted by Res(⊕), as a natural and simple fragment of AC0[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 exp(NΩ(1)), on the size of Res(⊕) proofs whose depth is upper bounded by O(Nlog 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 Ω(N1+ε) deep, for any constant ε> 0. We prove the first such lower bounds. In fact, we show that Res(⊕) refutations of Tseitin formulas on constant-degree expanders on m vertices, lifted with Inner-Product gadget of size O(log m), must have size exp(Ω(Nε)), as long as the depth of the Res(⊕) proofs are O(N2-ε), for every ε> 0. Here N=Θ(mlog 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].