We present a SMT-based checker for the recently proposed VIPR certificate, the first proof format for the correctness of answers produced by mixed-integer linear programming (MILP) solvers. The checker is based on the equivalence between the correctness of a VIPR certificate and the satisfiability of a formula in the theory of linear/integer real arithmetic. Evaluation on existing benchmark instances demonstrates the effectiveness of this approach.

翻译：我们提出了一种基于SMT的检验器，用于验证最新提出的VIPR证书——这是首个针对混合整数线性规划（MILP）求解器输出结果正确性的证明格式。该检验器基于VIPR证书正确性与线性/整数实数算术理论中公式可满足性之间的等价关系。对现有基准实例的评估表明，该方法具有有效性。