Certified Symmetry and Dominance Breaking for Combinatorial Optimisation

Authors

  • Bart Bogaerts Vrije Universiteit Brussel
  • Stephan Gocht Lund University University of Copenhagen
  • Ciaran McCreesh University of Glasgow
  • Jakob Nordström University of Copenhagen Lund University

DOI:

https://doi.org/10.1609/aaai.v36i4.20283

Keywords:

Constraint Satisfaction And Optimization (CSO)

Abstract

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.

Downloads

Published

2022-06-28

How to Cite

Bogaerts, B., Gocht, S., McCreesh, C., & Nordström, J. (2022). Certified Symmetry and Dominance Breaking for Combinatorial Optimisation. Proceedings of the AAAI Conference on Artificial Intelligence, 36(4), 3698-3707. https://doi.org/10.1609/aaai.v36i4.20283

Issue

Section

AAAI Technical Track on Constraint Satisfaction and Optimization