Parameterized Proof Complexity: a Complexity Gap for Parameterized Tree-like Resolution

We propose a proof-theoretic approach for gaining evidence that certain parameterized problems are not fixed-parameter 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. 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. We provide a first step and show that tree-like resolution 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’ Complexity Gap Theorem for tree-like resolution. Riis’ result establishes a dichotomy between polynomial and exponential size tree-like resolution proofs for propositional formulas that uniformly encode a first-order prin...

• Type: Journal
• Year: 2007
• Where: ECCC
• Authors: Stefan S. Dantchev, Barnaby Martin, Stefan Szeider
• Keywords: ECCC 2007, Propositional Formulas, Tree-like Resolution, Tree-like Resolution Proof