Generalized Geography is PSPACE-complete

Generalized Geography (Cslib.Complexity.GeneralizedGeography: a directed graph with a start vertex, on which two players alternately move a token along arcs to unvisited vertices, the first player unable to move losing, and the instance is in the set when the first player has a winning strategy) is PSPACE-complete Sipser, Theorem 8.14 Lichtenstein and Sipser. This is the vertex version of the game; Schaefer's original Generalized Geography, in which arcs may not be reused, is not treated [Sch78]. The proof has two halves:

• it is in PSPACE (Cslib.Complexity.GeneralizedGeography_mem_PSPACE): it is a game of polynomially many moves with a polynomial-time winning condition, decided in polynomial space by the characterization of PSPACE through such games;
• it is PSPACE-hard (Cslib.Complexity.GeneralizedGeography_pspaceHard): true quantified Boolean formulas in alternating prenex conjunctive normal form (Cslib.Complexity.TQBFCNF), which are PSPACE-hard, reduce to it by the diamond construction of Sipser's proof, which adapts Schaefer's reduction from quantified formulas to geography games.

Both are relative to the encoding encPair encGraph encNat of a graph, as lists of binary vertices and arcs, with a binary start vertex.

Main results

• Cslib.Complexity.GeneralizedGeography_pspaceComplete: Generalized Geography is PSPACE-complete.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 8.14
• D. Lichtenstein, M. Sipser, GO is polynomial-space hard
• T. J. Schaefer, On the complexity of some two-person perfect-information games

theorem Cslib.Complexity.GeneralizedGeography_pspaceComplete : PSPACEComplete (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) GeneralizedGeography

Generalized Geography is PSPACE-complete Sipser, Theorem 8.14 [LS80].