|
Título:
|
Exploiting multivalued knowledge in variable selection heuristics for SAT solvers
|
|
Autor/a:
|
Ansótegui Gil, Carlos José; Larrubia, Jose; Li, Chu-Min; Manyà Serres, Felip
|
|
Notas:
|
We show that we can design and implement extremely efficient variable
selection heuristics for SAT solvers by identifying, in Boolean clause databases, sets
of Boolean variables that model the same multivalued variable and then exploiting
that structural information. In particular, we define novel variable selection heuristics
for two of the most competitive existing SAT solvers: Chaff, a solver based on
look-back techniques, and Satz, a solver based on look-ahead techniques. Our
heuristics give priority to Boolean variables that belong to sets of variables that
model multivalued variables with minimum domain size in a given state of the
search process. The empirical investigation conducted to evaluate the new heuristics
provides experimental evidence that identifying multivalued knowledge in Boolean
clause databases and using variable selection heuristics that exploit that knowledge
leads to large performance improvements.
This research was partially supported by projects TIN2004-07933-C03-03 and TIC2003-00950 funded by the Ministerio de Educación y Ciencia. The last author is supported by a grant Ramón y Cajal. |
|
Materia(s):
|
-Satisfiability problems
-Solvers
-Heuristics |
|
Derechos:
|
(c) Springer Science Business Media B.V., 2007
info:eu-repo/semantics/restrictedAccess |
|
Tipo de documento:
|
article
publishedVersion |
|
Editor:
|
Springer Verlag
|
|
Compartir:
|
|
