The Community for Technology Leaders
48th Annual IEEE Symposium on Foundations of Computer Science (FOCS'07) (2007)
Providence, Rhode Island
Oct. 21, 2007 to Oct. 23, 2007
ISSN: 0272-5428
ISBN: 0-7695-3010-9
pp: 150-160
<p>We propose a proof-theoretic approach for gaining evidence that certain parameterized problems are not fixedparameter tractable. We consider proofs that witness that a given propositional CNF formula cannot be satisfied by a truth assignment that sets at most k variables to true, considering k as the parameter (we call such a formula a parameterized contradiction). One could separate the parameterized complexity classes FPT and W[2] by showing that there is no fpt-bounded parameterized proof system, i.e., that there is no proof system that admits proofs of size f(k)n^{{\rm O}(1)} where f is a computable function and n represents the size of the propositional formula.</p><p> By way of a first step, we introduce the system of parameterized tree-like resolution, and show that this system is not fpt-bounded. Indeed we give a general result on the size of shortest tree-like resolution proofs of parameterized contradictions that uniformly encode first-order principles over a universe of size n. We establish a dichotomy theorem that splits the exponential case of Riis?s Complexity Gap Theorem into two sub-cases, one that admits proofs of size f(k)n^{{\rm O}(1)} and one that does not.</p><p> We also discuss how the set of parameterized contradictions may be embedded into the set of (ordinary) contradictions by the addition of new axioms. When embedded into general (DAG-like) resolution, we demonstrate that the pigeonhole principle has a proof of size 2^k n^2. This contrasts with the case of tree-like resolution where the embedded pigeonhole principle falls into the "non-FPT" category of our dichotomy.</p>

B. Martin, S. Dantchev and S. Szeider, "Parameterized Proof Complexity," 48th Annual IEEE Symposium on Foundations of Computer Science (FOCS'07)(FOCS), Providence, Rhode Island, 2007, pp. 150-160.
92 ms
(Ver 3.3 (11022016))