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.

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.