Abstract

Exponential Lower Bounds for AC0 -Frege Imply Superpolynomial Frege Lower Bounds YUVAL FILMUS and TONIANN PITASSI, University of Toronto RAHUL SANTHANAM, University of Edinburgh We give a general transformation that turns polynomial-size Frege proofs into subexponential-size AC0 Frege proofs. This indicates that proving truly exponential lower bounds for AC0 -Frege is hard, as it is a long-standing open problem to prove superpolynomial lower bounds for Frege. Our construction is optimal for proofs of formulas of unbounded depth. As a consequence of our main result, we are able to shed some light on the question of automatizability for bounded-depth Frege systems. First, we present a simpler proof of the results of Bonet et al. showing that under cryptographic assumptions, bounded-depth Frege proofs are not automatizable. Second, we show that because our proof is more general, under the right cryptographic assumptions, it could resolve the automatizability question for lower-depth Frege systems. Categories and Subject Descriptors: F.1.3 [Computation by Abstract Devices]: Complexity Measures and Classes--Relations among complexity classes General Terms: Theory Additional Key Words and Phrases: Proof complexity ACM Reference Format: Yuval Filmus, Toniann Pitassi, and Rahul Santhanam. 2015. Exponential lower bounds for AC0 -Frege imply superpolynomial Frege lower bounds. ACM