Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Certifying MIP-Based Presolve Reductions for 0–1 Integer Linear Programs

Hoen, Alexander ; Oertel, Andy LU orcid ; Gleixner, Ambros and Nordström, Jakob LU (2024) 21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, CPAIOR 2024 In Lecture Notes in Computer Science 14742. p.310-328
Abstract
It is well known that reformulating the original problem can be crucial for the performance of mixed-integer programming (MIP) solvers. To ensure correctness, all transformations must preserve the feasibility status and optimal value of the problem, but there is currently no established methodology to express and verify the equivalence of two mixed-integer programs. In this work, we take a first step in this direction by showing how the correctness of MIP presolve reductions on 0–1 integer linear programs can be certified by using (and suitably extending) the VeriPB tool for pseudo-Boolean proof logging. Our experimental evaluation on both decision and optimization instances demonstrates the computational viability of the approach and... (More)
It is well known that reformulating the original problem can be crucial for the performance of mixed-integer programming (MIP) solvers. To ensure correctness, all transformations must preserve the feasibility status and optimal value of the problem, but there is currently no established methodology to express and verify the equivalence of two mixed-integer programs. In this work, we take a first step in this direction by showing how the correctness of MIP presolve reductions on 0–1 integer linear programs can be certified by using (and suitably extending) the VeriPB tool for pseudo-Boolean proof logging. Our experimental evaluation on both decision and optimization instances demonstrates the computational viability of the approach and leads to suggestions for future revisions of the proof format that will help to reduce the verbosity of the certificates and to accelerate the certification and verification process further. (Less)
Please use this url to cite or link to this publication:
author
; ; and
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
host publication
Integration of Constraint Programming, Artificial Intelligence, and Operations Research : 21st International Conference, CPAIOR 2024, Uppsala, Sweden, May 28–31, 2024, Proceedings, Part I - 21st International Conference, CPAIOR 2024, Uppsala, Sweden, May 28–31, 2024, Proceedings, Part I
series title
Lecture Notes in Computer Science
editor
Dilkina, Bistra
volume
14742
pages
310 - 328
publisher
Springer
conference name
21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research, CPAIOR 2024
conference location
Uppsala, Sweden
conference dates
2024-05-28 - 2024-05-31
external identifiers
  • scopus:85194011123
ISSN
0302-9743
1611-3349
ISBN
978-3-031-60597-0
978-3-031-60596-3
DOI
10.1007/978-3-031-60597-0_20
language
English
LU publication?
yes
id
cfa7f9df-a2a4-4372-871d-e09b7b7b1e1d
date added to LUP
2024-09-09 10:22:26
date last changed
2025-07-16 08:32:56
@inproceedings{cfa7f9df-a2a4-4372-871d-e09b7b7b1e1d,
  abstract     = {{It is well known that reformulating the original problem can be crucial for the performance of mixed-integer programming (MIP) solvers. To ensure correctness, all transformations must preserve the feasibility status and optimal value of the problem, but there is currently no established methodology to express and verify the equivalence of two mixed-integer programs. In this work, we take a first step in this direction by showing how the correctness of MIP presolve reductions on 0–1 integer linear programs can be certified by using (and suitably extending) the VeriPB tool for pseudo-Boolean proof logging. Our experimental evaluation on both decision and optimization instances demonstrates the computational viability of the approach and leads to suggestions for future revisions of the proof format that will help to reduce the verbosity of the certificates and to accelerate the certification and verification process further.}},
  author       = {{Hoen, Alexander and Oertel, Andy and Gleixner, Ambros and Nordström, Jakob}},
  booktitle    = {{Integration of Constraint Programming, Artificial Intelligence, and Operations Research : 21st International Conference, CPAIOR 2024, Uppsala, Sweden, May 28–31, 2024, Proceedings, Part I}},
  editor       = {{Dilkina, Bistra}},
  isbn         = {{978-3-031-60597-0}},
  issn         = {{0302-9743}},
  language     = {{eng}},
  month        = {{05}},
  pages        = {{310--328}},
  publisher    = {{Springer}},
  series       = {{Lecture Notes in Computer Science}},
  title        = {{Certifying MIP-Based Presolve Reductions for 0–1 Integer Linear Programs}},
  url          = {{http://dx.doi.org/10.1007/978-3-031-60597-0_20}},
  doi          = {{10.1007/978-3-031-60597-0_20}},
  volume       = {{14742}},
  year         = {{2024}},
}