Tradeoffs for small-depth Frege proofs

Abstract

We study the complexity of small-depth Frege proofs and give the first tradeoffs between the size of each line and the number of lines. Existing lower bounds apply to the overall proof size -- the sum of sizes of all lines -- and do not distinguish between these notions of complexity. For depth-$d$ Frege proofs of the Tseitin principle on the $n\times n$ grid where each line is a size-$s$ formula, we prove that $\exp (n/2^{\Omega (d\sqrt{\log s})})$ many lines are necessary. This yields new lower bounds on line complexity that are not implied by Håstad's recent $\exp (n^{\Omega (1/d)})$ lower bound on the overall proof size. For $s=\mathrm{poly}(n)$, for example, our lower bound remains $\exp (n^{1-o(1)})$ for all $d=o(\sqrt{\log n})$, whereas Håstad's lower bound is $\exp (n^{o(1)})$ once $d={\omega }_n(1)$. Our main conceptual contribution is the simple observation that techniques for establishing correlation bounds in circuit complexity can be leveraged to establish such tradeoffs in proof complexity.

FOCS 2021. Fixed typo in Theorem 1.1