SCIP: solving constraint integer programs. (English) Zbl 1171.90476

Achterberg, Tobias

Math. Program. Comput. 1, No. 1, 1-41 (2009).

Summary: 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.

MSC:

90C11	Mixed integer programming
68T20	Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
90C27	Combinatorial optimization
90-04	Software, source code, etc. for problems pertaining to operations research and mathematical programming
90-08	Computational methods for problems pertaining to operations research and mathematical programming

Keywords:

constraint programming; integer programming; SAT

Software:

MiniSat; Mosek; COIN-OR; Chaff; Siege; CLP; XPRESS; CPLEX; SIMPL; MIPLIB2003; Valse-XT; Decision tree for optimization software; Tabu search; FEASPUMP; SCIL; MIPLIB; Zimpl; SoPlex; SCIP; ABACUS; Benchmarks for Optimization Software

References:

[1]	Achterberg T.: Conflict analysis in mixed integer programming. Discret. Optim. 4(1), 4–20 (2007) (special issue: Mixed Integer Programming) · Zbl 1169.90414
[2]	Achterberg, T.: Constraint Integer Programming. Ph.D. Thesis, Technische Universität Berlin (2007). http://opus.kobv.de/tuberlin/volltexte/2007/1611/ · Zbl 1171.90476
[3]	Achterberg T., Berthold T.: Improving the feasibility pump. Discret. Optim. 4(1), 77–86 (2007) (special issue: Mixed Integer Programming) · Zbl 1170.90443
[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) · Zbl 1142.68504
[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)
[7]	Achterberg T., Koch T., Martin A.: Branching rules revisited. Oper. Res. Lett. 33, 42–54 (2005) · Zbl 1076.90037
[8]	Achterberg T., Koch T., Martin A.: MIPLIB 2003. Oper. Res. Lett. 34(4), 1–12 (2006) · Zbl 1133.90300
[9]	Akers S.B.: Binary decision diagrams. IEEE Trans. Comput. C-27(6), 509–516 (1978) · Zbl 0377.94038
[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) · Zbl 1019.90515
[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) · Zbl 1241.90181
[13]	Applegate D.L., Bixby R.E., Chvátal V., Cook W.J.: The Traveling Salesman Problem. Princeton University Press, Princeton (2006) · Zbl 1130.90036
[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) · Zbl 1143.90397
[16]	Armbruster, M., Fügenschuh, M., Helmberg, C., Martin, A.: On the bisection cut polytope. Darmstadt University of Technology (preprint, 2006) · Zbl 1194.90120
[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) · Zbl 1094.68636
[18]	Atamtürk A.: Flow pack facets of the single node fixed-charge flow polytope. Oper. Res. Lett. 29, 107–114 (2001) · Zbl 1018.90060
[19]	Atamtürk A.: On the facets of the mixed–integer knapsack polyhedron. Math. Programm. 98, 145–175 (2003) · Zbl 1082.90073
[20]	Atamtürk A., Rajan D.: On splittable and unsplittable capacitated network design arc-set polyhedra. Math. Programm. 92, 315–333 (2002) · Zbl 1094.90005
[21]	Balas E.: Facets of the knapsack polytope. Math. Programm. 8, 146–164 (1975) · Zbl 0316.90046
[22]	Balas E., Ceria S., Cornuéjols G., Natraj N.: Gomory cuts revisited. Oper. Res. h Lett. 19, 1–9 (1996) · Zbl 0865.90098
[23]	Balas E., Zemel E.: Facets of the knapsack polytope from minimal covers. SIAM J. Appl. Math. 34, 119–148 (1978) · Zbl 0385.90083
[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) · Zbl 0405.90049
[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) · Zbl 0233.90016
[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) · Zbl 1046.68578
[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) · Zbl 0996.68578
[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) · Zbl 1034.90517
[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) · Zbl 0593.94022
[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) · Zbl 0576.90065
[40]	Danna E., Rothberg E., Le Pape C.: Exploring relaxation induced neighborhoods to improve MIP solutions. Math. Programm. 102(1), 71–90 (2005) · Zbl 1131.90036
[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) · Zbl 0108.33103
[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) · Zbl 1049.90004
[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) · Zbl 1204.68191
[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)
[48]	Fischetti M., Lodi A.: Local branching. Math. Programm. 98(1–3), 23–47 (2003) · Zbl 1060.90056
[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)
[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) · Zbl 1103.68616
[53]	Gauthier J.M., Ribière G.: Experiments in mixed-integer linear programming using pseudocosts. Math. Programm. 12(1), 26–47 (1977) · Zbl 0362.90070
[54]	Glover F., Laguna M.: Tabu Search. Kluwer, Boston (1997) · Zbl 0930.90083
[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) · Zbl 0096.14505
[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) · Zbl 0235.90038
[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) · Zbl 1167.90512
[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) · Zbl 1238.90106
[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) · Zbl 0523.52009
[63]	Joswig M., Pfetsch M.E.: Computing optimal Morse matchings. SIAM J. Discret. Math. 20(1), 11–25 (2006) · Zbl 1190.90162
[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) · Zbl 1136.90407
[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) · Zbl 0428.90048
[68]	Letchford A.N., Lodi A.: Strengthening Chvátal–Gomory cuts and Gomory fractional cuts. Oper. Res. Lett. 30(2), 74–82 (2002) · Zbl 1027.90062
[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) · Zbl 1137.90622
[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) · Zbl 1040.90535
[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/ · Zbl 1116.68088
[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) · Zbl 1163.90671
[77]	Markowitz H.M., Manne A.S.: On the solution of discrete programming problems. Econometrica 25, 84–110 (1957) · Zbl 0078.34005
[78]	Marques-Silva J.P., Sakallah K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48, 506–521 (1999) · Zbl 01935259
[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) · Zbl 0258.90034
[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)
[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) · Zbl 0579.90072
[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) · Zbl 1167.90018
[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) · Zbl 0814.90093
[94]	Thienel, S.: ABACUS–A Branch-and-Cut System. Ph.D. Thesis, Institut für Informatik, Universität zu Köln (1995) · Zbl 0911.90282
[95]	Timpe C.: Solving planning and scheduling problems with combined integer and constraint programming. OR Spectr. 24(4), 431–448 (2002) · Zbl 1028.90017
[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) · Zbl 0593.90058
[98]	Wolsey L.A.: Valid inequalities for 0-1 knapsacks and MIPs with generalized upper bound constraints. Discret. Appl. Math. 29, 251–261 (1990) · Zbl 0718.90067
[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/ · Zbl 0871.65048
[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