Planning with SAT, Admissible Heuristics and A*

We study the relationship between optimal planning algorithms, in the form of (iterative deepening) A* with (forward) state-space search, and the reduction of the problem to SAT. Our results establish a strict dominance relation between the two approaches: any iterative deepening A* search can be efficiently simulated in the SAT framework, assuming that the heuristic has been encoded in the SAT problem, but the opposite is not possible as A* and IDA* searches sometimes take exponentially longer.