Revision #2 Authors: Philipp Hertel, Philipp Hertel

Accepted on: 25th April 2007 00:00

Downloads: 2406

Keywords:

The complexity of the Black-White Pebbling Game has remained an open problem for 30 years. It was devised to capture the power of non-deterministic space bounded computation. Since then it has been continuously studied and applied to problems in diverse areas of computer science including VLSI design and more recently propositional proof complexity. In 1983, determining its complexity was rated as "An Open Problem of the Month" in David Johnson's NP-Completeness Column. In this paper we show that the Black-White Pebbling Game is PSPACE-complete.

Revision #1 Authors: Stefan S. Dantchev, Barnaby Martin, Stefan Szeider

Accepted on: 7th January 2007 00:00

Downloads: 2139

Keywords:

TR07-001 Authors: Stefan S. Dantchev, Barnaby Martin, Stefan Szeider

Publication: 4th January 2007 12:07

Downloads: 2243

Keywords:

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 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.