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

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