Parameterized Proof Complexity

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 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 proof system (for CNF formulas) that admits proofs of size f(k)nO(1) where f is a computable function and n represents the size of the propositional formula. By way of a first step, we introduce the system of parameterized tree-like resolution, and show that this system does not admit such proofs. We obtain this result as a corollary to a meta-theorem, the main result of this paper. The meta-theorem extends Riis’s Complexity Gap Theorem for tree-like resolution. Riis’s result establishes a dichotomy between polynomial and exp...

• Type: Conference
• Year: 2007
• Where: FOCS
• Authors: Stefan S. Dantchev, Barnaby Martin, Stefan Szeider
• Keywords: FOCS 2007, Parameterized Tree-like Resolution, Theoretical Computer Science, Tree-like Resolution, Tree-like Resolution Proof