Exploiting Symmetries in MUS Computation
Authors: Ignace Bleukx, Hélène Verhaeghe, Bart Bogaerts, Tias Guns
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | 5 Experiments In this section, we evaluate our proposed modifications to algorithms for MUS-computation and enumeration on a set of benchmark instances. We aim to answer the following experimental questions: EQ1 To what extent is making MUS-computation symmetry-aware beneficial in terms of runtime? EQ2 How can symmetries be used for MUS enumeration? EQ3 How do MUS-computation algorithms benefit from the detection of row-interchangeability symmetries? We run all methods presented in this paper on unsatisfiable constraint problems encoded as pseudo-Boolean problems. Our benchmark consists of 272 instances with 146 pigeon-hole problems, 66 n+k-queens problems, and 60 binpacking problems. We implemented all MUS-finding algorithms on top of the CPMpy constraint modeling library (Guns 2019), version 0.9.20 in Python 3.10.14. Pseudo-Boolean solver Exact v1.2.1 (Devriendt 2023; Elffers and Nordstr om 2018) is used as SAT-oracle and Gurobi v11.0.2 as hitting-set-solver. Symmetries are computed using a custom branch of BREAKID2 (Devriendt et al. 2016). All methods were run on a single core of an Intel(R) Xeon(R) Silver 4214 CPU with 128GB of memory on Ubuntu 20.04. We used a time-out of 1h which includes symmetry-detection by BREAKID and unrolling to symmetric MUSes in LEX-MARCO. |
| Researcher Affiliation | Academia | 1KU Leuven, Dept. of Computer Science; Leuven.AI, Celestijnenlaan 200A, 3000 Leuven, Belgium 2UCLouvain, ICTEAM, Place Sainte Barbe 2, 1348 Louvain-la-Neuve, Belgium 3Vrije Universiteit Brussel, Dept. of Computer Science, Pleinlaan 9, 1050 Brussels, Belgium EMAIL, EMAIL, EMAIL, EMAIL |
| Pseudocode | Yes | Algorithm 1: SYMM-SHRINK(ϕ, recompute?) ... Algorithm 2: SYMM-OCUS(ϕ, f, dynamic?) ... Algorithm 3: CORRSUBSETS(S, ϕ, G) ... Algorithm 4: LEX-MARCO(ϕ) |
| Open Source Code | Yes | Code github.com/ML-KULeuven/Symmetry MUS |
| Open Datasets | No | Our benchmark consists of 272 instances with 146 pigeon-hole problems, 66 n+k-queens problems, and 60 binpacking problems. Explanation: The paper describes the types and counts of benchmark instances used but does not provide concrete access information (e.g., a specific link, DOI, or formal citation to where these instances can be downloaded or accessed as a dataset). |
| Dataset Splits | No | Our benchmark consists of 272 instances with 146 pigeon-hole problems, 66 n+k-queens problems, and 60 binpacking problems. Explanation: The paper describes the composition of the benchmark instances used but does not provide information on how these instances were split into training, testing, or validation sets. The problem instances are evaluated directly. |
| Hardware Specification | Yes | All methods were run on a single core of an Intel(R) Xeon(R) Silver 4214 CPU with 128GB of memory on Ubuntu 20.04. |
| Software Dependencies | Yes | We implemented all MUS-finding algorithms on top of the CPMpy constraint modeling library (Guns 2019), version 0.9.20 in Python 3.10.14. Pseudo-Boolean solver Exact v1.2.1 (Devriendt 2023; Elffers and Nordstr om 2018) is used as SAT-oracle and Gurobi v11.0.2 as hitting-set-solver. Symmetries are computed using a custom branch of BREAKID2 (Devriendt et al. 2016). |
| Experiment Setup | Yes | We used a time-out of 1h which includes symmetry-detection by BREAKID and unrolling to symmetric MUSes in LEX-MARCO. ... Here, u is the upperbound on the number of MCSes added in each iteration. |