Resolution Proofs, Exponential Bounds, and Kolmogorov Complexity

10 years 5 months ago
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.
Uwe Schöning
Added 08 Aug 2010
Updated 08 Aug 2010
Type Conference
Year 1997
Where MFCS
Authors Uwe Schöning
Comments (0)