All reports by Author Pavel Dvorak:

__
TR24-132
| 6th September 2024
__

Arkadev Chattopadhyay, Pavel Dvorak#### Super-critical Trade-offs in Resolution over Parities Via Lifting

__
TR24-022
| 6th February 2024
__

Sreejata Bhattacharya, Arkadev Chattopadhyay, Pavel Dvorak#### Exponential Separation Between Powers of Regular and General Resolution Over Parities

Revisions: 1

Arkadev Chattopadhyay, Pavel Dvorak

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

Sreejata Bhattacharya, Arkadev Chattopadhyay, Pavel Dvorak

Proving super-polynomial lower bounds on the size of proofs of unsatisfiability of Boolean formulas using resolution over parities, is an outstanding problem that has received a lot of attention after its introduction by Raz and Tzamaret (2008). Very recently, Efremenko, Garlik and Itsykson (2023) proved the first exponential lower bounds ... more >>>