Conflict analysis in mixed integer programming

Conflict analysis for infeasible subproblems is one of the key ingredients in modern SAT solvers. III contrast, it is common practice for today's mixed integer programming solvers to discard infeasible subproblems and the information they reveal. III this paper, we try to remedy this situation by generalizing SAT infeasibility analysis to mixed integer programming. We present heuristics for branch-and-cut solvers to generate valid inequalities from the Current infeasible subproblem and the associated branching information. SAT techniques can then be used to strengthen the resulting constraints. Extensive Computational experiments show the potential Of Our method. Conflict analysis greatly improves the performance oil particular models, while it does not interfere with the solving process on the other instances. In total, the number of required branching nodes oil general MIP instances was reduced by 18% in the geometric mean, and the solving time was reduced by 11%. On infeasible MIP arising in the context of chip verification and on a model for a particular combinatorial game, the number of nodes was reduced by 80%, thereby reducing the solving time by 50%. (c) 2006 Elsevier B.V. All rights reserved.