IntSat: integer linear programming by conflict-driven constraint learning

Abstract

State-of-the-art SAT solvers are nowadays able to handle huge real-world instances. The key to this success is the Conflict-Driven Clause-Learning (CDCL) scheme, which encompasses a number of techniques that exploit the conflicts that are encountered during the search for a solution. In this article, we extend these techniques to Integer Linear Programming (ILP), where variables may take general integer values instead of purely binary ones, constraints are more expressive than just propositional clauses, and there may be an objective function to optimize. We explain how these methods can be implemented efficiently and discuss possible improvements. Our work is backed with a basic implementation showing that, even in this far less mature stage, our techniques are already a useful complement to the state of the art in ILP.

Keywords:

• Integer linear programming
• SAT solving
• conflict-driven clause learning

Mathematics Subject Classification:

• 90C10

Disclosure statement

No potential conflict of interest was reported by the author(s).

Notes

1 We will be using the same acronym CDCL for both when there is no ambiguity.

2 The proofs of these lemmas as well as the rest of the theorems in this paper can be found as electronic supplementary material.

3 Due to space limitations, the names of some of the instances are only partially displayed.

4 Xpress and Gurobi were run with value 1 for the parameters HEUREMPHASIS and MIPFocus, respectively.

5 For the instances that according to MIPLIB are still open, we used the objective values of the best known solutions as a proxy.

Additional information

Funding

All authors are supported by grant PID2021-122830OB-C43, funded by MCIN/ AEI/10.13039/501100011033 and by ‘ERDF: A way of making Europe’ . We would like to thank Fair Isaac Corp. and Gurobi Optimization for their academic license programs that allowed free use of Xpress and Gurobi in this work, respectively.

Notes on contributors

Robert Nieuwenhuis

Robert Nieuwenhuis, B.S. and PhD. in Computer Science from the Technical University of Catalonia (UPC), Barcelona, Spain, in 1987 and 1990, is a professor of Computer Science at UPC since 2003. He is well known for his research at UPC and abroad (e.g., at the Max-Planck Institute), on automated reasoning, constraints, SAT, SMT, or ILP, with highly-cited publications and recognition as an invited speaker, program committee chair and editorial board membership in main conferences and journals. He is also known from the creation of the Barcelogic software tools for SAT and SMT, as well the company of the same name specialized in hard combinatorial optimization problems for scheduling and timetabling.

Albert Oliveras

Albert Oliveras received the B.S. degree in mathematics from the Technical University of Catalonia, Barcelona, Spain, in 2002 and the Ph.D. degree in computer science from the same institution in 2006. From 2006 to 2012, he was an Assistant Professor with the Department of Computer Science, Technical University of Catalonia, Barcelona, Spain. Since 2012, he has been an Associate Professor with the same institution. He is the author of more than 40 research papers, and the developer of several tools for SAT, SMT and ILP. His research interests include logics in computer, with special interest in SAT, SMT and variants of those problems.

Enric Rodríguez-Carbonell

Enric Rodríguez-Carbonell received the B.S. degree in Mathematics in 2002 and the Ph.D. degree in Computer Science in 2006 from the Technical University of Catalonia (UPC), Barcelona, Spain. Since 2012, he has been an Associate Professor with the Department of Computer Science of the Technical University of Catalonia. His main research interests are the applications of logics to Computer Science, in particular to program verification and analysis and to combinatorial problem solving.