Poly-logarithmic Frege depth lower bounds via an expander switching lemma.
T. Pitassi and B. Rossman and R. Servedio and L.-Y. Tan.
In 48th Annual Symposium on Foundations of Computer Science (STOC), 2016, to appear.


Abstract: We show that any polynomial-size Frege refutation of a certain linear-size unsatisfiable 3-CNF formula over $n$ variables must have depth \Omega(\sqrt{\log n}). This is an exponential improvement over the previous best results (Pitassi, Beame, Impagliazzo 1993; Krajicek, Pudlak, Woods 1995; Ben-Sasson 2002) which give \Omega(\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^{\Omega((\log n)/d^2)}. 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 \Omega(\sqrt{\log n}) iterative applications of this type of random restriction.


Back to main papers page