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.  



               [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.




              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.




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