|
Title:
|
Improving IntSat by expressing disjunctions of bounds as linear constraints
|
|
Author:
|
Asín Acha, Roberto Javier; Aloysius Bezem, Marcus; Nieuwenhuis, Robert Lukas Mario
|
|
Other authors:
|
Universitat Politècnica de Catalunya. Departament de Ciències de la Computació; Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació |
|
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. |
|
Abstract:
|
Peer Reviewed |
|
Subject(s):
|
-Àrees temàtiques de la UPC::Informàtica::Intel·ligència artificial
-Constraint programming (Computer science)
-SAT
-conflict-driven clause learning
-constraint programming
-integer linear programming
-Programació per restriccions (Informàtica) |
|
Rights:
|
|
|
Document type:
|
Article - Published version
Article |
|
Share:
|
|
