TY - JOUR AU - Bryce, Daniel AU - Gao, Sicun AU - Musliner, David AU - Goldman, Robert PY - 2015/03/04 Y2 - 2024/03/29 TI - SMT-Based Nonlinear PDDL+ Planning JF - Proceedings of the AAAI Conference on Artificial Intelligence JA - AAAI VL - 29 IS - 1 SE - Main Track: Planning and Scheduling DO - 10.1609/aaai.v29i1.9646 UR - https://ojs.aaai.org/index.php/AAAI/article/view/9646 SP - AB - <p> 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. </p> ER -