## Invited Session Wed.2.H 0110

#### Wednesday, 13:15 - 14:45 h, Room: H 0110

**Cluster 10: Implementations & software** [...]

### Exact MIP/LP solvers

**Chair: Daniel Steffy**

**Wednesday, 13:15 - 13:40 h, Room: H 0110, Talk 1**

**Sebastian Hoffmann**

Integration of an LP solver into interval constraint propagation

**Coauthors: Ernst Althaus, Bernd Becker, Daniel Dumitriu, Stefan Kupferschmid**

**Abstract:**

In this talk we describe the integration of a linear program (LP) solver into iSAT, a Satisfiability Modulo Theories (SMT) solver that can solve Boolean combinations of linear and nonlinear constraints.

iSAT is a tight integration of the well-known DPLL algorithm and interval constraint propagation (ICP) allowing it to reason about linear and nonlinear constraints.

As interval arithmetic is known to be less efficient on solving linear programs, we will demonstrate how the integration of an LP solver can improve the overall solving performance of iSAT.

**Wednesday, 13:45 - 14:10 h, Room: H 0110, Talk 2**

**Kati Wolter**

An exact rational mixed-integer programming solver

**Coauthors: William Cook, Thorsten Koch, Daniel E. Steffy**

**Abstract:**

We present an exact rational solver for mixed-integer programming that

avoids the numerical inaccuracies inherent in the floating-point

computations used by existing software. This allows the solver to be used

for establishing theoretical results and in applications where correct

solutions are critical due to legal and financial consequences. Our solver

is a hybrid symbolic/numeric implementation of LP-based branch-and-bound,

using numerically-safe methods for all binding computations in the search

tree. Computing provably accurate solutions by dynamically choosing the

fastest of several safe dual bounding methods, our exact solver is only

moderately slower than an inexact floating-point branch-and-bound

solver. The software is incorporated into the SCIP optimization

framework. Computational results are presented for a suite of test

instances taken from the MIPLIB and Mittelmann libraries and for a collection of numerically difficult instances.

**Wednesday, 14:15 - 14:40 h, Room: H 0110, Talk 3**

**Ojas Parekh**

Computing certificates for integer programs

**Coauthors: Robert D. Carr, Harvey J. Greenberg, Cynthia A. Phillips**

**Abstract:**

A certificate for a integer programming (IP) computation is information that allows an independent program to check that the output is correct, preferably far faster than the time required to compute the solution. The canonical example is the primal/dual certificate for a linear program (LP). Although solving an LP can take a large amount of time, checking a certificate requires two matrix vector multiplications and two dot products. A brute force

certificate for an integer program branch-and-bound computation must prove that each branching operation, added cut, and fathoming operation is correct. We will discuss what this entails in the context of PICO, our massively parallel integer programming solver. We give

certificates for some general cut classes and discuss ways to prove the correctness of a general cut, which is equivalent to another integer program. These integer programs appear to be significantly easier than the original IP. Intuitively, they are equivalent to proving integer infeasibility for the polytopes "cut off''. We will discuss numerical and other implementation issues and give computational results for moderate-sized IPs.