Certified Symmetry and Dominance Breaking for Combinatorial Optimisation

Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, Jakob Nordström

[AAAI-22] Main Track
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.

Introduction Video

Sessions where this paper appears

  • Poster Session 3

    Blue 5

  • Poster Session 7

    Blue 5

  • Oral Session 3

    Blue 5