When Symmetry Yields NP-Hardness: Affine ML-SAT on S5 Frames

2025/12/19 by Krebs, Andreas, Meier, Arne
#Computational Complexity (cs.CC) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2512.17378

Abstract

Hemaspaandra~et~al.~[JCSS 2010] conjectured that satisfiability for multi-modal logic restricted to the connectives XOR and 1, over frame classes T, S4, and S5, is solvable in polynomial time. We refute this for S5 frames, by proving NP-hardness.

Citations

• Complexity of Propositional Abduction for Restricted Sets of Boolean Functions
• The Tractability of Model-Checking for LTL: The Good, the Bad, and the\n Ugly Fragments
• Generalized Modal Satisfiability
• Automatic verification of finite-state concurrent systems using temporal logic specifications

Related

• Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic
• Logics with the axiom of convergence: complexity with a small number of variables in the language (extended version)
• On the Complexity of Elementary Modal Logics
• Generalized Modal Satisfiability
• PSPACE Reasoning for Graded Modal Logics