October 10, 2016 (first version May 20, 2015)

Temporal Planning by Satisfiability modulo Theories

Planning as satisfiability (see Planning by SAT) 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 work of Kautz and Selman limited to the simplest case of planning, with asynchoronous discrete systems expressible in terms of states consisting of Boolean state variables.

Later extensions to the work include

Both of these extensions include integer and real-valued state variables, which usually cannot be effectively handled in the basic SAT framework. What is needed is what is now known as Satisfiability modulo Theories (SMT), which extends the language of propositional logic with non-Boolean theories such as linear real arithmetics.

Modeling languages

Efficient reductions to SMT

Although reductions of temporal and hybrid systems planning to SMT have been known for a long time (see work of Shin and Davis, 2005), SMT has not been viewed as a competitive approach. Making SMT competitive is based on the following observations. The encodings of temporal planning in SMT (and all other constraint-based formalisms) follows the ideas first presented by Kautz and Selman (see Planning by SAT for details), with several extensions to handle the far more complex model with real-valued timelines and concurrency of actions.

Benchmark sets

We have translated standard PDDL 2.1 benchmarks into NDL. The first is a translation from the PDDL 2.1 version of the benchmarks expressed in terms of multi-valued state variables. With this modeling, it is not necessary to automatically recognize exactly-one (or at-most-one) invariants (although in some cases there are still some invariants adding which into the SMT encoding has a performance advantage.) The second variant is a Boolean representation, closely matching to the old-fashioned PDDL 2.1 Boolean modeling (mix of Boolean and numeric variables, instead of multi-valued, Boolean and numeric). With this representation, recognizing the relevant at-most-one invariants is essential for good performance. The computation of temporal invariants can, however, in some cases, take a substantial amount of time.

Software

Publications

Jussi Rintanen. Schematic invariants by reduction to ground invariants. In Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, 2017. (© 2017 American Association for Artificial Intelligence. AAAI)

Jussi Rintanen. Models of actions concurrency in temporal planning. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), AAAI Press, pages 1659-1665, 2015.

Jussi Rintanen. Discretization of temporal models with application to planning with SMT. In Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, pages 3349-3355, 2015. (© 2015 American Association for Artificial Intelligence. AAAI)

Jussi Rintanen. Impact of modeling languages on the theory and practice in planning research. In Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, pages 4052-4056, 2015. (© 2015 American Association for Artificial Intelligence. AAAI) (slides)

Jussi Rintanen. Constraint-based algorithm for computing temporal invariants. In Proceedings of the European Conference on Logic in Artificial Intelligence, Lecture Notes in Computer Science 8761, pages 665-673, Springer-Verlag, 2014.

Jussi Rintanen. Planning as satisfiability: heuristics, Artificial Intelligence Journal, 193, 45-83, December 2012.

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, 8 on 1]

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.

Bibliography

  1. Ji-Ae Shin and Ernest Davis, Processes and continuous change in a SAT-based planner, Artificial Intelligence, 166(1), pages 194-253, 2005. (Introduces SAT-based encodings for planning with timed/hybrid systems as modelled in PDDL 2.1.)
  2. S. A. Wolfman and D. S. Weld, The LPSAT engine & its application to resource planning, In Dean, T., ed., Proceedings of the 16th International Joint Conference on Artificial Intelligence, 310-315, Morgan Kaufmann Publishers, 1999.