In computational complexity theory, Savitch's theorem, proved by Walter Savitch in 1970, states that

NSPACE(f(n)) ⊆ DSPACE(f²(n)).

In other words, if a nondeterministic Turing machine can solve a problem using f(n) space, an ordinary deterministic Turing machine can solve the same problem in the square of the space. Although we believe that nondeterminism can speed up time exponentially, this theorem shows that it has a markedly more limited effect on space requirements.

The proof of the theorem is constructive: it demonstrates an algorithm for USTCON, the problem of determining whether there is a path between two vertices in an undirected graph, which runs in log²(n) time for n vertices. Then, it builds a DSPACE machine which runs the algorithm on the computation tree of the corresponding NSPACE machine to determine whether there is a path from the start node to the accept node, and accepts if and only if this is so.

Some important corollaries of the theorem include:

• PSPACE = NPSPACE
• NL = L²
• SL ⊆ L² = NL