SAT-Based Explicit LTLf Satisfiability Checking
Authors: Jianwen Li, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, Moshe Y. Vardi2946-2953
AAAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental evaluations show that CDLSC outperforms all other existing approaches for LTLf satisfiability checking, by demonstrating an approximate four-fold speed-up compared to the second-best solver. |
| Researcher Affiliation | Academia | Jianwen Li, Kristin Y. Rozier Iowa State University Ames, IA, USA {jianwen,kyrozier}@iastate.edu Geguang Pu, Yueling Zhang East China Normal University Shanghai, China {ggpu,ylzhang}@sei.ecnu.edu.cn Moshe Y. Vardi Rice University Houston, TX, USA vardi@cs.rice.edu |
| Pseudocode | Yes | Algorithm 1 Implementation of CDLSC; Algorithm 2 Implementation of try satisfy |
| Open Source Code | Yes | We implement CDLSC in the tool aaltaf 2 and use Minisat 2.2.0 (E en and S orensson 2003) as the SAT engine. ... 2https://github.com/lijwen2748/aaltaf |
| Open Datasets | Yes | All artifacts for enabling reproducibility, including benchmark formulas and their generators, are available from the paper website at http://temporallogic.org/research/AAAI19. ... LTL-as-LTLf benchmarks consist of the following. Random Formulas generated as in (Rozier and Vardi 2011)... Counter Formulas scale four... Pattern Formulas encode eight scalable patterns (from (Geldenhuys and Hansen 2006), and are generated by code from (Rozier and Vardi 2007))... Other LTL formulas that were used as specifications in realistic case studies: (Bloem et al. 2007; De Wulf et al. 2008; Filiot, Jin, and Raskin 2009). |
| Dataset Splits | No | The paper evaluates solvers on benchmarks but does not specify dataset splits (e.g., train/validation/test percentages or counts) typically associated with machine learning reproduction. |
| Hardware Specification | Yes | We ran the experiments on a Red Hat 6.0 cluster with 2304 processor cores in 192 nodes (12 processor cores per node), running at 2.83 GHz with 48GB of RAM per node. |
| Software Dependencies | Yes | We implement CDLSC in the tool aaltaf 2 and use Minisat 2.2.0 (E en and S orensson 2003) as the SAT engine. |
| Experiment Setup | Yes | Each tool executed on a dedicated node with a timeout of 60 seconds, measuring execution time with Unix time. |