Exploiting multivalued knowledge in variable selection heuristics for SAT solvers
MetadataShow full item record
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.