Deconstructing Planning as Satisfiability

Henry Kautz

The idea of encoding planning as satisfiability was proposed in 1992 as a method for generating interesting SAT problems, but did not appear to be a practical approach to planning. This changed in 1996, when Satplan was shown to be competitive with current planning technology, leading to a mini-explosion of interest in the approach. Within a few years, however, heuristic search planning appeared to be vastly superior to planning as satisfiability, and many researchers wrote off the earlier success of the approach as a fluke. It was therefore rather surprising when Satplan won first place for optimal STRIPS planning in the 2004 ICAPS planning competition, and repeated the feat in 2006. This talk will attempt to deconstruct the reasons for Satplan's successes and failures, and discuss ways the approach might be extended to handle open domains, metric constraints, and domain symmetries.