Temporalising Separation Logic for Planning with Search Control Knowledge
Authors: Xu Lu, Cong Tian, Zhenhua Duan
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We have implemented a planner S-TSolver which handles SCK in collaborating with the classical forward chaining algorithm and SMT solver Z3 [De Moura and Bjørner, 2008]. To plan with S-TSolver, a domain, an instance and SCK expressed in PPTLSL formulas are taken as input. ... We evaluate the performance of S-TSolver in planning on two domains: City Car and Transport. ... The experiment results are demonstrated in Table 2. |
| Researcher Affiliation | Academia | Xu Lu, Cong Tian and Zhenhua Duan, ICTT and ISN Laboratory, Xidian University Xi an, 710071, P.R. China xulu@stu.xidian.edu.cn, {ctian,zhhduan}@mail.xidian.edu.cn |
| Pseudocode | No | The paper describes algorithms and procedures in text but does not include any structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper mentions implementing a planner called S-TSolver but does not provide any information about the availability of its source code. |
| Open Datasets | Yes | City Car domain encoded in PDDL (Planning Domain Definition Language) standard [Fox and Long, 2003] is a newly introduced benchmark in International Planning Competition (IPC) 2014 [Vallati et al., 2015]. ... Original from IPC2008, the Transport domain is a variant of the well-known domain logistics. |
| Dataset Splits | No | The paper mentions using benchmark domains and problem instances but does not specify any training, validation, or test splits. It focuses on evaluating the planner's performance on selected instances. |
| Hardware Specification | Yes | All the experiments are conducted on a PC running Ubuntu 16.04 on an Intel Core TM i3-550 CPU 3.20GHz and 8Gb of RAM. |
| Software Dependencies | No | The paper mentions the use of 'SMT solver Z3 [De Moura and Bjørner, 2008]' but does not specify a version number for Z3. It also mentions 'SMT-LIB format [Barrett et al., 2010]'. |
| Experiment Setup | No | The paper describes the general process of the planner ('At each step, the forward chaining algorithm responds for exploring the current world of the instance by executing an action, while the equisatisfiable translation (Theorem 1) and the progression technique (Theorem 2) are employed to transform each SCK into its normal form.') but does not provide specific experimental setup details like hyperparameters, optimizer settings, or other training configurations. |