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

Authors

  • Thomas Caridroit CRIL, Artois University and CNRS
  • Jean-Marie Lagniez CRIL, Artois University and CNRS
  • Daniel Le Berre CRIL, Artois University and CNRS
  • Tiago de Lima CRIL, Artois University and CNRS
  • Valentin Montmirail CRIL, Artois University and CNRS

DOI:

https://doi.org/10.1609/aaai.v31i1.11128

Keywords:

Modal Logic S5, Translation into SAT, Propositional Logic, NP-complete, Benchmarks

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 phi 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 phi and to evaluate the effect of our caching technique. We also compared our solver againstexisting 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)

Downloads

Published

2017-02-12

How to Cite

Caridroit, T., Lagniez, J.-M., Le Berre, D., de Lima, T., & Montmirail, V. (2017). A SAT-Based Approach for Solving the Modal Logic S5-Satisfiability Problem. Proceedings of the AAAI Conference on Artificial Intelligence, 31(1). https://doi.org/10.1609/aaai.v31i1.11128

Issue

Section

Main Track: Search and Constraint Satisfaction