ZIB-Logo
KONRAD-ZUSE-ZENTRUM
FÜR INFORMATIONSTECHNIK
BERLIN
Home english » Research » Discrete Methods » Optimization » Linear and Nonlinear Integer Optimization

ExactIP - Exact Integer Programming

Project Description

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.


Problem Description


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.


Industrial Application


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.


Goal


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.


Publikationen

Organizational Details

Duration

07/2007 - 06/2013