组合优化中的认证对称性与支配破坏
摘要：对称性和主导分解对于解决困难的组合搜索和优化问题非常重要，但这些技术的正确性有时依赖于微妙的论证。因此，产生一个能够证明解决方案已正确计算的高效的、可机器验证的证书是非常理想的。基于切割平面证明系统，我们开发了一种优化问题的认证方法，其中对称性和主导分解很容易表达。我们的实验评估表明，我们可以有效地验证布尔满足（SAT）求解中的完全通用对称性分解，从而首次提供了一种统一的方法来证明一系列高级SAT技术，包括异或和基数推理。此外，我们将我们的方法应用于最大团问题的解决和约束编程中，作为一个概念验证，证明这种方法适用于更广泛的组合问题。
作者：Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, Jakob Nordstr"om
论文ID：2203.12275
分类：Artificial Intelligence
分类简称：cs.AI
提交时间：2023-08-17