Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



Revision #2 to TR07-001 | 25th April 2007 00:00

Black-White Pebbling is PSPACE-Complete


Revision #2
Authors: Philipp Hertel, Philipp Hertel
Accepted on: 25th April 2007 00:00
Downloads: 3068


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 to TR07-001 | 7th January 2007 00:00

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

Revision #1
Authors: Stefan S. Dantchev, Barnaby Martin, Stefan Szeider
Accepted on: 7th January 2007 00:00
Downloads: 2830



TR07-001 | 19th November 2006 00:00

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

ISSN 1433-8092 | Imprint