Notice: 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. Full accuracy metrics and methodology are described in [1].
ITSAT: An Efficient SAT-Based Temporal Planner
Authors: Masood Feyzbakhsh Rankooh, Gholamreza Ghassem-Sani
JAIR 2015 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our empirical results show that not only does ITSAT outperform the state-of-the-art temporally expressive planners, it is also competitive with the fast temporal planners that cannot handle required concurrency. |
| Researcher Affiliation | Academia | Masood Feyzbakhsh Rankooh EMAIL Gholamreza Ghassem-Sani EMAIL Computer Engineering Department, Sharif University of Technology, Azadi ave., Tehran, Iran |
| Pseudocode | Yes | We define chain(e1, ..., en; E; R; k; m) by the conjunction of formulae (C-1) to (C-3) stated below. (C-1) V{ek i bk j,m|i < j, ei E, ej R, {ei+1, ..., ej 1} R = } (C-2) V{bk i,m bk j,m|i < j, {ei, ej} R, {ei+1, ..., ej 1} R = } (C-3) V{bk i,m ek i |ei R} |
| Open Source Code | No | The paper does not provide explicit statements or links for the open-sourcing of ITSAT's code. It mentions using third-party tools like VAL and Precosat. |
| Open Datasets | Yes | As our benchmark problems, we have used the problem sets of all previous IPCs. These problems are from different planning domains including zenotravel, rovers, and depots of IPC 2004, airport of IPC 2006, pegsol, crewplanning, openstacks, elevators, sokoban, and parcprinter of IPC 2011, and driverlog, floortile, matchcellar, mapanalyser, parking, rtam, satellite, storage, turnandopen, and tms of IPC 2014. ... The corrected version of mentioned domains can be downloaded from the official website of POPF planner. |
| Dataset Splits | No | This paper focuses on AI planning problems and their solution, not on training machine learning models on datasets. The concept of training/test/validation splits is therefore not applicable in the context of this research. |
| Hardware Specification | Yes | All the experiments explained in this section have been conducted on a 3.1GHz corei5 CPU with 4GB main memory. |
| Software Dependencies | Yes | In the current version of ITSAT, we use Precosat (Biere, 2009), which is a free off-the-shelf system, as our SAT solver. We have also examined two other SAT solvers, namely Minisat (E en & Biere, 2005) and Lingeling (Biere, 2013) for satisfying the formulae. |
| Experiment Setup | Yes | For each problem, we start with a formula with just one step. We set a time limit of three minutes for precosat to find a model for the formula. In the case of the failure, we add three more steps to the formula and repeat this process until either a model is found or a predetermined maximum time of 30 minutes is reached. |