The paper demonstrates a tradeoff between size and depth in resolution over parities, suggesting a new complexity result.
Alekseev and Itsykson (STOC 2025) proved the existence of an unsatisfiable CNF formula such that any resolution over parities (Res(⊕)) refutation must either have exponential size (in the formula size) or superlinear depth (in the number of variables). In this paper, we extend this result by constructing a formula with the same hardness properties, but which additionally admits a resolution refutation of quasi-polynomial size. This establishes a supercritical tradeoff between size and depth for resolution over parities. The proof builds on the framework of Alekseev and Itsykson and relies on a lifting argument applied to the supercritical tradeoff between width and depth in resolution, proposed by Buss and Thapen (IPL 2026).
No takes yet. Share an insight, caveat, or question.
Itsykson et al. (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: