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
numeric state variables: Wolfman and Weld, The LPSAT engine & its application to resource planning, IJCAI 1999.
continuous time model with continuous change: Shin and Davis, Processes and continuous change in a SAT-based planner, Artificial Intelligence Journal, 166(1), 2005.
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
languages based on timed automata and their extensions (such as hybrid automata)
These languages are favored in the Computer Aided Verification community, due to the
focus on model-checking, in which system models are verified with respect to
complex specifications expressed in temporal logics, and both the models and the
specifications can be translated to timed or hybrid automata.
temporal extensions of PDDL
These are modeling languages that extend the original PDDL 1.0 specification (McDermott et al., 1998). The languages' main limitations are their limited data types (Booleans, reals), awkward syntax and semantics (with no formal semantics in existence), and a non-standard concurrency model that is largely incompatible with efficient constraint-based search and reasoning methods.
other modeling languages developed by the AI planning community, but none enjoy
wide use.
NDL
This is a rich modeling language supporting a wide range of data-types, and in comparison to PDDL, higher abstraction level with explicit resources, and more mainstream model of concurrent actions. My papers in IJCAI and AAAI have demonstrated that natural representations of most standard PDDL benchmarks in SMT, CP, etc. have a significant performance penalty in comparison to NDL models. This is the reason why we exclusively have focused on NDL, and do not recommend using PDDL, even for research purposes.
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.
Encodings have to be compact, preferably linear size.
Number of real-valued variables has to be minimized, and references to real-valued
variables have to be made simple.
Discretization (Rintanen, 2015) sometimes allows very compact encodings with no
real-valued variables, solvable with efficient SAT solvers.
Real-valued variables refer to absolute time and time relative to the start of
an action or an event. The number of linear inequalities referring to these
variables has to be minimized.
Same trade-offs as in classical planning (Rintanen, 2004; Rintanen et al. 2006) hold w.r.t. the number of steps in plans and the difficulty of finding plans.
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.
Values of all state variables are represented at each step.
A step corresponds to one time point in the real or rational-valued timeline.
For every action and every step there is a Boolean state variable indicating
if the action is taken at that step.
Unlike in classical (asynchronous) planning, the absolute time of each step
needs to be represented, either implicitly in terms of the difference
in time between a step and its predecessor, or as the absolute time of the step.
There are constraints preventing a co-occurrence of two actions that use
the same resources. This is similar, but different from the constraints for
parallel plans in SAT-encodings of classical planning: parallelism in the classical
planning case is simply a form of partial-order reduction (possibility to reorder
the actions in a plan without affecting the plans outcome; see (Rintanen et al. 2006)
for details), whereas the concurrency constraints for temporal planning express
the possibilities of having different actions to overlap on the real-valued timeline.
Resources are the main mechanism to limit concurrency at the level of modeling
languages.
The effects of a temporal action can take place at the same step, the next step,
or a step arbitrarily far in the future. How this delay between an action and its
effects is represented is one of the key issues in constraint-based representations
of temporal planning.
Benchmark sets
We have translated standard PDDL 2.1 benchmarks into NDL.
The benchmark set is a straightforward 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.)
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.)
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.