Processes and continuous change in a SAT-based planner

Ji Ae Shin, Ernest Davis

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Pages (from-to)194-253
Number of pages60
JournalArtificial Intelligence
Issue number1-2
StatePublished - Aug 2005


  • Continuous time
  • Metric quantities
  • Processes
  • SAT-based planning

ASJC Scopus subject areas

  • Language and Linguistics
  • Linguistics and Language
  • Artificial Intelligence


Dive into the research topics of 'Processes and continuous change in a SAT-based planner'. Together they form a unique fingerprint.

Cite this