Constraint Integer Programming

This work introduces the novel paradigm of constraint integer programming (CIP), which integrates constraint programming (CP) and mixed integer programming (MIP) modeling and solving techniques. It is supplemented by the software SCIP, which is a solver and framework for constraint integer programming that also features SAT solving techniques. SCIP is freely available in source code for academic and non-commercial purposes. Introduction......Page 15 I Concepts......Page 21 1.1 Constraint Programs......Page 23 1.2 Satisfiability Problems......Page 24 1.3 Mixed Integer Programs......Page 25 1.4 Constraint Integer Programs......Page 27 2.1 Branch and Bound......Page 29 2.2 Cutting Planes......Page 32 2.3 Domain Propagation......Page 33 3.1 Basic Concepts of SCIP......Page 37 3.2 Algorithmic Design......Page 43 3.3 Infrastructure......Page 51 II Mixed Integer Programming......Page 71 4 Introduction......Page 73 5 Branching......Page 75 5.2 Least Infeasible Branching......Page 76 5.4 Strong Branching......Page 77 5.5 Hybrid Strong/Pseudocost Branching......Page 78 5.7 Reliability Branching......Page 79 5.8 Inference Branching......Page 80 5.9 Hybrid Reliability/Inference Branching......Page 81 5.10 Branching Rule Classification......Page 82 5.11 Computational Results......Page 83 6.1 Depth First Search......Page 87 6.2 Best First Search......Page 88 6.3 Best First Search with Plunging......Page 89 6.4 Best Estimate Search......Page 90 6.6 Interleaved Best Estimate/Best First Search......Page 91 6.8 Computational Results......Page 92 7.1 Linear Constraints......Page 97 7.2 Knapsack Constraints......Page 103 7.3 Set Partitioning and Set Packing Constraints......Page 105 7.4 Set Covering Constraints......Page 107 7.5 Variable Bound Constraints......Page 109 7.6 Objective Propagation......Page 110 7.7 Root Reduced Cost Strengthening......Page 112 7.8 Computational Results......Page 113 8.1 Knapsack Cover Cuts......Page 115 8.2 Mixed Integer Rounding Cuts......Page 118 8.3 Gomory Mixed Integer Cuts......Page 119 8.4 Strong Chvátal-Gomory Cuts......Page 121 8.5 Flow Cover Cuts......Page 122 8.7 Clique Cuts......Page 123 8.8 Reduced Cost Strengthening......Page 124 8.10 Computational Results......Page 125 9 Primal Heuristics......Page 131 9.1 Rounding Heuristics......Page 132 9.2 Diving Heuristics......Page 134 9.3 Objective Diving Heuristics......Page 137 9.4 Improvement Heuristics......Page 139 9.5 Computational Results......Page 141 10.1 Linear Constraints......Page 147 10.2 Knapsack Constraints......Page 160 10.3 Set Partitioning, Set Packing, and Set Covering Constraints......Page 165 10.4 Variable Bound Constraints......Page 167 10.6 Probing......Page 168 10.7 Implication Graph Analysis......Page 171 10.8 Dual Fixing......Page 172 10.9 Restarts......Page 174 10.10 Computational Results......Page 175 11 Conflict Analysis......Page 179 11.1 Conflict Analysis in SAT Solving......Page 180 11.2 Conflict Analysis in MIP......Page 184 11.3 Computational Results......Page 192 III Chip Design Verification......Page 197 12 Introduction......Page 199 13.1 Constraint Integer Programming Model......Page 203 13.2 Function Graph......Page 206 14 Operators in Detail......Page 209 14.1 Bit and Word Partitioning......Page 210 14.3 Addition......Page 218 14.4 Subtraction......Page 224 14.5 Multiplication......Page 225 14.7 Bitwise And......Page 242 14.9 Bitwise Xor......Page 245 14.10 Unary And......Page 248 14.12 Unary Xor......Page 251 14.13 Equality......Page 255 14.14 Less-Than......Page 260 14.15 If-Then-Else......Page 265 14.16 Zero Extension......Page 270 14.19 Shift Left......Page 271 14.21 Slicing......Page 278 14.22 Multiplex Read......Page 281 14.23 Multiplex Write......Page 286 15.1 Term Algebra Preprocessing......Page 293 15.2 Irrelevance Detection......Page 304 16.1 Branching......Page 309 16.2 Node Selection......Page 310 17.1 Comparison of CIP and SAT......Page 313 17.2 Problem Specific Presolving......Page 322 17.3 Probing......Page 325 17.4 Conflict Analysis......Page 330 A.1 Computational Infrastructure......Page 333 A.2 Mixed Integer Programming Test Set......Page 334 A.3 Computing Averages......Page 335 A.4 Chip Design Verification Test Set......Page 336 B Tables......Page 339 C SCIP versus Cplex......Page 391 D Notation......Page 399 Bibliography......Page 405