Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > KEYWORD > RESOLUTION OVER PARITIES:
Reports tagged with Resolution over parities:
TR24-132 | 6th September 2024
Arkadev Chattopadhyay, Pavel Dvorak

Super-critical Trade-offs in Resolution over Parities Via Lifting

Revisions: 1

Razborov [J. ACM, 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-\epsilon}/k$ needs size $\text{exp}\big(n^{\Omega(k)}\big)$. We extend this result to tree-like ... more >>>


TR25-039 | 31st March 2025
Klim Efremenko, Dmitry Itsykson

Amortized Closure and Its Applications in Lifting for Resolution over Parities

The notion of closure of a set of linear forms, first introduced by Efremenko, Garlik, and Itsykson [EGI-STOC-24], has proven instrumental in proving lower bounds on the sizes of regular and bounded-depth Res($\oplus)$ refutations [EGI-STOC-24, AI-STOC-25]. In this work, we present amortized closure, an enhancement that retains the properties of ... more >>>


TR25-106 | 30th July 2025
Sreejata Bhattacharya, Arkadev Chattopadhyay

Exponential Lower Bounds on the Size of ResLin Proofs of Nearly Quadratic Depth

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


TR25-116 | 28th July 2025
Dmitry Itsykson, Alexander Knop

Supercritical Tradeoff Between Size and Depth for Resolution over Parities

Alekseev and Itsykson (STOC 2025) proved the existence of an unsatisfiable CNF formula such that any resolution over parities (Res($\oplus$)) 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 ... more >>>




ISSN 1433-8092 | Imprint