Efficient SAT-based minimal model generation methods for modal logic S5

DOI10.1007/978-3-030-80223-3_16OpenAlexW3194823730MaRDI QIDQ2118302

Minghao Liu, Jian Zhang, Feifei Ma, Pei Huang, Rundong Li

Publication date: 22 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-80223-3_16

zbMATH Keywords

symmetry breakingSATMaxSATminimal modelmodal logic S5

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational aspects of satisfiability (68R07)

Uses Software

• RC2

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Three new upper bounds on the chromatic number
• A simple propositional \(\text{S}5\) tableau system
• An assumption-based approach for solving the minimal S5-satisfiability problem
• A benchmark method for the propositional modal logics K, KT, S4
• Operational semantics and program verification using many-sorted hybrid modal logic
• A Tableau Calculus for Minimal Modal Model Generation
• Terminating Minimal Model Generation Procedures for Propositional Modal Logics
• One-Pass Tableaux for Computation Tree Logic
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• RC2: an Efficient MaxSAT Solver
• Weak models of distributed computing, with connections to modal logic