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.
 Ji-Ae Shin and Ernest Davis, Processes and Continuous Change in a SAT-based Planner,
Artificial Intelligence Journal, volume 166 (2005), pp. 195-254.
 Ji-Ae Shin and Ernest Davis, Continuous Time in a SAT-based Planner, AAAI, 2004.
 Ji-Ae Shin, TM-LPSAT: Encoding Temporal Metric Planning in Continuous Time, Ph.D. Dissertation, NYU, 2004.
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
· 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
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)