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


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


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


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.


  The main criterion for them is your ability to repay any Wisconsin Loans Online, they are not interested in your previous attempts, the current one is all that matters. What can cause long-term use of Viagra? In the network and other sources of information, there is no reliable data on the long-term use of Viagra and its negative effects on the body.