Correctness of results returned from mixed-integer linear programming (MILP) solvers is highly desirable, particularly in the context of applications such as hardware verification, compiler optimization, or machine-assisted theorem proving. To this end, VIPR is the first recently proposed certificate format for answers produced by MILP solvers. We design a schema to encode VIPR's inference rules as Satisfiability Modulo Theories (SMT) instances and show the equivalence of the certificates' correctness and the satisfiability of the corresponding SMT instances. In addition, we implement this schema with and without parallelization in a checker for VIPR certificates and test the viability of this approach on benchmark instances found in the literature with the cvc5 solver.

翻译：混合整数线性规划（MILP）求解器返回结果的正确性具有极高需求，特别是在硬件验证、编译器优化或机器辅助定理证明等应用场景中。为此，VIPR成为首个针对MILP求解器输出结果提出的新型证书格式。我们设计了一种将VIPR推理规则编码为可满足性模理论（SMT）实例的框架，并证明了证书正确性与对应SMT实例可满足性的等价性。此外，我们分别以串行和并行方式实现了该框架的VIPR证书验证器，并通过文献中的基准测试实例，利用cvc5求解器验证了该方法的可行性。