Exploiting Symmetries in MUS Computation (Extended version)
Ignace Bleukx, Hélène Verhaeghe, Bart Bogaerts, Tias Guns
TL;DR
This work addresses the computational bottleneck of Minimal Unsatisfiable Subset ($MUS$) computation and enumeration in the presence of problem symmetries. It adapts symmetry-detection and symmetry-exploitation techniques from SAT/PB solving to the MUS context via half-reified encodings and constraint symmetries, introducing methods such as Symm-Shrink, OCUS-based lex-minimization, and symmetry-aware MARCO. The authors formalize constraint symmetries for $MUS$ problems, propose static and dynamic strategies to leverage these symmetries, and demonstrate significant runtime improvements on symmetric benchmarks. The findings indicate that exploiting symmetries can substantially speed up both single MUS discovery and full MUS enumeration, with practical implications for explainable constraint solving and debugging of constraint models.
Abstract
In eXplainable Constraint Solving (XCS), it is common to extract a Minimal Unsatisfiable Subset (MUS) from a set of unsatisfiable constraints. This helps explain to a user why a constraint specification does not admit a solution. Finding MUSes can be computationally expensive for highly symmetric problems, as many combinations of constraints need to be considered. In the traditional context of solving satisfaction problems, symmetry has been well studied, and effective ways to detect and exploit symmetries during the search exist. However, in the setting of finding MUSes of unsatisfiable constraint programs, symmetries are understudied. In this paper, we take inspiration from existing symmetry-handling techniques and adapt well-known MUS-computation methods to exploit symmetries in the specification, speeding-up overall computation time. Our results display a significant reduction of runtime for our adapted algorithms compared to the baseline on symmetric problems.