Temporal Planning with Clock-Based SMT Encodings
Authors: Jussi Rintanen
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We compare our result to the Shin-Davis style step scheme and ITSAT which is one of the the strongest temporal planners [Rankooh and Ghassem-Sani, 2015], shown to outperform earlier planners [Gerevini et al., 2006; Coles et al., 2010; Eyerich et al., 2012; Lu et al., 2013]. Experimentation was based on Rintanen’s [2015a] code, including the discretization method to eliminate time variables whenever possible. We used Math SAT 5.3.6 [Audemard et al., 2005; Cimatti et al., 2013] for instances with real-valued variables, and Preco SAT [Biere, 2010] for purely Boolean ones. Experiments were run in Intel Xeon CPUs. From the SMT approach, SD is the baseline encoding [Rintanen, 2015a]. C is obtained from SD by using the clockbased encodings of resource constraints and delays (Sections 5 and 6). R additionally uses summarized steps (Section 4). Table 1 lists the number of IPC instances solved in 1800 seconds. ITSAT doesn’t handle numeric variables and cannot solve the problems indicated with a dash. Differences between SD, C and R are not clearly visible here: many problem series are solved (almost) completely by all planners, some series are too difficult, and e.g. Parking gets fully discretized and all three planners use the same SAT encoding. Figure 3 plots makespans for instances solved by both ITSAT and R, with ITSAT makespans often close to twice those of R. R makespans are higher only with few instances of TMS. On these, C makespans are the same as ITSAT’s. Figure 4 shows |
| Researcher Affiliation | Academia | Jussi Rintanen Aalto University, Department of Computer Science, Helsinki, Finland Also affiliated with Griffith University, Brisbane, Australia, and the Helsinki Institute for Information Technology, Finland. |
| Pseudocode | No | The paper does not include pseudocode or clearly labeled algorithm blocks. |
| Open Source Code | No | The paper does not provide an explicit statement or link indicating that the source code for the methodology is openly available. |
| Open Datasets | No | The paper mentions “IPC instances” and “standard benchmark problems” but does not provide a specific link, DOI, repository, or formal citation (with authors and year) for accessing these datasets. |
| Dataset Splits | No | The paper does not explicitly specify exact percentages or counts for training, validation, and test dataset splits. |
| Hardware Specification | Yes | Experiments were run in Intel Xeon CPUs. |
| Software Dependencies | Yes | We used Math SAT 5.3.6 [Audemard et al., 2005; Cimatti et al., 2013] for instances with real-valued variables, and Preco SAT [Biere, 2010] for purely Boolean ones. |
| Experiment Setup | No | The paper does not provide specific details on hyperparameters (e.g., learning rate, batch size) or detailed system-level training settings. |