论文标题
认证的对称性和优势优化的优势破坏
Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
论文作者
论文摘要
对称和主导地位破坏对于解决硬组合搜索和优化问题至关重要，但是这些技术的正确性有时依赖于微妙的论点。因此，希望能够正确计算解决方案的高效，可验证的证书。在切割平面系统的基础上，我们开发了一种认证方法来优化问题，其中对称性和优势破坏很容易表达。我们的实验评估表明，我们可以有效地验证布尔可满足性（SAT）解决（SAT）解决的完全一般对称性破坏，从而首次提供了一种统一的方法来证明一系列先进的SAT技术，该技术也包括XOR和心脏性推理。此外，我们将我们的方法应用于最大集团解决和约束编程，作为该方法适用于更广泛组合问题的概念证明。
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.
