|
Título:
|
Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-boolean constraints
|
|
Autor/a:
|
Ansótegui Gil, Carlos; Bofill Arasa, Miquel; Coll Caballero, Jordi; Dang, Nguyen; Esteban Ángeles, Juan Luis; Miguel, Ian; Nightingale, Peter; Salamon, András Z.; Suy Franch, Josep; Villaret Auselle, Mateu
|
|
Otros autores:
|
Universitat Politècnica de Catalunya. Departament de Ciències de la Computació |
|
Abstract:
|
Pseudo-Boolean (PB) constraints often have a critical role in constraint satisfaction and optimisation problems. Encoding PB constraints to SAT has proven to be an efficient approach in many applications, however care must be taken to encode them compactly and with good propagation properties. It has been shown that at-most-one (AMO) and exactly-one (EO) relations over subsets of the variables can be exploited in various encodings of PB constraints, improving their compactness and solving performance. In this paper we detect AMO and EO relations completely automatically and exploit them to improve SAT encodings that are based on Multi-Valued Decision Diagrams (MDDs). Our experiments show substantial reductions in encoding size and dramatic improvements in solving time thanks to automatic AMO and EO detection. |
|
Abstract:
|
Peer Reviewed |
|
Materia(s):
|
-Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica
-Constraint programming (Computer science)
-Computer algorithms
-Algebra, Boolean
-Automatic CSP reformulation
-SAT
-Pseudo-Boolean
-Atmost-one constraint
-Programació per restriccions (Informàtica)
-Algorismes computacionals
-Àlgebra booleana |
|
Derechos:
|
|
|
Tipo de documento:
|
Artículo - Versión presentada
Objeto de conferencia |
|
Editor:
|
Springer
|
|
Compartir:
|
|
