Discretization of Temporal Models with Application to Planning with SMT
Authors: Jussi Rintanen
AAAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments We have translated IPC benchmark sets (2008 and 2011) for temporal planning into our modeling language. This is mostly straightforward. Parcprinter was excluded, due to its complexity. Table 2 classifies these problems according to whether the problem is discretizable (Theorems 3 and 4), whether some or all of discretizable actions are short (duration at most 5), and whether all actions have unit durations. The last two cases are particularly interesting: encodings in those cases do not contain real variables, and the result is a pure SAT problem. Further, in these two cases plans with the smallest possible number of steps have optimal makespan. Then the translations from earlier in this work were applied to produce input for SMT solvers. Temporal invariants (Rintanen 2014) were included in the SMT encodings. Table 3 gives numbers of problem instances solved for a number of benchmark problems by our planners Cd and C in 1800 seconds of SMT solving time (the Z3 SMT solver on a Intel Xeon E3-1230 at 3.2 GHz). C is our baseline planner, with a Shin&Davis style encoding of steps for all actions.2 Cd is the same planner with the encoding using discretization as presented in the previous section. Both planners increase the number of steps by 3 after the SMT solver determines the current formula to be unsatisfiable. For instances with short durations Cd therefore is guaranteed to always find plans with makespan at most 2 from optimal. The column ITSAT presents runtimes for the ITSAT planner (Rankooh and Ghassem-Sani 2013). |
| Researcher Affiliation | Academia | Jussi Rintanen Department of Information and Computer Science Aalto University, Helsinki, Finland Also affiliated with Griffith University, Brisbane, Australia, and the Helsinki Institute of Information Technology, Finland. |
| Pseudocode | No | The paper describes encoding methods and mathematical proofs but does not include any structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper does not provide any concrete access to source code for the methodology described, nor does it mention a repository link or state that code is available in supplementary materials. |
| Open Datasets | Yes | We have translated IPC benchmark sets (2008 and 2011) for temporal planning into our modeling language. |
| Dataset Splits | No | The paper does not provide specific dataset split information (exact percentages, sample counts, or detailed splitting methodology) for training, validation, or testing. |
| Hardware Specification | Yes | Table 3 gives numbers of problem instances solved for a number of benchmark problems by our planners Cd and C in 1800 seconds of SMT solving time (the Z3 SMT solver on a Intel Xeon E3-1230 at 3.2 GHz). |
| Software Dependencies | No | The paper mentions 'Z3 SMT solver', 'Precosat SAT solver', and 'Mini SAT solver' but does not provide specific version numbers for any of these software components. |
| Experiment Setup | Yes | Both planners increase the number of steps by 3 after the SMT solver determines the current formula to be unsatisfiable.C is our baseline planner, with a Shin&Davis style encoding of steps for all actions.2 Cd is the same planner with the encoding using discretization as presented in the previous section. |