Tradeoffs for small-depth Frege proofs
share
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 where each line is a size-s formula, we prove that exp(n/2^Ω(d√(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^Ω(1/d)) lower bound on the overall proof size. For s = poly(n), for example, our lower bound remains exp(n^1-o(1)) for all d = o(√(log n)), whereas Håstad's lower bound is exp(n^o(1)) once d = ω_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.
READ FULL TEXT