Hardness of Parameterized Resolution

9 years 10 months ago
Hardness of Parameterized Resolution
Parameterized Resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider [16] (FOCS’07). In that paper, Dantchev et al. show a complexity gap in tree-like Parameterized Resolution for propositional formulas arising from translations of first-order principles. We broadly investigate Parameterized Resolution obtaining the following main results: ∙ We introduce a purely combinatorial approach to obtain lower bounds to the proof size in tree-like Parameterized Resolution. For this we devise a new asymmetric ProverDelayer game which characterizes proofs in (parameterized) tree-like Resolution. By exhibiting good Delayer strategies we then show lower bounds for the pigeonhole principle as well as the order principle. ∙ Interpreting a well-known FPT algorithm for vertex cover as a DPLL procedure for Parameterized Resolution, we devise a proof search algorithm for Parameterized Resolution and show that tree-like Para...
Olaf Beyersdorff, Nicola Galesi, Massimo Lauria
Added 25 Jan 2011
Updated 25 Jan 2011
Type Journal
Year 2010
Where ECCC
Authors Olaf Beyersdorff, Nicola Galesi, Massimo Lauria
Comments (0)