Name
Abstract | ||
|---|---|---|
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 Ω(loglogn) 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)/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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2897518.2897637 | STOC |
Keywords | Field | DocType |
propositional proof complexity,Frege proof system,small-depth circuits,switching lemma,random projections | Discrete mathematics,Graph,Combinatorics,Embedding,Expander graph,Exponential function,Logarithm,Lemma (mathematics),Mathematics | Conference |
ISSN | Citations | PageRank |
0737-8017 | 3 | 0.40 |
References | Authors | |
15 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Toniann Pitassi | 1 | 2282 | 155.18 |
| Benjamin Rossman | 2 | 298 | 20.00 |
| Rocco A. Servedio | 3 | 1656 | 133.28 |
| Li-Yang Tan | 4 | 159 | 24.26 |