SCIP: solving constraint integer programs | Mathematical Programming Computation Skip to main content
Springer Nature Link
Log in

SCIP: solving constraint integer programs

  • Full length paper
  • Published:
Mathematical Programming Computation Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Achterberg T.: Conflict analysis in mixed integer programming. Discret. Optim. 4(1), 4–20 (2007) (special issue: Mixed Integer Programming)

    Article  MATH  MathSciNet  Google Scholar 

  2. Achterberg, T.: Constraint Integer Programming. Ph.D. Thesis, Technische Universität Berlin (2007). http://opus.kobv.de/tuberlin/volltexte/2007/1611/

  3. Achterberg T., Berthold T.: Improving the feasibility pump. Discret. Optim. 4(1), 77–86 (2007) (special issue: Mixed Integer Programming)

    Article  MATH  MathSciNet  Google Scholar 

  4. Achterberg, T., Berthold, T., Koch, T., Wolter, K.: Constraint integer programming: a new approach to integrate CP and MIP. In: Perron, L., Trick, M.A. (eds.) Integration of AI and OR techniques in constraint programming for combinatorial optimization problems, 5th international conference, CPAIOR 2008. Lecture Notes in Computer Science, vol. 5015, pp. 6–20. Springer, Heidelberg (2008)

  5. Achterberg, T., Brinkmann, R., Wedler, M.: Property checking with constraint integer programming. Technical Report 07-37, Zuse Institute Berlin (2007). http://opus.kobv.de/zib/volltexte/2007/1065/

  6. Achterberg T., Grötschel M., Koch T.: Teaching MIP modeling and solving. ORMS Today 33(6), 14–15 (2006)

    Google Scholar 

  7. Achterberg T., Koch T., Martin A.: Branching rules revisited. Oper. Res. Lett. 33, 42–54 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  8. Achterberg T., Koch T., Martin A.: MIPLIB 2003. Oper. Res. Lett. 34(4), 1–12 (2006)

    Article  MathSciNet  Google Scholar 

  9. Akers S.B.: Binary decision diagrams. IEEE Trans. Comput. C-27(6), 509–516 (1978)

    Article  Google Scholar 

  10. Althaus, E., Bockmayr, A., Elf, M., Jünger, M., Kasper, T., Mehlhorn, K.: SCIL—symbolic constraints in integer linear programming. Technical Report ALCOMFT-TR-02-133, MPI Saarbrücken, May (2002)

  11. Anders, C.: Das Chordalisierungspolytop und die Berechnung der Baumweite eines Graphen. Master’s Thesis, Technische Universität Berlin (2006)

  12. Andreello G., Caprara A., Fischetti M.: Embedding cuts in a branch&cut framework: a computational study with \({\{0,\frac{1}{2}\}}\) -cuts. INFORMS J. Comput. 19(2), 229–238 (2007)

    Article  MathSciNet  Google Scholar 

  13. Applegate D.L., Bixby R.E., Chvátal V., Cook W.J.: The Traveling Salesman Problem. Princeton University Press, Princeton (2006)

    MATH  Google Scholar 

  14. Armbruster, M.: Branch-and-Cut for a Semidefinite Relaxation of the Minimum Bisection Problem. Ph.D. Thesis, Technische Universität Chemnitz (2007)

  15. Armbruster, M., Fügenschuh, M., Helmberg, C., Martin, A.: Experiments with linear and semidefinite relaxations for solving the minimum graph bisection problem. Technical Report, Darmstadt University of Technology (2006)

  16. Armbruster, M., Fügenschuh, M., Helmberg, C., Martin, A.: On the bisection cut polytope. Darmstadt University of Technology (preprint, 2006)

  17. Aron, I.D., Hooker, J.N., Yunes, T.H.: SIMPL: a system for integrating optimization techniques. In: Régin, J.-C., Rueher, M. (eds.) Integration of AI and OR techniques in constraint programming for combinatorial optimization problems, first international conference, CPAIOR. Lecture Notes in Computer Science, vol. 3011, pp. 21–36. Springer, Nice, France (2004)

  18. Atamtürk A.: Flow pack facets of the single node fixed-charge flow polytope. Oper. Res. Lett. 29, 107–114 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  19. Atamtürk A.: On the facets of the mixed—integer knapsack polyhedron. Math. Programm. 98, 145–175 (2003)

    Article  MATH  Google Scholar 

  20. Atamtürk A., Rajan D.: On splittable and unsplittable capacitated network design arc-set polyhedra. Math. Programm. 92, 315–333 (2002)

    Article  MATH  Google Scholar 

  21. Balas E.: Facets of the knapsack polytope. Math. Programm. 8, 146–164 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  22. Balas E., Ceria S., Cornuéjols G., Natraj N.: Gomory cuts revisited. Oper. Res. h Lett. 19, 1–9 (1996)

    Article  MATH  Google Scholar 

  23. Balas E., Zemel E.: Facets of the knapsack polytope from minimal covers. SIAM J. Appl. Math. 34, 119–148 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  24. Beale E.M.L.: Branch and bound methods for mathematical programming systems. In: Hammer, P.L., Johnson, E.L., Korte, B.H.(eds) Discrete Optimization II, pp. 201–219. North Holland Publishing Co., Amsterdam (1979)

    Google Scholar 

  25. Bénichou M., Gauthier J.M., Girodet P., Hentges G., Ribière G., Vincent O.: Experiments in mixed-integer linear programming. Math. Programm. 1, 76–94 (1971)

    Article  MATH  Google Scholar 

  26. Berthold, T.: Primal heuristics for mixed integer programs. Master’s Thesis, Technische Universität Berlin

  27. Berthold, T., Heinz, S., Pfetsch, M.E.: Solving pseudo-Boolean problems with SCIP. Report 07–10, Zuse Institute Berlin (2008)

  28. Biere, A., Clarke, E.M., Raimi, R., Zhu, Y.: Verifying safety properties of a Power PC microprocessor using symbolic model checking without BDDs. In: Computer-aided verification. Lecture Notes in Computer Science, vol. 1633, pp. 60–71. Springer, Heidelberg (1999)

  29. Bilgen, E.: Personalkostenminimierung bei der Einsatzplanung von parallelen identischen Bearbeitungszentren in der Motorradproduktion. Master’s Thesis, Technische Universität Chemnitz (2007)

  30. Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an Alpha microprocessor using satisfiability solvers. In: Computer-aided verification. Lecture Notes in Computer Science, vol. 2102, pp. 454–464. Springer, Heidelberg (2001)

  31. Bley, A., Kupzog, F., Zymolka, A.: Auslegung heterogener Kommunikationsnetze nach performance und Wirtschaftlichkeit. In: Proceedings of 11th Kasseler Symposium Energie-Systemtechnik: Energie und Kommunikation, pp. 84–97, Kassel, November (2006)

  32. Bockmayr A., Kasper T.: Branch-and-infer: a unifying framework for integer and finite domain constraint programming. INFORMS J. Comput. 10(3), 287–300 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  33. Bockmayr, A., Pisaruk, N.: Solving assembly line balancing problems by combining IP and CP. In: Sixth Annual Workshop of the ERCIM Working Group on Constraints, June (2001)

  34. Brinkmann, R.: Preprocessing for Property Checking of Sequential Circuit on the Register Transfer Level. Ph.D. Thesis, University of Kaiserslautern, Kaiserslautern, Germany (2003)

  35. Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: Proceedings of the IEEE VLSI Design Conference, pp. 741–746 (2002)

  36. Bryant R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8), 677–691 (1986)

    Article  Google Scholar 

  37. Ceselli, A., Gatto, M., Lübbecke, M., Nunkesser, M., Schilling, H.: Optmizing the cargo express service of swiss federal railways. Transport. Sci. (to appear)

  38. COIN-OR. Computational Infrastructure for Operations Research. http://www.coin-or.org

  39. Crowder H., Johnson E.L., Padberg M.W.: Solving large scale zero-one linear programming problems. Oper. Res. 31, 803–834 (1983)

    Article  MATH  Google Scholar 

  40. Danna E., Rothberg E., Le Pape C.: Exploring relaxation induced neighborhoods to improve MIP solutions. Math. Programm. 102(1), 71–90 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  41. Dantzig, G.B.: Maximization of a linear function of variables subject to linear inequalities. In: Koopmans, T. (ed.) Activity Analysis of Production and Allocation, pp. 339–347. Wiley, New York (1951)

  42. Dantzig G.B.: Linear Programming and Extensions. Princeton University Press, Princeton (1963)

    MATH  Google Scholar 

  43. Dash Optimization. Xpress-MP. http://www.dashoptimization.com

  44. Dix, A.: Das Statische Linienplanungsproblem. Master’s Thesis, Technische Universität Berlin (2007)

  45. Dolan E., Moré J.: Benchmarking optimization software with performance profiles. Math. Programm. 91, 201–213 (2002)

    Article  MATH  Google Scholar 

  46. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Proceedings of SAT 2003, pp. 502–518. Springer, Heidelberg (2003)

  47. Fallah F., Devadas S., Keutzer K.: Functional vector generation for HDL models using linear programming and boolean satisfiability. IEEE Trans. CAD CAD-20(8), 994–1002 (2001)

    Google Scholar 

  48. Fischetti M., Lodi A.: Local branching. Math. Programm. 98(1–3), 23–47 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  49. Forrest, J.J.H.: COIN branch and cut. COIN-OR, http://www.coin-or.org

  50. Forrest, J.J.H., de la Nuez, D., Lougee-Heimer, R.: CLP user guide. COIN-OR,http://www.coin-or.org/Clp/userguide

  51. Fügenschuh, A., Martin, A.: Computational integer programming and cutting planes. In: Aardal, K., Nemhauser, G.L., Weismantel, R. (eds.) Discrete Optimization. Handbooks in Operations Research and Management Science, Chap. 2, vol. 12, pp. 69–122. Elsevier, Amsterdam (2005)

    Google Scholar 

  52. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Proceedings of the International Conference on Computer Aided Verification (CAV-04). pp. 26–37 (2004)

  53. Gauthier J.M., Ribière G.: Experiments in mixed-integer linear programming using pseudocosts. Math. Programm. 12(1), 26–47 (1977)

    Article  MATH  Google Scholar 

  54. Glover F., Laguna M.: Tabu Search. Kluwer, Boston (1997)

    MATH  Google Scholar 

  55. Gomory, R.E.: Solving linear programming problems in integers. In: Bellman, R., Hall, J.M. (eds.) Combinatorial Analysis Symposia in Applied Mathematics X, pp. 211–215. American Mathematical Society, Providence (1960)

  56. Gomory, R.E.: An algorithm for integer solutions to linear programming. In: Graves, R.L., Wolfe, P. (eds.) Recent Advances in Mathematical Programming, pp. 269–302. McGraw-Hill, New York (1963)

  57. Gottlieb, J., Paulmann, L.: Genetic algorithms for the fixed charge transportation problem. In: Proceedings of the 1998 IEEE International Conference on Evolutionary Computation, pp. 330–335. IEEE Press, New York (1998)

  58. Hooker J.N.: Planning and scheduling by logic-based Benders decomposition. Oper. Res. 55(3), 588–602 (2007)

    Article  MathSciNet  Google Scholar 

  59. ILOG. Cplex.http://www.ilog.com/products/cplex

  60. Jain V., Grossmann I.E.: Algorithms for hybrid MILP/CP models for a class of optimization problems. INFORMS J. Comput. 13(4), 258–276 (2001)

    Article  MathSciNet  Google Scholar 

  61. Jerraya, A.A., Wolf, W.: Multiprocessor Systems-on-Chips. The Morgan Kaufmann Series in Systems on Silicon. Elsevier/Morgan Kaufman, Boston/San Francisco (2004)

  62. Johnson E.L., Padberg M.W.: Degree-two inequalities, clique facets, and biperfect graphs. Ann. Discret. Math. 16, 169–187 (1982)

    MATH  MathSciNet  Google Scholar 

  63. Joswig M., Pfetsch M.E.: Computing optimal Morse matchings. SIAM J. Discret. Math. 20(1), 11–25 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  64. Kaibel, V., Peinhardt, M., Pfetsch, M.E.: Orbitopal fixing. In: Fischetti, M., Williamson, D. (eds.) Proceedings of the 12th Integer Programming and Combinatorial Optimization conference (IPCO). LNCS, vol. 4513, pp. 74–88. Springer, Heidelberg (2007)

  65. Koch, T.: Rapid mathematical programming or how to solve sudoku puzzles in a few seconds. In: Haasis, H.-D., Kopfer, H., Schönberger, J. (eds.) Operations Research Proceedings 2005, pp. 21–26 (2006)

  66. Kutschka, M.: Algorithmen zur Separierung von \({\{0,\frac{1}{2}\}}\) -Schnitten. Master’s Thesis, Technische Universität Berlin (2007)

  67. Land A., Powell S.: Computer codes for problems of integer programming. Ann. Discret. Math. 5, 221–269 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  68. Letchford A.N., Lodi A.: Strengthening Chvátal–Gomory cuts and Gomory fractional cuts. Oper. Res. Lett. 30(2), 74–82 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  69. Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of 15th International Joint Conference on Artificial Interlligence (IJCAI 1997), pp. 366–371. Morgan Kaufmann, Japan (1997)

  70. Li, C.M., Anbulagan: Look-ahead versus look-back for satisfiability problems. In: Proceedings of third international conference on Principles and Practice of Constraint Programming (CP 1997), pp. 342–356. Springer, Autriche (1997)

  71. Linderoth, J.T., Ralphs, T.K.: Noncommercial software for mixed-integer linear programming. In: Karlof, J. (ed.) Integer Programming: Theory and Practice, Operations Research Series, pp. 253–303. CRC Press, Boca Raton (2005)

  72. Linderoth J.T., Savelsbergh M.W.P.: A computational study of search strategies for mixed integer programming. INFORMS J. Comput. 11, 173–187 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  73. Madre, J.C., Billon, J.P.: Proving circuit correctness using formal comparison between expected and extracted behavior. In: Proceedings of the 25th Design Automation Conference, pp. 205–210 (1988)

  74. Manquinho, V., Roussel, O.: Pseudo Boolean evaluation (2007).http://www.cril.univ-artois.fr/PB07/

  75. Marchand, H.: A polyhedral study of the mixed knapsack set and its use to solve mixed integer programs. Ph.D. Thesis, Faculté des Sciences Appliquées, Université catholique de Louvain (1998)

  76. Marchand H., Wolsey L.A.: Aggregation and mixed integer rounding to solve MIPs. Oper. Res. 49(3), 363–371 (2001)

    Article  MathSciNet  Google Scholar 

  77. Markowitz H.M., Manne A.S.: On the solution of discrete programming problems. Econometrica 25, 84–110 (1957)

    Article  MATH  MathSciNet  Google Scholar 

  78. Marques-Silva J.P., Sakallah K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48, 506–521 (1999)

    Article  MathSciNet  Google Scholar 

  79. Martin, A.: Integer programs with block structure. Habilitations-Schrift, Technische Universität Berlin (1998).http://www.zib.de/Publications/abstracts/SC-99-03/

  80. Martin, A., Weismantel, R.: The intersection of knapsack polyhedra and extensions. In: Bixby, R.E., Boyd, E., Ríos-Mercado, R.Z. (eds.) Integer programming and combinatorial optimization. Proceedings of the 6th IPCO Conference, pp. 243–256 (1998).http://www.zib.de/Publications/abstracts/SC-97-61/

  81. Mitra G.: Investigations of some branch and bound strategies for the solution of mixed integer linear programs. Math. Programm. 4, 155–170 (1973)

    Article  MATH  Google Scholar 

  82. Mittelmann, H.: Decision tree for optimization software: Benchmarks for optimization software.http://plato.asu.edu/bench.html

  83. Mosek. Mosek Optimization tools.http://www.mosek.com

  84. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference, July (2001)

  85. Nemhauser G.L., Trick M.A.: Scheduling a major college basketball conference. Oper. Res. 46(1), 1–8 (1998)

    Article  Google Scholar 

  86. Nunkesser, M.: Algorithm design and analysis of problems in manufacturing, logistic, and telecommunications: An algorithmic jam session. Ph.D. Thesis, Eidgenössische Technische Hochschule ETH Zürich (2006)

  87. Orlowski, S., Koster, A.M.C.A., Raack, C., Wessäly, R.: Two-layer network design by branch- and-cut featuring MIP-based heuristics. In: Proceedings of the Third International Network Optimization Conference (INOC 2007). Spa, Belgium (2007)

  88. Padberg M.W., Roy T.J., Wolsey L.A.: Valid inequalities for fixed charge problems. Oper. Res. 33(4), 842–861 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  89. Parthasarathy, G., Iyer, M.K., Cheng, K.T., Wang, L.C.: An efficient finite-domain constraint solver for RTL circuits. In: Proceedings of the International Design Automation Conference (DAC-04) June (2004)

  90. Pfetsch, M.E.: Branch-and-cut for the maximum feasible subsystem problem. Report 05-46, ZIB (2005)

  91. Ryan, D.M., Foster, B.A.: An integer programming approach to scheduling. In: Wren, A. (ed.) Computer Scheduling of Public Transport Urban Passenger Vehicle and Crew Scheduling, pp. 269–280. North Holland, Amsterdam (1981)

  92. Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Master’s Thesis, Simon Fraser University

  93. Savelsbergh M.W.P.: Preprocessing and probing techniques for mixed integer programming problems. ORSA J. Comput. 6, 445–454 (1994)

    MATH  MathSciNet  Google Scholar 

  94. Thienel, S.: ABACUS—A Branch-and-Cut System. Ph.D. Thesis, Institut für Informatik, Universität zu Köln (1995)

  95. Timpe C.: Solving planning and scheduling problems with combined integer and constraint programming. OR Spectr. 24(4), 431–448 (2002)

    Article  MATH  Google Scholar 

  96. VALSE-XT: Eine integrierte Lösung für die SoC-Verifikation (2005).http://www.edacentrum.de/ekompass/projektflyer/pf-valse-xt.pdf

  97. Roy T.J., Wolsey L.A.: Valid inequalities for mixed 0-1 programs. Discret. Appl. Math. 14(2), 199–213 (1986)

    Article  MATH  Google Scholar 

  98. Wolsey L.A.: Valid inequalities for 0-1 knapsacks and MIPs with generalized upper bound constraints. Discret. Appl. Math. 29, 251–261 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  99. Wolter, K.: Implementation of cutting plane separators for mixed integer programs. Master’s Thesis, Technische Universität Berlin (2006)

  100. Wunderling, R.: Paralleler und objektorientierter Simplex-Algorithmus. Ph.D. Thesis, Technische Universität Berlin (1996).http://www.zib.de/Publications/abstracts/TR-96-09/

  101. Zeng, Z., Kalla, P., Ciesielski, M.: LPSAT: a unified approach to RTL satisfiability. In: Proceedings of Conference on Design, Automation and Test in Europe (DATE-01) Munich, March (2001)

  102. Zuse Institute Berlin. SCIP: solving constraint integer programs.http://scip.zib.de

Download references

Author information

Authors and Affiliations

  1. Zuse Institute Berlin, Berlin, Germany

    Tobias Achterberg

Authors
  1. Tobias Achterberg
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tobias Achterberg.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Achterberg, T. SCIP: solving constraint integer programs. Math. Prog. Comp. 1, 1–41 (2009). https://doi.org/10.1007/s12532-008-0001-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s12532-008-0001-1

Keywords

Mathematics Subject Classification (2000)

Search

Navigation