List of PSPACE-complete problems
Here are some of the more commonly known problems that are PSPACE-complete when expressed as decision problems. This list is in no way comprehensive.
Games and puzzles
versions of:- Amazons
- Atomix
- Checkers if a draw is forced after a polynomial number of non-jump moves
- Dyson Telescope Game
- Cross Purposes
- Geography
- Two-player game version of Instant Insanity
- Ko-free Go
- Ladder capturing in Go
- Gomoku
- Hex
- Konane
- Lemmings
- Node Kayles
- Poset Game
- Reversi
- River Crossing
- Rush Hour
- Finding optimal play in Mahjong solitaire
- Scrabble
- Sokoban
- Super Mario Bros.
- Black Pebble game
- Black-White Pebble game
- Acyclic pebble game
- One-player pebble game
- Token on acyclic directed graph games:
Logic
- Quantified boolean formulas
- First-order logic of equality
- Provability in intuitionistic propositional logic
- Satisfaction in modal logic S4
- First-order theory of the natural numbers under the successor operation
- First-order theory of the natural numbers under the standard order
- First-order theory of the integers under the standard order
- First-order theory of well-ordered sets
- First-order theory of binary strings under lexicographic ordering
- First-order theory of a finite Boolean algebra
- Stochastic satisfiability
- Linear temporal logic satisfiability and model checking
Lambda calculus
- Type inhabitation problem for simply typed lambda calculus
Automata and language theory
Circuit theory
- Integer circuit evaluation
Automata theory
- Word problem for linear bounded automata
- Word problem for quasi-realtime automata
- Emptiness problem for a nondeterministic two-way finite state automaton
- Equivalence problem for nondeterministic finite automata
- Word problem and emptiness problem for non-erasing stack automata
- Emptiness of intersection of an unbounded number of deterministic finite automata
- A generalized version of Langton's Ant
- Minimizing nondeterministic finite automata
Formal languages
- Word problem for context-sensitive language
- Intersection emptiness for an unbounded number of regular languages
- Regular Expression Star-Freeness
- Equivalence problem for regular expressions
- Emptiness problem for regular expressions with intersection.
- Equivalence problem for star-free regular expressions with squaring.
- Covering for linear grammars
- Structural equivalence for linear grammars
- Equivalence problem for Regular grammars
- Emptiness problem for ET0L grammars
- Word problem for ET0L grammars
- Tree transducer language membership problem for top down finite-state tree transducers
Graph theory
- Succinct versions of many graph problems, with graphs represented as Boolean circuits, ordered binary decision diagrams or other related representations:
- * s-t reachability problem for succinct graphs. This is essentially the same as the simplest plan existence problem in automated planning and scheduling.
- * planarity of succinct graphs
- * acyclicity of succinct graphs
- * connectedness of succinct graphs
- * existence of Eulerian paths in a succinct graph
- Bounded two-player Constraint Logic
- Canadian traveller problem.
- Determining whether routes selected by the Border Gateway Protocol will eventually converge to a stable state for a given set of path preferences
- Deterministic constraint logic
- Dynamic graph reliability.
- Graph coloring game
- Node Kayles game and clique-forming game: two players alternately select vertices and the induced subgraph must be an independent set. The last to play wins.
- Nondeterministic Constraint Logic
Others
- Finite horizon POMDPs.
- Hidden Model MDPs.
- Dynamic Markov process.
- Detection of inclusion dependencies in a relational database
- Computation of any Nash equilibrium of a 2-player normal-form game, that may be obtained via the Lemke–Howson algorithm.
- The Corridor Tiling Problem: given a set of Wang tiles, a chosen tile and a width given in unary notation, is there any height such that an rectangle can be tiled such that all the border tiles are ?