Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2312.10420 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914088110522368 |
|---|---|
| author | Wood, Kenan Zhou, Runtian Wu, Haoze Mendes, Hammurabi Pulaj, Jonad |
| author_facet | Wood, Kenan Zhou, Runtian Wu, Haoze Mendes, Hammurabi Pulaj, Jonad |
| contents | 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 formally verify the correctness of our schema at the logical level using Why3's automated deductive logic framework. Furthermore, we implement a checker for VIPR certificates by expressing our formally verified 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2312_10420 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Satisfiability Modulo Theories for Verifying MILP Certificates Wood, Kenan Zhou, Runtian Wu, Haoze Mendes, Hammurabi Pulaj, Jonad Logic in Computer Science 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 formally verify the correctness of our schema at the logical level using Why3's automated deductive logic framework. Furthermore, we implement a checker for VIPR certificates by expressing our formally verified 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. |
| title | Satisfiability Modulo Theories for Verifying MILP Certificates |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2312.10420 |