整数规划中证明对称性与最优性推理的证明系统
最优化与控制
2023-11-09 v2
摘要
我们提出了一个用于确立优化算法所产生结果正确性的证明系统，重点关注混合整数规划（MIP）。我们的系统将 Bogaerts、Gocht、McCreesh 和 Nordström（2022）关于二元规划的开创性工作推广到处理由无界和连续变量引起的任何额外困难，并涵盖广泛求解技术，包括对称性处理、割平面和预处理约简。通过对解集上的一对传递关系实现影响可行域的所有决策间的一致性，这依赖于新引入的一致分支树概念。结合一系列机器可验证的推导规则，所得框架提供了实用方案，以增强整数规划作为在可靠性和正确性至关重要的应用中的方法论的可信度。
引用
@article{arxiv.2311.03877,
title = {A proof system for certifying symmetry and optimality reasoning in integer programming},
author = {Jasper van Doornmalen and Leon Eifler and Ambros Gleixner and Christopher Hojny},
journal= {arXiv preprint arXiv:2311.03877},
year = {2023}
}