Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds

Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds 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. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png ACM Transactions on Computation Theory (TOCT) Association for Computing Machinery

Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds

Download PDF
16 pages

Loading next page...
 
/lp/association-for-computing-machinery/exponential-lower-bounds-for-ac0-frege-imply-superpolynomial-frege-Ft4tdzgyQD
Publisher
Association for Computing Machinery
Copyright
Copyright © 2015 ACM
ISSN
1942-3454
eISSN
1942-3462
DOI
10.1145/2656209
Publisher site
See Article on Publisher Site

Abstract

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.

Journal

ACM Transactions on Computation Theory (TOCT) – Association for Computing Machinery

Published: May 11, 2015

Keywords: Proof complexity

References

  • Resolution is not automatizable unless W{P} is tractable
    Alekhnovich, Michael; Razborov, Alexander
  • Minimizing disjunctive normal form formulas and AC0 circuits given a truth table
    Allender, Eric; Hellerstein, Lisa; McCabe, Paul; Pitassi, Toniann; Saks, Michael
  • Mean-payoff games and propositional proofs
    Atserias, Albert; Maneva, Elitza
  • A quasi-polynomial algorithm for discrete logarithm in finite fields of small characteristic
    Barbulescu, Razvan; Gaudry, Pierrick; Joux, Antoine; Thom, Emmanuel
  • Exponential lower bounds for the pigeonhole principle
    Beame, Paul W.; Impagliazzo, Russell; Krajíček, Jan; Pitassi, Toniann; Pudlák, Pavel; Woods, Alan
  • Are there hard examples for Frege systems? In Feasible Mathematics II, P
    Bonet, Maria Luisa; Buss, Samuel R.; Pitassi, Toniann
  • Non-automatizability of bounded-depth Frege proofs
    Bonet, Maria Luisa; Domingo, Carlos; Gavaldà, Ricard; Maciel, Alexis; Pitassi, Toniann
  • On interpolation and automatization for Frege systems
    Bonet, Maria Luisa; Pitassi, Toniann; Raz, Ran
  • The parallel evaluation of general arithmetic expressions
    Brent, Richard P.
  • Polynomial size proofs of the pigeonhole principle
    Buss, Samuel R.
  • The relative efficiency of propositional proof systems
    Cook, Stephen A.; Reckhow, Robert A.
  • Simplified lower bounds for propositional proofs
    Fu, Xudong; Urquhart, Alasdair
  • Theories for subexponential-size bounded-depth Frege proofs
    Ghasemloo, Kaveh; Cook, Stephen A.
  • Computational Limitations of Small Depth Circuits
    Håstad, Johan
  • The intractability of resolution
    Haken, Armin
  • A new index calculus algorithm with complexity L(1/4 + o(1)) in very small characteristic
    Joux, Antoine
  • Lower bounds to the size of constant-depth propositional proofs
    Krajíček, Jan
  • Bounded Arithmetic, Propositional Logic, and Complexity Theory
    Krajíček, Jan
  • Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
    Krajíček, Jan
  • Forcing with Random Variables and Proof Complexity
    Krajíček, Jan
  • An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle
    Krajíček, Jan; Pudlák, Pavel; Woods, Alan
  • Universal sequential search problems
    Levin, Leonid A.
  • Polylogarithmic cuts in models of V0
    Müller, Sebastian
  • Rudimentary predicates and Turing calculations
    Nepomnjaščij, V. A.
  • On the power of clause-learning SAT solvers as resolution engines
    Pipatsrisawat, Knot; Darwiche, Adnan
  • Exponential lower bounds for the pigeonhole principle
    Pitassi, Toniann; Beame, Paul; Impagliazzo, Russell
  • On the Lengths of Proofs in the Propositional Calculus
    Reckhow, Robert A.
  • Borel sets and circuit complexity
    Sipser, Michael
  • On time-hardware complexity tradeoffs for Boolean functions
    Spira, P. M.