AAAI Publications, Sixteenth International Conference on Principles of Knowledge Representation and Reasoning

Font Size: 
A SAT-Based Approach For PSPACE Modal Logics
Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail

Last modified: 2018-09-24


SAT solvers have become efficient for solving NP-complete problems (and beyond). Usually, those problems are solved by direct translation to SAT or by solving iteratively SAT problems in a procedure like CEGAR. Recently, a new recursive CEGAR loop working with two abstraction levels, called RECAR, was proposed and instantiated for modal logic K. We aim to complete this work for modal logics based on axioms (B), (D), (T), (4) and (5. Experimental results show that the approach is competitive against state-of-the-art solvers for modal logics K, KT, and S4.


Modal Logics; SAT; Constraints; Benchmarks

Full Text: PDF