ExactIP - Exact Integer Programming
Available solvers for mixed integer programs (MIPs) focus on rapidly finding close to optimal solutions for feasible instances. The answers, however, are computed with finite precision, which might lead to wrong results. For most applications, the errors can be neglected. This situation changes fundamentally, if MIPs are used to study theoretical problems (i.e, a "computer proof" is needed), if feasibility questions are considered, and if wrong answers can have legal consequences. For such applications an exact MIP solver is required. The aim of this project is to develop such a solver.
Solvers for MIPs have made tremendous progress in the last years. State-of-the-art MIP solvers, most of which utilize a linear programming (LP) based branch-and-cut approach, have become widely accepted as a powerful tool for tackling optimization problems arising from various industrial applications.
The implementations, however, use (finite-precision) floating-point arithmetic. In the context of MIP solving, this can lead to wrong results. For example, if a Gomory mixed integer cutting plane is added, feasible optimal solutions might be cut off. Furthermore, it may happen that the computed solution is, in fact, not feasible or, even worse, that a solution has been computed, but the MIP itself is infeasible. The risk of claiming infeasible instances to be feasible is the reason why state-of-the-art MIP solvers might not be appropriate for handling feasibility questions of MIPs. Furthermore, they are not adequate if MIPs are used to study theoretical problems and if wrong answers can have legal consequences.
An industrial application where infeasibility plays a prime role is the chip design verification problem (see Matheon-Project Chip Design Verification). Here, the task is to check whether a given chip design satisfies the requirements of a given specification. This problem is usually tackled by transformation into a satisfiability (SAT) problem. Current state-of-the-art SAT solvers, however, show a poor performance for chip properties that involve arithmetic operations, as they often arise in practice. In particular, for larger designs these solvers often fail. Nevertheless, these chip design verification problems can be transformed into feasibility problems which involve integer linear or arithmetic non-linear constraints. To tackle such instances in practice, an exact solver is required, since the feasibility decision must prove whether a chip design is correct or not. If a faulty chip design is declared to be correct, this might lead to huge costs and, maybe even more important, to a loss of reputation for a company.
In this project, we will develop and implement an approach for the exact solution of MIPs. Extending the constraint integer programming framework SCIP, we want to provide a tool, which will be freely available to the scientific community, to compute exact optimal solutions.
At the beginning, we utilize a branch-and-bound approach. Here the main problem is to generate safe dual bounds via the LP relaxation. This approach will then be extended to an exact branch-and-cut approach. This includes the development of exact preprocessing techniques, safe primal heuristics, and safe cutting plane separators. In connection to exact MIP solvers, we will also investigate exact certificates for infeasible MIPs.
- A Hybrid Branch-and-Bound Approach for Exact Rational Mixed-Integer Programming William Cook, Thorsten Koch, Daniel E. Steffy, and Kati Wolter. Accepted for publication in Mathematical Programming Computation. Available as ZIB-Report 12-49, 2012
- Improving the Accuracy of Linear Programming Solvers with Iterative Refinement Ambros Gleixner, Daniel E. Steffy and Kati Wolter. Proceedings of the 37th International Symposium on Symbolic and Algebraic Computation, 187-194, 2012. Available as ZIB-Report 12-19, 2012
- Valid Linear Programming Bounds for Exact Mixed-Integer Programming Daniel E. Steffy and Kati Wolter. INFORMS Journal on Computing, 25(2):271-284, 2013. Available as ZIB-Report 11-08, 2011
- An Exact Rational Mixed-Integer Programming Solver William Cook, Thorsten Koch, Daniel E. Steffy, and Kati Wolter. IPCO 2011: The 15th Conference on Integer Programming and Combinatorial Optimization, LNCS 6655, 104-116, 2011. Available as ZIB-Report 11-07, 2011
- MIPLIB 2010 Thorsten Koch, Tobias Achterberg, Erling Andersen, Oliver Bastert, Timo Berthold, Robert E. Bixby, Emilie Danna, Gerald Gamrath, Ambros M. Gleixner, Stefan Heinz, Andrea Lodi, Hans Mittelmann, Ted Ralphs, Domenico Salvagnin, Daniel E. Steffy, and Kati Wolter. Mathematical Programming Computation, 3(2):103-163, 2011. Available as ZIB-Report 10-31, 2010
- William Cook: H. Milton Stewart School of Industrial and Systems Engineering, Georgia Institute of Technology in Atlanta, USA
- Daniel Espinoza: Departamento de Ingenieria Industrial, Universidad de Chile in Santiago, Chile
- Marc Pfetsch: Department of Mathematics, Technische Universität Darmstadt
- Daniel Steffy: Department of Mathematics and Statistics, Oakland University in Rochester, USA
07/2007 - 06/2013