Author: Ji-Ae
Shin

Advisor: Ernest Davis

**Abstract**

In any domain
with change, the dimension of time is inherently involved. Whether the domain
should be modeled in discrete time or continuous time depends on aspects of the
domain to be modeled. Many complex real-world domains involve continuous time,
resources, metric quantities and concurrent actions. Planning in such domains
must necessarily go beyond simple discrete models of time and change.

In this thesis, we show how the SAT-based
planning framework can be extended to generate plans of concurrent asynchronous
actions that may depend on or make change piecewise linear metric constraints in
continuous time.

In the SAT-based planning framework, a planning problem is formulated as
a satisfiability problem of a set of propositional constraints (axioms) such
that any model of the axioms corresponds to a valid plan. There are two
parameters to a SAT-based planning system: an encoding scheme for representing
plans of bounded length and a propositional SAT solver to search for a model. The
LPSAT architecture is composed of a SAT solver integrated with a linear
arithmetic constraint solver in order to deal with metric aspects of domains.

We present encoding schemes for temporal models of continuous time defined
in PDDL+: (i) Durative actions with discrete and/or
continuous changes; (ii) Real-time temporal model with exogenous events and autonomous
processes capturing continuous changes. The encoding represents, in a CNF
formula over arithmetic constraints and propositional fluents,
time-stamped parallel plans possibly with concurrent continuous and/or discrete
changes. In addition, we present encoding schemes for multi-capacity resources,
partitioned interval resources, and metric quantities which are represented as
intervals. An interval type can be used as
a parameter to action as well as a fluent type.

Based on the LPSAT engine, the TM-LPSAT temporal metric planner has been
implemented: Given a PDDL+ representation of a planning problem, the compiler
of TM-LPSAT translates it in a CNF formula, which is fed into the LPSAT engine
to find a solution corresponding to a plan for the planning problem. We also have
experimented on our temporal metric encodings with other decision procedure, MathSAT, which deals with propositional combinations of
linear constraints and Boolean variables. The results show that in terms of
searching time the SAT-based approach to temporal metric planning can be
comparable to other planning approaches and there is plenty of room to push
further the limits of the SAT-based approach.