Poly-logarithmic Frege depth lower bounds via an expander switching lemma


Conference Paper

© 2016 ACM. We show that any polynomial-size Frege refutation of a certain linear-size unsatisfiable 3-CNF formula over n variables must have depth Ω(√logn). This is an exponential improvement over the previous best results (Pitassi et al. 1993, Krajíček et al. 1995, Ben-Sasson 2002) which give Ω(log log n) lower bounds. The 3-CNF formulas which we use to establish this result are Tseitin contradictions on 3-regular expander graphs. In more detail, our main result is a proof that for every d, any depth-d Frege refutation of the Tseitin contradiction over these n-node graphs must have size nΩ(logn n)/d2). A key ingredient of our approach is a new switching lemma for a carefully designed random restriction process over these expanders. These random restrictions reduce a Tseitin instance on a 3-regular n-node expander to a Tseitin instance on a random subgraph which is a topological embedding of a 3-regular n'-node expander, for some n' which is not too much less than n. Our result involves Ω(√logn) iterative applications of this type of random restriction.

Full Text

Duke Authors

Cited Authors

  • Pitassi, T; Rossman, B; Tan, LY; Servedio, RA

Published Date

  • June 19, 2016

Published In

Volume / Issue

  • 19-21-June-2016 /

Start / End Page

  • 644 - 657

International Standard Serial Number (ISSN)

  • 0737-8017

International Standard Book Number 13 (ISBN-13)

  • 9781450341325

Digital Object Identifier (DOI)

  • 10.1145/2897518.2897637

Citation Source

  • Scopus