SCIP: solving constraint integer programs |
| |
Authors: | Tobias Achterberg |
| |
Institution: | (1) Zuse Institute Berlin, Berlin, Germany |
| |
Abstract: | Constraint integer programming (CIP) is a novel paradigm which integrates constraint programming (CP), mixed integer programming (MIP), and satisfiability (SAT) modeling and solving techniques. In this paper we discuss the software framework and solver SCIP (Solving Constraint
Integer Programs), which is free for academic and non-commercial use and can be downloaded in source code. This paper gives
an overview of the main design concepts of SCIP and how it can be used to solve constraint integer programs. To illustrate
the performance and flexibility of SCIP, we apply it to two different problem classes. First, we consider mixed integer programming
and show by computational experiments that SCIP is almost competitive to specialized commercial MIP solvers, even though SCIP
supports the more general constraint integer programming paradigm. We develop new ingredients that improve current MIP solving
technology. As a second application, we employ SCIP to solve chip design verification problems as they arise in the logic
design of integrated circuits. This application goes far beyond traditional MIP solving, as it includes several highly non-linear
constraints, which can be handled nicely within the constraint integer programming framework. We show anecdotally how the
different solving techniques from MIP, CP, and SAT work together inside SCIP to deal with such constraint classes. Finally,
experimental results show that our approach outperforms current state-of-the-art techniques for proving the validity of properties
on circuits containing arithmetic.
|
| |
Keywords: | Constraint programming Integer programming SAT |
本文献已被 SpringerLink 等数据库收录! |
|