为0-1整数线性规划的MIP预处理简化提供认证
Certifying MIP-based Presolve Reductions for 0-1 Integer Linear Programs
AI总结：
本文提出利用VeriPB工具对0-1整数线性规划的MIP预处理简化进行正确性认证，实验验证了其计算可行性，并为未来证明格式修订提供建议。
摘要：
众所周知，对原始问题进行重构对于混合整数规划（MIP）求解器的性能至关重要。为确保正确性，所有变换必须保持问题的可行状态和最优值，但目前尚无既定的方法论来表达和验证两个混合整数规划之间的等价性。在本工作中，我们朝这一方向迈出了第一步，展示了如何通过使用（并适当扩展）用于伪布尔证明记录的VeriPB工具，来认证0-1整数线性规划上MIP预处理简化的正确性。我们在决策实例和优化实例上的实验评估证明了该方法的计算可行性，并为未来修订证明格式提出了建议，这些修订将有助于减少证明的冗长性，并进一步加速认证和验证过程。
英文摘要：
It is well known that reformulating the original problem can be crucial for the performance of mixed-integer programming (MIP) solvers. To ensure correctness, all transformations must preserve the fea sibility status and optimal value of the problem, but there is currently no established methodology to express and verify the equivalence of two mixed-integer programs. In this work, we take a first step in this direction by showing how the correctness of MIP presolve reductions on 0-1 integer linear programs can be certified by using (and suitably extending) the VeriPB tool for pseudo-Boolean proof logging. Our experimental evaluation on both decision and optimization instances demonstrates the computational viability of the approach and leads to suggestions for future revisions of the proof format that will help to reduce the verbosity of the certificates and to accelerate the certification and verification process further.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
