A general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider [9]. There the authors concentrate on tree-like Parameterized Resolution-a parameterized version of classical Resolution-and their gap complexity theorem implies lower bounds for that system. The main result of the present paper significantly improves upon this by showing optimal lower bounds for a parameterized version of bounded-depth Frege. More precisely, we prove that the pigeonhole principle requires proofs of size n Ω(k) in parameterized bounded-depth Frege, and, as a special case, in dag-like Parameterized Resolution. This answers an open question posed in [9]. In the opposite direction, we interpret a well-known technique for FPT algorithms as a DPLL procedure for Parameterized Resolution. Its generalization leads to a proof search algorithm for Parameterized Resolution that in particular shows that tree-like Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNF's. © 2011 Springer-Verlag.
Parameterized bounded-depth Frege is not optimal / Olaf, Beyersdorff; Galesi, Nicola; Lauria, Massimo; Alexander A., Razborov:. - 6755 LNCS:PART 1(2011), pp. 630-641. (Intervento presentato al convegno 38th International Colloquium on Automata, Languages and Programming, ICALP 2011 tenutosi a Zurich nel 4 July 2011 through 8 July 2011) [10.1007/978-3-642-22006-7_53].
Parameterized bounded-depth Frege is not optimal
GALESI, NICOLA;LAURIA, MASSIMO;
2011
Abstract
A general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider [9]. There the authors concentrate on tree-like Parameterized Resolution-a parameterized version of classical Resolution-and their gap complexity theorem implies lower bounds for that system. The main result of the present paper significantly improves upon this by showing optimal lower bounds for a parameterized version of bounded-depth Frege. More precisely, we prove that the pigeonhole principle requires proofs of size n Ω(k) in parameterized bounded-depth Frege, and, as a special case, in dag-like Parameterized Resolution. This answers an open question posed in [9]. In the opposite direction, we interpret a well-known technique for FPT algorithms as a DPLL procedure for Parameterized Resolution. Its generalization leads to a proof search algorithm for Parameterized Resolution that in particular shows that tree-like Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNF's. © 2011 Springer-Verlag.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
