Relaxed Exists-Step Plans in Planning as SMT
Authors: Miquel Bofill, Joan Espasa, Mateu Villaret
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In this section we evaluate the impact of the presented encoding under the R2 -step plan semantics and the proposed strategy for eliminating redundant actions. The proposed encoding (R2Chained onwards)1 is compared with the encoding in [Bofill et al., 2016b] which uses the -step semantics (from now on noted as SEM+C), and the two planners Springroll [Scala et al., 2016] and SMTPlan [Cashmore et al., 2016]. The three systems are the most recent non-heuristic numeric planners available. |
| Researcher Affiliation | Academia | Miquel Bofill, Joan Espasa, Mateu Villaret University of Girona, Spain. {miquel.bofill, joan.espasa, mateu.villaret}@udg.edu |
| Pseudocode | No | The paper does not contain any structured pseudocode or algorithm blocks. |
| Open Source Code | Yes | The planner and the non-IPC instances can be obtained from http://imae.udg.edu/recerca/lap/rantanplan/rantanplan.html |
| Open Datasets | Yes | We consider the domains of the third IPC [Long and Fox, 2003] with integer numeric fluents and without quantified preconditions, as the rest of the domains contain features that are not commonly supported by the considered planners. These domains are: Zenotravel, Driverlog, Depots and Rovers. The Petrobras and Planes domains from [Bofill et al., 2016b] are also considered since they have a higher numerical component. |
| Dataset Splits | No | The paper uses various domains (e.g., Zenotravel, Driverlog, Depots, Rovers, Petrobras, Planes) but does not provide specific information about how these datasets are split into training, validation, or test sets for reproducibility. |
| Hardware Specification | Yes | Experiments have been run on 8GB Intel R Xeon R E31220v2 machines at 3.10 GHz |
| Software Dependencies | Yes | Experiments have been run on 8GB Intel R Xeon R E31220v2 machines at 3.10 GHz, using Yices [Dutertre and De Moura, 2006] v2.5.1 as the back-end SMT solver, under the quantifier-free linear integer arithmetic logic [Barrett et al., 2010]. Z3 [de Moura and Bjørner, 2008] v4.5.1 is used as the Max SMT solver to remove redundant actions. |
| Experiment Setup | No | The paper specifies a 'total timeout' of 1 hour for experiments. It discusses the impact of 'orderings' on efficiency and proposes an 'informed ordering', but it does not provide explicit details about hyperparameter values, specific training schedules, or other system-level configurations beyond the comparison of different encodings. |