Conflict analysis in mixed integer programming
In this talk 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 cuts. We performed computational experiments which show the potential of our method: On feasible MIP instances, the number of required branching nodes was reduced by 50% in the geometric mean. However, the total solving time increased by 20%. On infeasible MIPs arising in the context of chip verification, the number of nodes was reduced by 90%,thereby reducing the solving time by 60%.