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.