Satisfiability Modulo Theories for Verifying MILP Certificates
| Autor: | Wood, Kenan, Zhou, Runtian, Wu, Haoze, Mendes, Hammurabi, Pulaj, Jonad |
|---|---|
| Rok vydání: | 2023 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: Redesigned and optimized the transformation to a ground formula. Reimplemented the transformation in a more functional style of programming. Expanded the experiments. Improved exposition |
| Databáze: | arXiv |
| Externí odkaz: |
|