用辅助变量加速对称性破缺的可验证证明，显著提升效率。
Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables
- 改用辅助变量编码字典序，避免大整数瓶颈。
- 实验显示证明生成与校验速度提升数量级。
- 适合需要高可靠性证明的自动推理系统开发者。
对称性破缺是现代组合求解中的关键技术，但其正确实现难以保证。最有效的应对方法是让求解器具备可验证性，即输出不仅包含解，还包含符合标准格式的数学证明，供形式化验证工具检查。这要求在证明中解释对称性推理，但高效实现这一目标仍是长期未解难题。Bogaerts 等人（2023）提出了一种通用方法，但依赖大整数编码字典序，对大规模对称性迅速失效。本文提出使用辅助变量编码字典序的新方法，在理论和实践中均实现数量级提速。通过在 state-of-the-art satsuma 对称性破缺器与 VeriPB 证明校验工具链上进行实验验证了该方法的有效性。
原文摘要 · Abstract (English)
Symmetry breaking is a crucial technique in modern combinatorial solving, but it is difficult to be sure it is implemented correctly. The most successful approach to deal with bugs is to make solvers certifying, so that they output not just a solution, but also a mathematical proof of correctness in a standard format, which can then be checked by a formally verified checker. This requires justifying symmetry reasoning within the proof, but developing efficient methods for this has remained a long-standing open challenge. A fully general approach was recently proposed by Bogaerts et al. (2023), but it relies on encoding lexicographic orders with big integers, which quickly becomes infeasible for large symmetries. In this work, we develop a method for instead encoding orders with auxiliary variables. We show that this leads to orders-of-magnitude speed-ups in both theory and practice by running experiments on proof logging and checking for SAT symmetry breaking using the state-of-the-art satsuma symmetry breaker and the VeriPB proof checking toolchain.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。