FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem

Authors: Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail

Paper Information

Title:An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Authors:Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail
Proceedings:IJCAR Proceedings 9th IJCAR, 2018
Editors: Stephan Schulz, Didier Galmiche and Roberto Sebastiani
Keywords:Modal Logic, S5, Incremental SAT, Minimisation
Abstract:

ABSTRACT. Recent work on the practical aspects on the modal logic S5 satisfiability problem showed that using a SAT-based approach outperforms other existing approaches. In this work, we go one step further and study the related minimal S5 satisfiability problem (MinS5-SAT), the problem of finding an S5 model, a Kripke structure, with the smallest number of worlds.

Finding a small S5 model is crucial as soon as the model should be presented to a user, displayed on a screen for instance. SAT-based approaches tend to produce S5-models with a large number of worlds, thus the need to minimize them.

That optimization problem can obviously be solved as a pseudo-Boolean optimization problem. We show in this paper that it is also equivalent to the extraction of a maximal satisfiable set (MSS). It can thus be solved using a standard pseudo-Boolean or MaxSAT solver, or an MSS-extractor.

We show that a new incremental, SAT-based approach can be proposed by taking into account the equivalence relation between the possible worlds on S5 models. That specialized approach presented the best performance on our experiments conducted on a wide range of benchmarks from the modal logic community and a wide range of pseudo-Boolean and MaxSAT solvers.

Our results demonstrate once again that domain knowledge is key to building efficient SAT-based tools.

Pages:16
Talk:Jul 14 14:00 (Session 96E: SAT Extensions & Applications)
Paper: