Certifying MIP-based Presolve Reductions for 0-1 Integer Linear Programs
arxiv(2024)
摘要
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 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要