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...

• Type: Journal
• Year: 2010
• Where: ECCC
• Authors: Olaf Beyersdorff, Nicola Galesi, Massimo Lauria
• Keywords: Dag-like Parameterized Resolution, ECCC 2010, Parameterized Resolution, Tree-like Parameterized Resolution