Reachability method

The reachability method is a recursive divide-and-conquer technique for determining whether a path exists between two points in an exponentially large state space, without requiring memory proportional to the number of states. Pioneered in the proof of Savitch's theorem, it replaces exhaustive search with a halving strategy: to find a path of length k, one searches for a midpoint that splits the path into two subpaths of length k/2. The method trades exponential time for quadratic space, revealing that memory-constrained computation can simulate branching exploration through recursive decomposition rather than parallel tracking.

The reachability method generalizes beyond graph reachability to any problem where a solution can be verified by recursive bisection — including model checking, game solving, and constraint satisfaction. Its core insight is that space is reusable in ways that time is not: the same memory can be overwritten at each recursive level, making the method a paradigm for space-efficient computation.

The reachability method is not merely an algorithmic trick; it is a proof that exponential branching does not require exponential memory. Any system that can recursively evaluate and discard partial solutions — whether a theorem prover, a strategic reasoner, or a biological search process — already embodies this principle, whether it knows it or not.