Processes and Continuous Change in a SAT-based Planner
Ji-Ae Shin and Ernest Davis
The TM-LPSAT planner can construct plans in domains containing
atomic actions and durative actions; events and processes;
discrete, real-valued, and interval-valued fluents;
reusable resources, both numeric and interval-valued; and
continuous linear change to quantities.
It works in three stages. In the first stage, a representation of
the domain and problem in an extended version of PDDL+ is compiled
into a system of Boolean combinations of propositional atoms and linear
constraints over numeric variables. In the second stage, a SAT-based
arithmetic constraint solver, such as LPSAT or MathSAT, is used to find
a solution to the system of constraints. In the third stage, a correct
plan is extracted from this solution.
We discuss the structure of the planner and show how planning with time
and metric quantities is compiled into a system of constraints.
The proofs of soundness and completeness over a substantial subset of
our extended version of PDDL+ are presented.