SMT-Based Nonlinear PDDL+ Planning

Daniel Bryce, Sicun Gao, David J. Musliner, Robert P. Goldman

AAAI 2015 pp. 3247-3253

doi:10.1609/AAAI.V29I1.9646 /aaai/2015/bryce2015aaai-smt/

Abstract

PDDL+ planning involves reasoning about mixed discrete-continuous change over time. Nearly all PDDL+ planners assume that continuous change is linear. We present a new technique that accommodates nonlinear change by encoding problems as nonlinear hybrid systems. Using this encoding, we apply a Satisfiability Modulo Theories (SMT) solver to find plans. We show that it is important to use novel planning- specific heuristics for variable and value selection for SMT solving, which is inspired by recent advances in planning as SAT. We show the promising performance of the resulting solver on challenging nonlinear problems.

PDF AAAI Semantic Scholar

Cite

Text

Bryce et al. "SMT-Based Nonlinear PDDL+ Planning." AAAI Conference on Artificial Intelligence, 2015. doi:10.1609/AAAI.V29I1.9646

Markdown

[Bryce et al. "SMT-Based Nonlinear PDDL+ Planning." AAAI Conference on Artificial Intelligence, 2015.](https://mlanthology.org/aaai/2015/bryce2015aaai-smt/) doi:10.1609/AAAI.V29I1.9646

BibTeX

@inproceedings{bryce2015aaai-smt,
  title     = {{SMT-Based Nonlinear PDDL+ Planning}},
  author    = {Bryce, Daniel and Gao, Sicun and Musliner, David J. and Goldman, Robert P.},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2015},
  pages     = {3247-3253},
  doi       = {10.1609/AAAI.V29I1.9646},
  url       = {https://mlanthology.org/aaai/2015/bryce2015aaai-smt/}
}