A SAT-Based Approach for Solving the Modal Logic S5-Satisfiability Problem
Authors: Thomas Caridroit, Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail
AAAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We implemented a generic SAT-based approach within the modal logic S5 solver S52SAT. It allowed us to compare experimentally our new upper-bound against previously known one, i.e. the number of modalities of φ and to evaluate the effect of our caching technique. We also compared our solver against existing modal logic S5 solvers. The proposed approach outperforms previous ones on the benchmarks used. |
| Researcher Affiliation | Academia | Thomas Caridroit, Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail CRIL, Univ. Artois and CNRS, F62300 Lens, France {caridroit,lagniez,leberre,delima,montmirail}@cril.fr |
| Pseudocode | No | The paper describes translation functions with mathematical notation but does not include a clearly labeled pseudocode or algorithm block. |
| Open Source Code | Yes | We compared them to 4 different configurations of S52SAT: nm, nm+ (with caching), dd, dd+ (with caching) (http://www.cril.univ-artois.fr/ montmirail/s52SAT). |
| Open Datasets | Yes | We evaluated these solvers on well established modal logic benchmarks: 3CNFK (Patel-Schneider and Sebastiani 2003), MQBFK (Massacci 1999), TANCS 2000K (Massacci and Donini 2000) and LWBK,KT,S 4 (Balsiger, Heuerding, and Schwendimann 2000). |
| Dataset Splits | No | The paper evaluates solvers on benchmarks, which are for testing purposes, but does not describe any training, validation, or test dataset splits typically used for model training and validation. |
| Hardware Specification | No | The paper specifies memory limits (8GB, 32GB RAM) and runtime limits (900 seconds) for the experiments, but does not provide specific details about the CPU, GPU, or other hardware components used. |
| Software Dependencies | Yes | We use Glucose 4.0 (Audemard and Simon 2009) as backend SAT solver. |
| Experiment Setup | Yes | We set the memory limit to 8GB and the runtime limit to 900 seconds. We also considered Met Tel2 (Tishkovsky, Schmidt, and Khodadadi 2012) and Lo TREC (Gasquet et al. 2005). |