A Study of the Power of Heuristic-based Pruning via SAT Planning

Planning as SAT (satisfiability) is the method of representing a horizon-bounded planning problem as a Boolean SAT problem, and using a SAT decision procedure to solve that problem. Representations are direct, thus a solution plan can be obtained directly from a satisfying valuation. By querying a SAT solver over a series of horizon lengths, up to a completeness threshold, this approach can be the basis of a complete planning procedure. SAT planning algorithms have been theoretically contrasted with IDA∗ search, a heuristic state-based search algorithm, where a theoretical exponential separation is demonstrated in favour of the SAT approach. Here a nominated heuristic is implemented in SAT with the query formulae encoding heuristic information. We make two practical contributions related to this background. First, we provide to the best of our knowledge the first practical implementation of a theoretical SAT encoding of the h² heuristic. Second, we empirically evaluate SAT based pruning by implementing heuristics h_max and h².