Improving IntSat by expressing disjunctions of bounds as linear constraints

Article type: Research Article

Authors: Asín, Roberto^a | Bezem, Marc^b | Nieuwenhuis, Robert^{c; *}

Affiliations: [a] Universidad Católica de la Santísima Concepción, Concepción, Chile | [b] Department of Informatics, University of Bergen, Bergen, Norway | [c] Technical University of Catalonia, Barcelona, Spain

Correspondence: [*] Corresponding author. E-mail: roberto@cs.upc.edu.

Abstract: 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.

Keywords: SAT, conflict-driven clause learning, constraint programming, integer linear programming

DOI: 10.3233/AIC-150684

Journal: AI Communications, vol. 29, no. 1, pp. 205-209, 2016