Bibliographic Details
| Title: |
Satisfiability Modulo Theories for Verifying MILP Certificates |
| Authors: |
Wood, Kenan, Zhou, Runtian, Wu, Haoze, Mendes, Hammurabi, Pulaj, Jonad |
| Publication Year: |
2023 |
| Collection: |
Computer Science |
| Subject Terms: |
Computer Science - Logic in Computer Science |
| More Details: |
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 |
| Document Type: |
Working Paper |
| Access URL: |
http://arxiv.org/abs/2312.10420 |
| Accession Number: |
edsarx.2312.10420 |
| Database: |
arXiv |
