## Conflict Analysis in Mixed Integer Programming

Please always quote using this URN: urn:nbn:de:0297-zib-8537

- Conflict analysis for infeasible subproblems is one of the key ingredients in modern SAT solvers to cope with large real-world instances. In contrast, it is common practice for today's mixed integer programming solvers to just discard infeasible subproblems and the information they reveal. In this paper we try to remedy this situation by generalizing the 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 15\%. 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\%.

Author: | Tobias Achterberg |
---|---|

Document Type: | ZIB-Report |

Tag: | SAT; branch and cut ; conflict analysis ; mixed integer programming |

MSC-Classification: | 90-XX OPERATIONS RESEARCH, MATHEMATICAL PROGRAMMING / 90-08 Computational methods |

90-XX OPERATIONS RESEARCH, MATHEMATICAL PROGRAMMING / 90Cxx Mathematical programming [See also 49Mxx, 65Kxx] / 90C11 Mixed integer programming | |

CCS-Classification: | G. Mathematics of Computing / G.4 MATHEMATICAL SOFTWARE |

I. Computing Methodologies / I.2 ARTIFICIAL INTELLIGENCE / I.2.3 Deduction and Theorem Proving (F.4.1) | |

I. Computing Methodologies / I.2 ARTIFICIAL INTELLIGENCE / I.2.8 Problem Solving, Control Methods, and Search (F.2.2) | |

Date of first Publication: | 2005/03/22 |

Series (Serial Number): | ZIB-Report (05-19) |

Published in: | Appeared in: Discrete Optimization 4 (2007) 4-20 |