SMT-Based Nonlinear PDDL+ Planning
Authors: Daniel Bryce, Sicun Gao, David Musliner, Robert Goldman
AAAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We evaluate our solver on both linear and nonlinear variations of the generator and car problems from the literature and a new domain that plans how to dribble a ball subject to nonlinear drag and gravity. 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. |
| Researcher Affiliation | Collaboration | Daniel Bryce SIFT, LLC. dbryce@sift.net Sicun Gao MIT CSAIL sicung@csail.mit.edu David Musliner & Robert Goldman SIFT, LLC. {musliner, rpgoldman}@sift.net |
| Pseudocode | Yes | Algorithm 1: Extend a choice stack to a complete path. |
| Open Source Code | No | The paper does not provide an explicit statement about releasing the source code for the methodology described, nor does it provide a link to a code repository. |
| Open Datasets | Yes | We use the generator and car domains from the literature (Bogomolov et al. 2014) and a new domain called Dribble. |
| Dataset Splits | No | The paper evaluates its solver on problem instances from established domains (car, generator) and a new one (Dribble) but does not provide specific training/validation/test dataset splits, percentages, or cross-validation details typically found in machine learning contexts. |
| Hardware Specification | No | The paper does not explicitly describe the specific hardware (e.g., GPU/CPU models, memory) used to run its experiments. |
| Software Dependencies | No | The paper mentions several software components used (d Real solver, SAT solver, ICP solver, DPLL(T) framework, CAPD library) but does not provide specific version numbers for any of them. |
| Experiment Setup | Yes | We report results for the minimal step encoding required to solve each instance. In all experiments comparing with other planners, d Real uses all heuristics and δ = 0.1. We first show experiments that evaluate d Real with and without the heuristics described in the previous section and for various values of δ. The first time that ICP selects a time variable ti with interval [lb(ti), ub(ti)], we split its interval into the two subintervals [lb(ti), lb(ti) + ϵ] and [lb(ti) + ϵ, ub(ti)]. |