# Exploiting Symmetries in MUS Computation (Extended version)

arXiv: https://arxiv.org/abs/2412.13606 · HTML: https://mlsanity.com/paper/2412.13606/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 34 references that are in the map.
- First posted on arXiv 18 Dec 2024.

## Builds on (most cited first, 3 of 3)

- [A Commentary on "Breaking Row and Column Symmetries in Matrix Models"](https://mlsanity.com/paper/1910.01423/) (2019)
- [A framework for step-wise explaining how to solve constraint satisfaction problems](https://mlsanity.com/paper/2006.06343/) (2020)
- [Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended algorithms and examples)](https://mlsanity.com/paper/2303.11712/) (2023)

## Abstract (arXiv)

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.