Improving IntSat by expressing disjunctions of bounds as linear constraints

Conflict-Driven Clause Learning (CDCL) SAT solvers can automatically solve very large real-world problems. IntSat is a new technique extending CDCL to Integer Linear Programming (ILP). For some conflicts, IntSat generates no strong enough ILP constraint, and the backjump has to be done based on the conflicting set of bounds. The techniques given in this article precisely analyze how and when that set can be translated into the required new ILP constraint. Moreover, this can be done efficiently. This obviously strengthens learning and significantly improves the performance of IntSat (as confirmed by our experiments). We also briefly discuss extensions and other applications.Peer ReviewedPostprint (published version