ECCC-Report TR07-001https://eccc.weizmann.ac.il/report/2007/001Comments and Revisions published for TR07-001en-usSun, 07 Jan 2007 00:00:00 +0200
Revision 1
| Parameterized Proof Complexity: a Complexity Gap for Parameterized Tree-like Resolution |
Stefan S. Dantchev,
Barnaby Martin,
Stefan Szeider
https://eccc.weizmann.ac.il/report/2007/001#revision1Sun, 07 Jan 2007 00:00:00 +0200https://eccc.weizmann.ac.il/report/2007/001#revision1
Paper TR07-001
| Parameterized Proof Complexity: a Complexity Gap for Parameterized Tree-like Resolution |
Stefan S. Dantchev,
Barnaby Martin,
Stefan Szeider
https://eccc.weizmann.ac.il/report/2007/001We 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 formulae) that admits proofs of size f(k)n^{O(1)} where f is a computable function and n denotes 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 formulae that uniformly encode a first-order principle over a universe
of size n: (1) either there are tree-like resolution proofs of size polynomial in n, or (2) the proofs have size at least 2^{\epsilon n} for some constant \epsilon; the second case prevails exactly when the first-order principle has no finite but some infinite model.
We show that the parameterized setting allows a refined classification, splitting the second case into two subcases: (2a) there are tree-like resolution proofs of size at most \beta^k n^\alpha for some constants \alpha,\beta; or (2b) every tree-like resolution proof has size at least n^{k^\gamma} for some constant \gamma in (0,1]; the latter case prevails exactly if for every infinite model, a certain associated hypergraph has no finite dominating set. We provide examples of first-order principles for all three cases.
Thu, 04 Jan 2007 12:07:50 +0200https://eccc.weizmann.ac.il/report/2007/001