Planning as satisfiability is a principal approach to planning with many eminent advantages. The existing planning as satisfiability techniques usually use encodings compiled from STRIPS. We introduce a novel SAT encoding scheme (SASE) based on the SAS formalism. The new scheme exploits the structural information in SAS, resulting in an encoding that is both more compact and efficient for planning. We prove the correctness of the new encoding by establishing an isomorphism between the solution plans of SASE and that of STRIPS based encodings. We further analyze the transition variables newly introduced in SASE to explain why it accommodates modern SAT solving algorithms and improves performance. We give empirical statistical results to support our analysis. We also develop a number of techniques to further reduce the encoding size of SASE, and conduct experimental studies to show the strength of each individual technique. Finally, we report extensive experimental results to demonstrate significant improvements of SASE over the state-of-the-art STRIPS based encoding schemes in terms of both time and memory efficiency.
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 (Kautz & Selman 1992). 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 (Kautz & Selman 1996). 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 (Edelkamp et al. 2004). 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.
Planning as satisfiability is known as an efficient approach to deal with many types of planning problems. However, this approach has not been competitive with the state-space based methods in temporal planning. This paper describes ITSAT as an efficient SAT-based (satisfiability based) temporal planner capable of temporally expressive planning. The novelty of ITSAT lies in the way it handles temporal constraints of given problems without getting involved in the difficulties of introducing continuous variables into the corresponding satisfiability problems. We also show how, as in SAT-based classical planning, carefully devised preprocessing and encoding schemata can considerably improve the efficiency of SAT-based temporal planning.
I have developed three planners that use this approach: MAX-PLAN G-MAXPLAN and ZANDER. MAXPLAN which assumes complete unobservability, converts a dynamic belief network representation of the planning problem to an instance of a stochastic satisfiability problem called E-MAJSAT. C-MAXPLAN and ZANDER extend this paradigm to contingent planning in stochastic domains with partial observability.
In recent years, there is a growing awareness of the importance of reachability and relevance-based pruning techniques for planning, but little work specifically targets these techniques. In this paper, we compare the ability of two classes of algorithms to propagate and discover reachability and relevance constraints in classical planning problems. The first class of algorithms operates on SAT encoded planning problems obtained using the linear and Graphplan encoding schemes. It applies unit-propagation and more general resolution steps (involving larger clauses) to these plan encodings. The second class operates at the plan level and contains two families of pruning algorithms: Reachable-k and Relevant-k. Reachable-k provides a coherent description of a number of existing forward pruning techniques used in numerous algorithms, while Relevant-k captures different grades of backward pruning. Our results shed light on the ability of different plan-encoding schemes to propagate information forward and backward and on the relative merit of plan-level and SAT-level pruning methods.