We exhibit a monotone function computable by a monotone circuit of quasipolynomial size such that any monotone circuit of polynomial depth requires exponential size. This is the first size–depth tradeoff result for monotone circuits in the so-called supercritical regime. Our proof is based on an analogous result in proof complexity: We introduce a new family of unsatisfiable 3-CNF formulas (called bracket formulas) that admit resolution refutations of quasipolynomial size while any refutation of polynomial depth requires exponential size.

Abstract. We study Frege proofs using depth-[Formula: see text] Boolean formulas for the Tseitin contradiction on [Formula: see text] grids. We prove that if each line in the proof is of size [Formula: see text], then the number of lines is exponential in [Formula: see text]. This strengthens a recent result of Pitassi, Ramakrishman, and Tan [2022 IEEE 62 nd Annual Symposium on Foundations of Computer Science, 2022, pp. 445–456]. The key technical step is a multiswitching lemma extending the switching lemma of Håstad [ J. ACM, 68 (2021), 1] for a space of restrictions related to the Tseitin contradiction. The strengthened lemma also allows us to improve the lower bound for standard proof size of bounded depth Frege refutations from exponential in [Formula: see text] to exponential in [Formula: see text]. This strengthens the bounds given in the preliminary version of this paper [J. Håstad and K. Risse, 2022 IEEE 63 rd Annual Symposium on Foundations of Computer Science, 2022, pp. 1138–1149].

We prove that polynomial calculus (and hence also Nullstellensatz) over any field requires linear degree to refute that sparse random regular graphs, as well as sparse Erdős-Rényi random graphs, are 3-colourable. Using the known relation between size and degree for polynomial calculus proofs, this implies strongly exponential lower bounds on proof size

We prove that unary Sherali-Adams requires proofs of size $n^{\Omega(d)}$ to rule out the existence of an $n^{\Theta(1)}$-clique in Erdős-Rényi random graphs whose maximum clique is of size $d \leq 2 \log n$. This lower bound is tight up to the multiplicative constant in the exponent. We obtain this result by introducing a technique inspired by pseudo-calibration which may be of independent interest. The technique involves defining a measure on monomials that precisely captures the contribution of a monomial to a refutation. This measure intuitively captures progress and should have further applications in proof complexity.

We study Frege proofs using depth-d Boolean formulas for the Tseitin contradiction on $n\times n$ grids. We prove that if each line in the proof is of size M then the number of lines is exponential in $n/(\log M)^{O(d)}$. This strengthens a recent result of Pitassi et al. [12]. The key technical step is a multi-switching lemma extending the switching lemma of Hastad [8] for a space of restrictions related to the Tseitin contradiction. The strengthened lemma also allows us to improve the lower bound for standard proof size of bounded depth Frege refutations from exponential in $\tilde{\Omega}(n^{1/59d})$ to exponential in $\tilde{\Omega}(n^{1/(2d-1)})$.