首页    期刊浏览 2024年11月30日 星期六
登录注册

文章基本信息

  • 标题:SCIP: Solving constraint integer programs
  • 其他标题:SCIP: Solving constraint integer programs
  • 本地全文:下载
  • 作者:Achterberg, Tobias
  • 期刊名称:Mathematical Programming Computation
  • 印刷版ISSN:1867-2957
  • 出版年度:2009
  • 期号:1
  • 页码:1-41
  • DOI:10.1007/mpc.v0i1.4
  • 语种:English
  • 出版社:Mathematical Programming Computation
  • 摘要: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.
国家哲学社会科学文献中心版权所有