Optimal Planning Modulo Theories
Authors: Francesco Leofante, Enrico Giunchiglia, Erika Ábráham, Armando Tacchella
IJCAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present a new encoding for optimal planning in this setting and we evaluate our approach using wellknown, as well as new, numeric benchmarks. |
| Researcher Affiliation | Academia | Imperial College London, United Kingdom University of Genoa, Italy RWTH Aachen University, Germany |
| Pseudocode | Yes | Algorithm 1 Optimal Planning Modulo Theories |
| Open Source Code | Yes | OMTPlan is available at: https://github.com/fraleo/OMTPlan. |
| Open Datasets | Yes | simple numeric domains are taken from [Scala et al., 2017]; linear domains are from [Li et al., 2018]... ; finally, planning problems with SDACs are developed specifically to test OMTPLAN. |
| Dataset Splits | No | The paper evaluates on various planning 'domains' and 'instances' but does not describe a typical machine learning style train/validation/test split for a dataset, nor does it specify validation data or procedures for hyperparameter tuning in that context. |
| Hardware Specification | Yes | Experiments are carried out using a timeout of 30 minutes and 4 GB memory limits on a machine running Debian 3.16 with processor Intel(R) Xeon(R) CPU E5-2640 v4 @ 2.40GHz. |
| Software Dependencies | Yes | Our implementation leverages the modules developed in [Eyerich et al., 2009] for parsing, and uses the Python API3 of νZ [Bjørner et al., 2015] to build and solve OMT formulas. |
| Experiment Setup | Yes | Given a planning problem Π and a user-specified upper bound ub, our procedure builds bounded encodings for increasing horizons (lines 2 4). At each iteration, we check if formula Πopt n is satisfiable. ... Experiments are carried out using a timeout of 30 minutes and 4 GB memory limits... |