# Planning as Satisfiability

Planning as satisfiability is a powerful approach to domain-independent planning (in artificial intelligence) first proposed by Henry Kautz and Bart Selman in their SATPLAN system in the 1990s.

The latest planners based on SAT rival (and exceed) the performance of planners based on other search paradigms. Additionally, this level of performance is obtained almost completely by general purpose SAT solving algorithms, without the need for the kind of specialized techniques used in connection with the recent state-space search planners (such as algorithm/heuristic portfolios, incomplete search algorithms, recognition of "multi-valued" structure from standard Boolean representations, macros and other non-systematic ways of introducing short-cuts in the state space graph, techniques targeting specific benchmark domains e.g. goal-agendas, and so on and on).

## Problem encodings

The main development in planning as SAT in the last years has been the introduction of asymptotically optimal, linear-size encodings for the main classes of plans, including the GraphPlan notion of parallel plans. All earlier encodings had a quadratic size (for the action exclusion axioms in particular), which led to formulas of sizes of hundreds or thousands of megabytes, making e.g. the use of efficient parallel search strategies impossible.

Almost all of earlier research has used parallel plans based on the notion of interference: two actions are allowed to take place in parallel when they do not interfere. A sometimes dramatically more efficient planning is obtained with a more relaxed notion of plans, called ∃-step semantics, uses a more relaxed asymmetric notion of interference, which allows parallelization of actions in many cases where the no-interference condition is not satisfied. A further elaboration of the ∃-step semantics (for the more restricted class of STRIPS problems) is reported in a paper by Wehrle and Rintanen, Planning as satisfiability with relaxed ∃-step plans, where the conditions on parallel actions are further relaxed, in some cases leading to further performance improvements. These two ∃-step encodings are the fastest encodings in existence.

Different Plan Types and Encodings, with Increasing Compactness and Efficiency
plan type description references for encodings
sequential exactly one (or at most one) action per time point Kautz & Selman 1992; Kautz & Selman 1996 (factored encodings); Ernst et al. 1997 (factored encodings)
∀-step plans ("GraphPlan parallelism") A set of actions can be simultaneous if they are pairwise independent (more relaxed definition: can be executed in any order). Kautz & Selman 1996 papers (original work); Rintanen et al. 2006 (compact and linear-size encodings); Robinson et al. 2009 (factored encodings)
∃-step plans A set of actions can be simultaneous if they can be totally ordered so that an earlier action does not disable a later action or change its (conditional) effects (more relaxed definition: can be executed in at least one order). Dimopoulos et al. 1997 (original idea); Rintanen et al. 2004/2006 (analysis, encodings (linear-size)); Ogata et al. 2004; Wehrle & Rintanen 2007

The smallest and generally most efficient encodings have an asymptotically optimal linear size, (which strongly contrasts with the quadratic size all the early encodings from the 1990s, and some of the recent implementations, have). Further improvements, also for asymptotically optimal encodings, can be obtained by finding regularities which can be represented more compactly, most notably in the form of cliques and bicliques in constraint graphs formed by binary clauses (Rintanen 2006).

Many implementations, including BLACKBOX and its successors, use ∀-step plans, corresponding to GraphPlan's notion of parallel plans. These planners map (most of) the contents of the planning graphs to a SAT problem. The extremely large size of the planning graphs, and especially their high number of action mutexes, is the main reason for the extremely large size of the encodings these planners use. These encodings can be substantially improved by eliminating unnecessary action mutexes (Rintanen et al. 2006; Sideris & Dimopoulos, 2010).

It is sometimes believed that ∀-step plans represent "real" parallelism, and this is used as a justification when focusing on "optimal" (minimal horizon length) ∀-step plans. This idea, however, is wrong. Minimal horizon length ∀-step plans don't in general have anything to do with any practically interesting optimality criterion (e.g. minimum cost, minimum makespan). In particular, the definition of ∀-step plans does not guarantee that two actions that take place in the same step can actually be taken in parallel, or that two actions that interfere could not in reality be taken in parallel. Further, in those cases in which the problem modeling has guaranteed that the parallelism reflects reality (which could just as well be achieved with any other definition of parallel plans), usually the action durations vary so much that the minimal number of steps does not have much to do with minimal makespan: all the actions would have to have exactly the same duration for this to work (a condition rarely fulfilled.) For these reasons optimality interpreted as minimum horizon length is a rather uninteresting property of ∀-step plans.

## Parallel plan search

A planner that solves several SAT instances simultaneously (even by using only one CPU or core) can find plans much more efficiently than traditional SAT-based planners. It is this idea, together with the best encodings, that lead to planners with a very good performance.

Top-Level Algorithms for Planning with SAT
algorithm description references
sequential Solve SAT problems sequentially one at a time for horizon lengths 1, 2, 3, 4, ... until a plan is found. Kautz & Selman 1992
algorithm A Start n SAT solvers simultaneously, solving the planning problem for horizon lengths 1,2,3,4,...,n. If a formula is found satisfiable, we have a plan, and terminate. If a formula is found unsatisfiable, start a solver for the shortest plan length not solved yet (first n+1, then n+2, n+3, and so on) so that there are always n SAT instances being solved. Rintanen 2004; Rintanen et al. 2006
algorithm B Solve horizon lengths 1,2,3,... in parallel, assigning to the SAT solver with horizon length t CPU time g times that of horizon length t-1, for some constant g<1. That is, the rate at which SAT problems are solved form a decreasing geometric sequence. Some finite bound is used for the number of SAT solvers run at any given moment (as determined by available memory.) Rintanen 2004; Rintanen et al. 2006
algorithm C Solve horizon lengths 1,2,4,8,16,... in parallel, up to some finite length (some hundreds or thousands), with the same amount of CPU assigned to each horizon length. This strategy works surprisingly well, and does not rely on the implicit assumption that the horizon lengths are short. Rintanen 2012 (unpublished)

Other algorithms have been used, but they either don't lead to substantial runtime improvements (e.g. at most a small multiplicative factor like 2) and/or rely on the availability of plan length upper bounds which are not (efficiently) available. Algorithms A and B trade the possibility of a constant factor slow-down to a potentially arbitrarily high speed-up. Algorithm C does not have any practical performance guarantees w.r.t. A or B or the sequential strategy, but for problems with very long plans it is sometimes much better than A and B.

A requirement for the use of the efficient parallel search strategies is the compactness of the SAT encodings, a condition not fulfilled e.g. by BLACKBOX and its successors.

## Heuristics

Practically all work on planning with SAT has used general-purpose SAT solvers. Some works on planning with CSP has used heuristics specific to planning, but the resulting planners have not been very competitive. Recent work has shown that the conflict-directed clause learning algorithm (CDCL), which most the current best SAT solvers use, together with an extremely simple planning-specific scheme for selecting decision variables (forcing CDCL to do a form of backward chaining, and leveraging the inferences made by CDCL) lead to very competitive planning, typically matching other search paradigms (Rintanen 2010a, 2010b). Simple heuristics on top of the basic variable selection scheme improve the efficiency further.

With the new heuristics, plans for many instances of standard benchmarks are found without backtracking (Airport, DriverLog, Gripper (all), Logistics (almost all), MPrime, Mystery, ParcPrinter, PSR, Rover, Satellite, Scanalyzer, Storage, Woodworking, ZenoTravel). Some of the instances with no or little backtracking (< 10 leaf nodes in the search tree) are not solved by the competition (= heuristic state-space search planners) in a reasonable amount of time (they cannot find plans in 5 minutes, and in some cases we have verified that no plans are found in 8 hours.)

## Software

I have an efficient implementation of Planning as SAT.
• newest amd64 executables: M, Mp (September 10, 2012) © Jussi Rintanen (permission to use granted for academic research purposes only)
• M.32bit executable, Ubuntu Linux 10.04 for Intel x86 (May 10, 2012) © Jussi Rintanen (permission to use granted for academic research purposes only)
03/06/10 changes: More efficient SAT solving. Plan output in the IPC format with -Q. Fixed incorrect output of ∀-step plans.
30/09/10 changes: Fixed handling of problem instances that reduce to nothing.
16/11/10 changes: Small bug fixes.
24/09/11 changes: A parser bug and a grounding bug fixed.
12/01/12 changes: Small bug fixes.
10/04/12 changes: Lots of fixes in the front-end, memory management etc.
• Mp.32bit executable, Ubuntu Linux 10.04 for Intel x86 (May 10, 2012) © Jussi Rintanen (permission to use granted for academic research purposes only)
30/09/10 changes: Fixed handling of problem instances that reduce to nothing.
16/11/10 changes: Small bug fixes. Supports conditional effects (but no disjunction).
24/09/11 changes: A parser bug and a grounding bug fixed. Supports both conditional effects and disjunction.
12/01/12 changes: Small bug fixes.
10/04/12 changes: Lots of fixes in the front-end, memory management etc.
• Source code is available.
Start the program without arguments to get help.

## Comparison between different types of planners

For an illustration of the relative performance of different types of planners, see the following diagram, which shows the number of problem instances from the International Planning Competitions 1998-2011 different planners solve as the timeout limit is increased (1646 instances total, and if a domain appeared twice, the later or more difficult version used).

(See also more diagrams, and data for each IPC domain.) The curve for FF's 2nd phase (FF-2) is a good approximation for Bonet & Geffner's original HSP planner's hypothetical extension to handle non-STRIPS problems with conditional effects.

The planning competition benchmarks are in general quite favorable to planners that use explicit state space search (which were mostly developed by the planning competition community in tandem with the benchmark set), in comparison to other types of planning problems. Porco et al. (ICAPS'11) have translated graph problems to planning, and the picture from those results is quite a bit different. Here, general-purpose SAT solvers fare best (see more detailed discussion in the Porco et al. ICAPS'11 paper), followed by SAT with planning-specific heuristics.

Number of Porco et al. ICAPS'11 benchmarks solved in 300 seconds
domaininstances Mp M LAMA FF HSP YAHSP
clique6006119337422361
coloring280646614518
Hamiltonian200827165523854
k-colorability4801221111145454113
matching1606980350033
SAT2004178391200
total1920439599291153140279

## Publications

J. Rintanen. Planning as satisfiability: heuristics, Artificial Intelligence Journal, 2012.

J. Rintanen. Engineering Efficient Planners with SAT, In ECAI 2012. Proceedings of the 20th European Conference on Artificial Intelligence, IOS Press, 2012.

J. Rintanen. Planning with specialized SAT solvers. In Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, pages 1563-1566, 2011. (© 2011 American Association for Artificial Intelligence. AAAI) (slides)

J. Rintanen. Planning with SAT, admissible heuristics and A*. In Proceedings of the International Joint Conference on Artificial Intelligence, AAAI Press, pages 2015-2020, 2011. (© 2011 American Association for Artificial Intelligence. AAAI)

J. Rintanen. Heuristics for planning with SAT and expressive action definitions. In Proceedings of the International Conference on Automated Planning and Scheduling, AAAI Press, pages 210-217, 2011. (© 2011 American Association for Artificial Intelligence. AAAI)

Jussi Rintanen. Heuristic planning with SAT: beyond strict depth-first search. Twenty-Third Australasian Joint Conference on Artificial Intelligence, Adelaide, December 7-10, 2010, Proceedings. Lecture Notes in Computer Science, Springer-Verlag, 2010.

Jussi Rintanen. Heuristics for planning with SAT. In David Cohen, ed., Principles and Practice of Constraint Programming - CP 2010, 16th International Conference, CP 2010, St. Andrews, Scotland, September 2010, Proceedings. Lecture Notes in Computer Science 6308, pages 414-428, Springer-Verlag, 2010.

Jussi Rintanen. Planning graphs and propositional clause-learning. In Gerhard Brewka and Patrick Doherty, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Eleventh International Conference (KR 2008), pages 535-543, AAAI Press, 2008.

M. Wehrle and J. Rintanen, Planning as satisfiability with relaxed ∃-step plans, In M. Orgun and J. Thornton, eds, AI 2007 : Advances in Artificial Intelligence: 20th Australian Joint Conference on Artificial Intelligence, Surfers Paradise, Gold Coast, Australia, December 2-6, 2007, Proceedings, Lecture Notes in Computer Science 4830, pages 244-253, Springer-Verlag, 2007. The winner of the AI 2007 Best Paper Award

J. Rintanen, K. Heljanko and I. Niemelä, Planning as satisfiability: parallel plans and algorithms for plan search, Artificial Intelligence, 170(12-13), pages 1031-1080, 2006.

J. Rintanen, Evaluation strategies for planning as satisfiability, in R. Lopez de Mantaras and Lorenza Saitta, eds., ECAI 2004. Proceedings of the 16th European Conference on Artificial Intelligence, pages 682-687, IOS Press, 2004. [additional material on slides of ECAI'04 talk, 4 on 1]

J. Rintanen, Phase transitions in classical planning: an experimental study, in Principles of Knowledge Representation and Reasoning: Proceedings of the Ninth International Conference (KR 2004), pages 710-719, AAAI Press, 2004. [additional material on slides of KR'04 talk, 8 on 1]

J. Rintanen, Compact representation of sets of binary constraints, ECAI 2006. Proceedings of the 17th European Conference on Artificial Intelligence, pages 143-147, IOS Press, 2006. [ECAI'06 talk] Biclique-based representations of binary constraints for improving the scalability of SAT representations for very large planning problems.

J. Rintanen, Symmetry reduction for SAT representations of transition systems, in Proceedings of the 13th International Conference on Automated Planning and Scheduling, pages 32-40, AAAI Press, 2003. (© 2003 American Association for Artificial Intelligence. All rights reserved. AAAI)

J. Rintanen and H. Jungholt. Numeric state variables in constraint-based planning, in Recent Advances in AI Planning: 5th European Conference on Planning, ECP'99, Durham, UK, September 8-10, 1999, S. Biundo and M. Fox, eds., Lecture Notes in Artificial Intelligence 1809, pages 109-121, 2000. Springer-Verlag, Berlin, Germany.

J. Rintanen. A planning algorithm not based on directional search. in Principles of Knowledge Representation and Reasoning: Proceedings of the Sixth International Conference (KR '98), A. G. Cohn, L. K. Schubert, and S. C. Shapiro, eds., pages 617-624, Trento, Italy, June 1998. Morgan Kaufmann Publishers, San Francisco, California.

M. Büttner and J. Rintanen, Satisfiability planning with constraints on the number of actions, in Proceedings of the 15th International Conference on Automated Planning and Scheduling, pages 292-299, AAAI Press, 2005.

Overviews:

J. Rintanen, Planning and SAT, in A. Biere, M. Heule, H. van Maaren and T. Walsh, Handbook of Satisfiability, IOS Press, 2009.

J. Rintanen. State-space traversal techniques for planning, Albert-Ludwigs-Universität-Freiburg, Institut für Informatik, Technical Report 220, 76 pages, 2005. (AAAI-06 Tutorial, IJCAI-05 Tutorial)

J. Rintanen. Introduction to automated planning, course notes, Albert-Ludwigs-Universität Freiburg, 2003-2005.

## Bibliography

A. Sideris, Y. Dimopoulos, Constraint propagation in propositional planning, Proceedings of the 20th International Conference on Automated Planning and Scheduling ICAPS'10, AAAI Press, 2010.

Y. Dimopoulos, B. Nebel and J. Koehler, Encoding planning problems in nonmonotonic logic programs, European Conference on Planning, Springer-Verlag, 1997.

H. Kautz and B. Selman, Planning as satisfiability, Proceedings of the Tenth European Conference on Artificial Intelligence (ECAI'92), John Wiley, 1992.

H. Kautz and B. Selman, Pushing the envelope: planning, propositional logic, and stochastic search, Proceedings of the Thirteenth National Conference on Artificial Intelligence and the Eighth Innovative Applications of Artificial Intelligence Conference, AAAI Press, 1996.

N. Robinson, C. Gretton, D.-N. Pham and A. Sattar, SAT-based parallel planning using a split representation of actions, International Conference on Automated Planning and Scheduling, AAAI Press, 2009.