The TM-LPSAT is a temporal
metric planner that is built on the SAT-based planning framework. It can deal
with durative actions,
exogenous events, and autonomous
processes that cause continuous change.
In this planning framework, a planning problem is
compiled into Boolean combinations of
propositional atoms and linear constraints over numeric variables in such a way
that any model
of the system of constraints corresponds
to a valid plan to the original planning problem. A SAT-based arithmetic
constraint solver,
such as LPSAT or MathSAT, is used to find
a solution to the systems of constraints.
Publications
[3] Ji-Ae Shin and Ernest Davis, Processes and Continuous Change in a SAT-based Planner,
Artificial Intelligence Journal, volume 166 (2005), pp. 195-254.
Abstract, Experiments with TM-LPSAT
[2] Ji-Ae Shin and Ernest Davis, Continuous Time in a SAT-based Planner, AAAI, 2004.
[1] Ji-Ae Shin, TM-LPSAT: Encoding Temporal Metric Planning in Continuous Time, Ph.D. Dissertation, NYU, 2004.
Downloads
TM-LPSAT: The encoding generated by TM-LPSAT compiler can be solved by any constraint solver that can handle
Boolean combinations of logical and numeric constraints; currently options for a constraint solver include
LPSAT and three versions of the MathSAT family ( MathSAT 1, MathSAT 2, and MathSAT 3.1.0 ).
· The executable for Linux dealing with PDDL+ Level 5, a deterministic real-time temporal model,
along with Perl scripts to transform the encoding in LCNF and to reconstruct a plan from a model.
Problem Domain: Defined in an extended version of PDDL+ Level 5
· The “Bucket” domain introduced in our AIJ paper [3] and its problem instances #0, #1, #2, #3.
Links
Wolfman and Weld’s LPSAT, a LPSAT constraint solver and its application to a metric planning in discrete time.
The MathSAT family, the SAT-based arithmetic constraint solver built on the layered architecture.
McDermott’s Optop, an estimated regression-based planner that can reason about autonomous processes.
Acknowledgement: The current version of TM-LPSAT was implemented based on Wolfman and Weld’s LPSAT.
Last updated on June 16th, 2005 (contact: jiae.shin at gmail.com)