Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Certifying MIP-based Presolve Reductions for 0-1 Integer Linear Programs

Alexander Hoen, Andy Oertel, Ambros Gleixner, Jakob Nordström

TL;DR

This work shows 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.

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 fea sibility 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.

Certifying MIP-based Presolve Reductions for 0-1 Integer Linear Programs

TL;DR

This work shows 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.

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 fea sibility 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.
Paper Structure (16 sections, 15 equations, 2 figures, 4 tables)

This paper contains 16 sections, 15 equations, 2 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Pseudo-Boolean Proof Logging with Veri-PB
  3. Pseudo-Boolean Reasoning with the Cutting Planes Method
  4. A New Rule for Objective Function Updates
  5. Examples for Proof Logging Syntax
  6. Certifying Presolve Reductions
  7. General Techniques
  8. Primal Reductions
  9. Dual Reductions
  10. Example
  11. Computational Study
  12. Experimental Setup
  13. Overhead of Proof Logging
  14. Verification Performance on Presolve Certificates
  15. Performance Analysis on Constraint Propagation
  16. ...and 1 more sections

Figures (2)

  • Figure 1: A Veri-PB certificate to substitute an implied free variable $x_1$.
  • Figure 2: Running times of Veri-PB vs. PaPILO on test sets PB16 (left) and MIPLIB (right), including all instances with more than 1 seconds in Veri-PB and less than 30 minutes in PaPILO, and excluding timeouts. Green $+$ signs mark optimization and blue $\times$ signs mark decision instances.