Research map / Learning theory and algorithms / Combinatorial and search optimization
Exploiting Symmetries in MUS Computation
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Adapts MUS computation algorithms (shrinking, IHS/OCUS, MARCO) to exploit constraint symmetries detected via BreakID on half-reified pseudo-Boolean specifications, speeding up MUS computation and enumeration on symmetric benchmarks.
Problem
Finding and enumerating minimal unsatisfiable subsets (MUSes) is expensive for highly symmetric constraint specifications, and symmetry handling has been studied for satisfaction but barely for MUS computation.
Approach
Detect constraint symmetries by reformulating constraints with indicator variables (half-reification) and running a symmetry detection tool on partial assignments; then use these symmetries to mark symmetric transition constraints in shrinking, add lex-leader breaking constraints and symmetric MCS enumeration in IHS/OCUS, and lex-minimal seeds in MARCO.
Key results
- Symm-Shrink solves all instances between 5 and 10 times faster than the default shrink algorithm.
- Lex+Enum finds an MUS for almost double the number of instances compared to OCUS.
- Lex-MARCO completely enumerates the set of MUSes for 197 instances compared to 112 for MARCO.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Remove symmetric transition constraints during shrinking | Shrink · 272 benchmark instances | runtime: 5 and 10 times faster | Helped |
| Recompute symmetries in each iteration (ablation) | Symm-Shrink · Most benchmark instances | runtime | Hurt |
| Disable detection of row-interchangeability symmetries (ablation) | Symm-Shrink · 272 benchmark instances | runtime | Hurt |
| Add symmetry-breaking constraints | OCUS · 272 benchmark instances | instances solved | Helped |
| Enumerate symmetric MCSes | OCUS · 272 benchmark instances | instances solved | Helped |
| Combine symmetry-breaking constraints with symmetric MCS enumeration | OCUS · 272 benchmark instances | instances solved: almost double | Helped |
| Increase the upper bound on added MCSes (ablation) | Enum · Easier benchmark instances | runtime | Hurt |
| Increase the number of extra MCSes while using Lex+Enum (ablation) | Lex+Enum · 272 benchmark instances | instances solved | No clear effect |
| Enumerate lex-minimal seeds and unroll symmetric MUSes | MARCO · 272 benchmark instances | instances with full MUS enumeration within 1h: 112 -> 197 | Helped |
| Return only lex-minimal MUSes before unrolling | Lex-MARCO · 272 benchmark instances | number of MUSes enumerated before unrolling | Hurt |
Surprising findings
- Recomputing symmetries in each shrinking iteration is less efficient, often even slower than the default algorithm.
- Adding more symmetric MCSes beyond a point does not increase instances solved when combined with lex-leader constraints, and performance slightly degrades.
Limitations
- Only symmetry-detection via BreakID (syntactic symmetries) is used; semantic symmetries are not exploited.
- Enumerating many symmetric MCSes can slow the hitting set solver and degrade performance.
- Evaluation limited to pseudo-Boolean encodings of three problem families.
Experimental setup
Datasets: pigeon-hole problems n+k-queens problems bin-packing problems
Benchmarks: pigeon-hole problems n+k-queens bin-packing
Metrics: runtime number of instances solved number of MUSes enumerated
Baselines: Shrink OCUS MARCO Model rotation
Builds on: MARCO BreakID Implicit hitting set MUS/OCUS QuickXplain Model rotation
Closest papers by meaning
- Faster Symmetry Breaking Constraints for Abstract Structures (AAAI 2026 · similarity 0.89)
- The Impact of Literal Sorting on Cardinality Constraint Encodings (AAAI 2025 · similarity 0.85)
- Breaking Symmetries in Quantified Graph Search: A Comparative Study (AAAI 2025 · similarity 0.85)
- Using Symmetries to Lift Satisfiability Checking (AAAI 2024 · similarity 0.85)
- SymILO: A Symmetry-Aware Learning Framework for Integer Linear Optimization (NeurIPS 2024 · similarity 0.84)
- Complete Symmetry Breaking for Finite Models (AAAI 2025 · similarity 0.83)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.