Resolution Proofs, Exponential Bounds, and Kolmogorov Complexity

We prove an exponential lower bound for the length of any resolution proof for the same set of clauses as the one used by Urquhart [13]. Our contribution is a significant simplification in the proof and strengthening of the bound, as compared to [13]. We use on the one hand a simplification similar to the one suggested by Beame and Pitassi in [1] for the case of the pidgeon hole clauses. Additionally, we base our construction on a simpler version of expander graphs than the ones used in [13]. These expander graphs are located in the core of the construction. We show the existence of our expanders by a Kolmogorov complexity argument which has not been used before in this context and might be of independent interest since the applicability of this method is quite general.

• Type: Conference
• Year: 1997
• Where: MFCS
• Authors: Uwe Schöning
• Keywords: Expander Graphs, Exponential Lower Bound, MFCS 1997, Pidgeon Hole Clauses, Theoretical Computer Science