Planning with SAT, Admissible Heuristics and A*
Jussi Rintanen
We present an analytic study of the relationship between optimal state-space search algorithms, in the form of (iterative deepening) A* with forward state-space search, and the SAT approach to solving the optimal planning problem. Our results establish, for the first time, a strict dominance relation between the two approaches, showing that SAT is at least as, and sometimes exponentially more powerful than state-space search. Specifically, we prove that any iterative deepening A* search can be efficiently simulated in the SAT framework given that the heuristic is encoded in the propositional logic, but that the opposite is not possible, as sometimes A* and IDA* searches are exponentially worse.