# 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

Generalized 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 (unbounded)
* 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 (resp. clique). The last to play wins.
* Nondeterministic Constraint Logic (unbounded)

## Others

* Finite horizon POMDPs (Partially Observable Markov Decision Processes).
* Hidden Model MDPs (hmMDPs).
* 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 $T_{0}$ and a width $n$ given in unary notation, is there any height $m$ such that an $n\times m$ rectangle can be tiled such that all the border tiles are $T_{0}$?