2026-07-21T12:18:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23718 2025-10-27T10:42:47Z ddc:004 open_access

Super-Critical Trade-Offs in Resolution over Parities via Lifting Chattopadhyay, Arkadev Dvořák, Pavel Proof complexity Lifting Resolution over parities Razborov [Alexander A. Razborov, 2016] exhibited the following surprisingly strong trade-off phenomenon in propositional proof complexity: for a parameter k = k(n), there exists k-CNF formulas over n variables, having resolution refutations of O(k) width, but every tree-like refutation of width n^{1-ε}/k needs size exp(n^Ω(k)). We extend this result to tree-like Resolution over parities, commonly denoted by Res(⊕), with parameters essentially unchanged. To obtain our result, we extend the lifting theorem of Chattopadhyay, Mande, Sanyal and Sherif [Arkadev Chattopadhyay et al., 2023] to handle tree-like affine DAGs. We introduce additional ideas from linear algebra to handle forget nodes along long paths. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Arkadev Chattopadhyay and Pavel Dvořák 2025 Is Part Of LIPIcs, Volume 339, 40th Computational Complexity Conference (CCC 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CCC.2025.24 urn:nbn:de:0030-drops-237186 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.24 eng https://creativecommons.org/licenses/by/4.0/legalcode