Correctness of results from mixed-integer linear programming (MILP) solvers is critical, particularly in the context of applications such as hardware verification, compiler optimization, or machine-assisted theorem proving. To this end, VIPR 1.0 is the first recently proposed general certificate format for answers produced by MILP solvers. We design a schema to encode VIPR's inference rules as a ground formula that completely characterizes the validity of the algorithmic check, removing any ambiguities and imprecisions present in the specification. We implement a checker for VIPR certificates by expressing our ground formula with the Satisfiability Modulo Theory Library (SMT-LIB) and check its validity. Our approach is solver-agnostic, and we test its viability using benchmark instances found in the literature.

翻译：混合整数线性规划（MILP）求解器结果的正确性至关重要，尤其是在硬件验证、编译器优化或机器辅助定理证明等应用背景下。为此，VIPR 1.0 是近期首个提出的、用于MILP求解器输出答案的通用证书格式。我们设计了一种方案，将VIPR的推理规则编码为一个完全刻画算法检查有效性的基公式，从而消除了规范中存在的任何模糊性和不精确性。我们通过使用可满足性模理论库（SMT-LIB）表达我们的基公式，并检查其有效性，实现了一个VIPR证书检查器。我们的方法与求解器无关，并使用文献中的基准实例测试了其可行性。