Théorème de Savitch

In computational complexity theory, Savitch's theorem, proved by Walter Savitch in 1970, gives a relationship between deterministic and non-deterministic space complexity. It states that for any function , In other words, if a nondeterministic Turing machine can solve a problem using space, a deterministic Turing machine can solve the same problem in the square of that space bound. Although it seems that nondeterminism may produce exponential gains in time (as formalized in the unproven exponential time hypothesis), Savitch's theorem shows that it has a markedly more limited effect on space requirements. The proof relies on an algorithm for STCON, the problem of determining whether there is a path between two vertices in a directed graph, which runs in space for vertices. The basic idea of the algorithm is to solve recursively a somewhat more general problem, testing the existence of a path from a vertex to another vertex that uses at most edges, for a parameter given as input. STCON is a special case of this problem where is set large enough to impose no restriction on the paths (for instance, equal to the total number of vertices in the graph, or any larger value). To test for a -edge path from to , a deterministic algorithm can iterate through all vertices , and recursively search for paths of half the length from to and from to . This algorithm can be expressed in pseudocode (in Python syntax) as follows: def stcon(s, t) -> bool: """Test whether a path of any length exists from s to t""" return k_edge_path(s, t, n) # n is the number of vertices def k_edge_path(s, t, k) -> bool: """Test whether a path of length at most k exists from s to t""" if k == 0: return s == t if k == 1: return (s, t) in edges for u in vertices: if k_edge_path(s, u, floor(k / 2)) and k_edge_path(u, t, ceil(k / 2)): return True return False Because each recursive call halves the parameter , the number of levels of recursion is . Each level requires bits of storage for its function arguments and local variables: and the vertices , , and require bits each.