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

TL;DR

This paper proves that the satisfiability problem for a specific multi-modal logic over S5 frames is NP-hard, refuting previous conjectures of polynomial-time solvability.

Contribution

It establishes NP-hardness of affine ML-SAT on S5 frames, challenging prior beliefs about its computational complexity.

Findings

Satisfiability for affine ML over S5 frames is NP-hard.

Refutes previous conjecture of polynomial-time solvability.

Highlights the impact of symmetry on computational complexity.

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.