A SAT-Based Approach for Solving the Modal Logic S5-Satisfiability Problem

Thomas Caridroit Jean-Marie Lagniez 1 Daniel Le Berre 1 Tiago de Lima 1 Valentin Montmirail 1
1 CRIL - Centre de Recherche en Informatique de Lens
Abstract : We present a SAT-based approach for solving the modal logic S5-satisfiability problem. That problem being NP-complete, the translation into SAT is not a surprise. Our contribution is to greatly reduce the number of propositional variables and clauses required to encode the problem. We first present a syntactic property called diamond degree. We show that the size of an S5-model satisfying a formula φ can be bounded by its diamond degree. Such measure can thus be used as an upper bound for generating a SAT encoding for the S5-satisfiability of that formula. We also propose a lightweight caching system which allows us to further reduce the size of the propositional formula. 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. These promising results open interesting research directions for the practical resolution of others modal logics (e.g. K, KT, S4)
Document type :
Conference papers
Complete list of metadatas

Cited literature [36 references]  Display  Hide  Download
https://hal.univ-cotedazur.fr/hal-02271408
Contributor : Valentin Montmirail <>
Submitted on : Monday, August 26, 2019 - 5:50:13 PM
Last modification on : Thursday, August 29, 2019 - 1:20:33 AM

File

AAAI.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02271408, version 1

Collections

UNIV-COTEDAZUR | CNRS | UNIV-ARTOIS

Citation

Thomas Caridroit, Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail. A SAT-Based Approach for Solving the Modal Logic S5-Satisfiability Problem. Thirty-First AAAI Conference on Artificial Intelligence, Feb 2017, San Francisco, United States. ⟨hal-02271408⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

12

Files downloads

10

Support

Université Nice Sophia Antipolis (UNS) Observatoire de la Côte d’Azur (OCA) Centre national de la recherche scientifique (CNRS) Institut national de la recherche en informatique et en automatique (Inria) SKEMA Business School EDHEC Business School  Centre Hospitalier Universitaire de Nice (CHU Nice) Centre National de Création Musicale (CIRM)  Ecole Nationale Supérieure d’Art Villa Arson Ecole Supérieure de Réalisation Audiovisuelle (ESRA) The Sustainable Design School (SDS) Ecole Supérieure de Danse de Cannes Rosella Hightower Conservatoire National à Rayonnement Régional de Nice (CNRR)