Modal Logic S5 Satisfiability in Answer Set Programming
  Modal logic S5 has attracted significant attention and has led to several
practical applications, owing to its simplified approach to dealing with
nesting modal operators. Efficient implementations for evaluating
satisfiability of S5 formulas commonly rely on Skolemisation to convert them
into propositional logic formulas, essentially by introducing copies of
propositional atoms for each set of interpretations (possible worlds). This
approach is simple, but often results into large formulas that are too
difficult to process, and therefore more parsimonious constructions are
required. In this work, we propose to use Answer Set Programming for
implementing such constructions, and in particular for identifying the
propositional atoms that are relevant in every world by means of a reachability
relation. The proposed encodings are designed to take advantage of other
properties such as entailment relations of subformulas rooted by modal
operators. An empirical assessment of the proposed encodings shows that the
reachability relation is very effective and leads to comparable performance to
a state-of-the-art S5 solver based on SAT, while entailment relations are
possibly too expensive to reason about and may result in overhead. This paper
is under consideration for acceptance in TPLP.
