Processes and continuous change in a SAT-based planner

Ji Ae Shin, Ernest Davis

Research output: Contribution to journalArticle

Abstract

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
Volume166
Issue number1-2
DOIs
StatePublished - Aug 2005

Fingerprint

Planning
Atoms
planning
event
resources
Satisfiability
time
Atom
Resources
Completeness

Keywords

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

ASJC Scopus subject areas

  • Artificial Intelligence
  • Computational Theory and Mathematics

Cite this

Processes and continuous change in a SAT-based planner. / Shin, Ji Ae; Davis, Ernest.

In: Artificial Intelligence, Vol. 166, No. 1-2, 08.2005, p. 194-253.

Research output: Contribution to journalArticle

@article{483e51ad92214214ad6d83437dc376e3,
title = "Processes and continuous change in a SAT-based planner",
abstract = "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.",
keywords = "Continuous time, LPSAT, Metric quantities, Processes, SAT-based planning",
author = "Shin, {Ji Ae} and Ernest Davis",
year = "2005",
month = "8",
doi = "10.1016/j.artint.2005.04.001",
language = "English (US)",
volume = "166",
pages = "194--253",
journal = "Artificial Intelligence",
issn = "0004-3702",
publisher = "Elsevier",
number = "1-2",

}

TY - JOUR

T1 - Processes and continuous change in a SAT-based planner

AU - Shin, Ji Ae

AU - Davis, Ernest

PY - 2005/8

Y1 - 2005/8

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

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

KW - Continuous time

KW - LPSAT

KW - Metric quantities

KW - Processes

KW - SAT-based planning

UR - http://www.scopus.com/inward/record.url?scp=21444436584&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=21444436584&partnerID=8YFLogxK

U2 - 10.1016/j.artint.2005.04.001

DO - 10.1016/j.artint.2005.04.001

M3 - Article

AN - SCOPUS:21444436584

VL - 166

SP - 194

EP - 253

JO - Artificial Intelligence

JF - Artificial Intelligence

SN - 0004-3702

IS - 1-2

ER -