CEGAR-Tableaux: Improved Modal Satisfiability via Modal Clause-Learning and SAT
Date
2021
Authors
Gore, Rajeev
Kikkert, Cormac
Journal Title
Journal ISSN
Volume Title
Publisher
Springer Nature Switzerland AG
Abstract
We present CEGAR-Tableaux, a tableaux-like method for propositional modal logics utilising SAT-solvers, modal clause-learning and multiple optimisations from modal and description logic tableaux calculi. We use the standard Counter-example Guided Abstract Refinement (CEGAR) strategy for SAT-solvers to mimic a tableau-like search strategy that explores a rooted tree-model with the classical propositional logic part of each Kripke world evaluated using a SAT-solver. Unlike modal SAT-solvers and modal resolution methods, we do not explicitly represent the accessibility relation but track it implicitly via recursion. By using “satisfiability under unit assumptions”, we can iterate rather than “backtrack” over the satisfiable diamonds at the same modal level (context) of the tree model with one SAT-solver. By keeping modal contexts separate from one another, we add further refinements for reflexivity and transitivity which manipulate modal contexts once only. Our solver CEGARBox is, overall, the best for modal logics K, KT and S4 over the standard benchmarks, sometimes by orders of magnitude.
Description
Keywords
Citation
Collections
Source
Automated Reasoning with Analytic Tableaux and Related Methods
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
Restricted until
2099-12-31
Downloads
File
Description