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.

翻译：对称性和支配性剪枝对于解决困难的组合搜索和优化问题至关重要，但这些技术的正确性有时依赖于微妙的论证。因此，我们需要能够生成高效且可机器验证的证书，以证明解的正确性。基于切割平面证明系统，我们开发了一种针对优化问题的认证方法，在该方法中，对称性和支配性剪枝能够被轻松表达。实验评估表明，我们能够高效地验证布尔可满足性（SAT）求解中完全通用的对称性剪枝，从而首次为包括XOR和基数推理在内的一系列高级SAT技术提供了统一的认证方法。此外，作为概念验证，我们将该方法应用于最大团求解和约束规划，证明该方法适用于更广泛的组合问题。