Hardness of Parameterized Resolution

Circuits, Logic, and Games

计算机科学;物理学;数学

Olaf Beyersdorff ; Nicola Galesi ; Massimo Lauria

Others  :  http://drops.dagstuhl.de/opus/volltexte/2010/2525/pdf/10061.GalesiNicola.Paper.2525.pdf
PID  :  44034

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

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 Prover-Delayer 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 Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNF's. We answer a question posed by Dantchev, Martin, and Szeider in [16] showing that dag-like Parameterized Resolution is not fpt-bounded. We obtain this result by proving that the pigeonhole principle requires proofs of size n^Ω(k) in dag-like Parameterized Resolution. For this lower bound we use a different Prover-Delayer game which was developed for Resolution by Pudlák [27].