Notice: This website is continuously updated as new conference proceedings and journal volumes are published. Consequently, the figures presented here may differ from those reported in our publications.
A brief overview of our methodology is provided on the Methods page, along with references to publications documenting our approach and links to the code and data used in each study.
The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates.
Optimal Planning Modulo Theories
Authors: Francesco Leofante, Enrico Giunchiglia, Erika Ábráham, Armando Tacchella
IJCAI 2020 | Venue PDF | LLM Run Details | Input Tokens: 16,365 Total number of tokens sent to the LLM as input for this paper's analysis. | Output Tokens: 3,327 Total number of tokens produced by the LLM (including reasoning/thinking tokens) for this paper's analysis.
| 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... |