License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-25254
URL: http://drops.dagstuhl.de/opus/volltexte/2010/2525/

Beyersdorff, Olaf ; Galesi, Nicola ; Lauria, Massimo

Hardness of Parameterized Resolution

pdf-format:
Dokument 1.pdf (469 KB)


Abstract

Parameterized Resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (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: 1) 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. 2) 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. 3) We answer a question posed by Dantchev, Martin, and Szeider 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^{Omega(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.

BibTeX - Entry

@InProceedings{beyersdorff_et_al:DSP:2010:2525,
  author =	{Olaf Beyersdorff and Nicola Galesi and Massimo Lauria},
  title =	{Hardness of Parameterized Resolution},
  booktitle =	{Circuits, Logic, and Games},
  year =	{2010},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th{\'e}rien and Heribert Vollmer},
  number =	{10061},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2525},
  annote =	{Keywords: Proof complexity, parameterized complexity, Resolution, Prover-Delayer Games}
}

Keywords: Proof complexity, parameterized complexity, Resolution, Prover-Delayer Games
Seminar: 10061 - Circuits, Logic, and Games
Issue date: 2010
Date of publication: 26.04.2010


DROPS-Home | Fulltext Search | Imprint Published by LZI