# Certified Symmetry and Dominance Breaking for Combinatorial Optimisation

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

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 69 references that are in the map.
- First posted on arXiv 23 Mar 2022.

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

- [Efficient Certified RAT Verification](https://mlsanity.com/paper/1612.02353/) (2016)
- [Efficient Certified Resolution Proof Checking](https://mlsanity.com/paper/1610.06984/) (2016)
- [Verifying Integer Programming Results](https://mlsanity.com/paper/1611.08832/) (2016)
- [A Computational Status Update for Exact Rational Mixed Integer Programming](https://mlsanity.com/paper/2101.09141/) (2021)
- [Finding Maximum k-Cliques Faster using Lazy Global Domination](https://mlsanity.com/paper/1408.6485/) (2014)

## Built on by (most cited first, 13 of 13)

- [Distribution-Specific Auditing For Subgroup Fairness](https://mlsanity.com/paper/2401.16439/) (2024)
- [Certified MaxSAT Preprocessing](https://mlsanity.com/paper/2404.17316/) (2024)
- [Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability](https://mlsanity.com/paper/2501.17493/) (2025)
- [The Complexity of Symmetry Breaking Beyond Lex-Leader](https://mlsanity.com/paper/2407.04419/) (2024)
- [Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach](https://mlsanity.com/paper/2508.07015/) (2025)
- [Pseudo-Boolean Proof Logging for Optimal Classical Planning](https://mlsanity.com/paper/2504.18443/) (2025)
- [Efficient Certified Reasoning for Binarized Neural Networks](https://mlsanity.com/paper/2507.02916/) (2025)
- [Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables](https://mlsanity.com/paper/2511.16637/) (2025)
- [Orbitopal Fixing in SAT](https://mlsanity.com/paper/2601.16855/) (2026)
- [Streaming LRAT Certificates into Lean Theorems](https://mlsanity.com/paper/2607.00815/) (2026)
- [Towards a Certifying Grounder](https://mlsanity.com/paper/2607.21199/) (2026)
- [LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean](https://mlsanity.com/paper/2607.28459/) (2026)
- [The Refutation Gap: Certifying Both Halves of an Optimality Claim](https://mlsanity.com/paper/2609.20873/) (2026)

## Abstract (arXiv)

Symmetry and dominance breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly. Building on the cutting planes proof system, we develop a certification method for optimisation problems in which symmetry and dominance breaking are easily expressible. Our experimental evaluation demonstrates that we can efficiently verify fully general symmetry breaking in Boolean satisfiability (SAT) solving, thus providing, for the first time, a unified method to certify a range of advanced SAT techniques that also includes XOR and cardinality reasoning. In addition, we apply our method to maximum clique solving and constraint programming as a proof of concept that the approach applies to a wider range of combinatorial problems.