caa a22 4500 463187210 CHVBK 20180406164857.0 cr unu---uuuuu 170326e20070401xx s 000 0 eng 10.1007/s10472-007-9062-5 doi (NATIONALLICENCE)springer-10.1007/s10472-007-9062-5 Exploiting multivalued knowledge in variable selection heuristics for SAT solvers [Elektronische Daten] [Carlos Ansótegui, Jose Larrubia, Chu-Min Li, Felip Manyà] 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. Springer Science+Business Media B.V., 2007 Satisfiability problems nationallicence Solvers nationallicence Heuristics nationallicence Ansótegui Carlos Department of Computer Science, Cornell University, 14853, Ithaca, NY, USA aut Larrubia Jose Department of Computer Science, Universitat de LLeida, Jaume II 69, 25001, LLeida, Spain aut Li Chu-Min LaRIA, Université de Picardie Jules Verne, 33 Rue Saint Leu, 80039, Amiens Cedex 01, France aut Manyà Felip Artificial Intelligence Research Institute (IIIA-CSIC), Campus UAB, 08193, Bellaterra, Spain aut Annals of Mathematics and Artificial Intelligence Springer Netherlands 49/1-4(2007-04-01), 191-205 1012-2443 49:1-4<191 2007 49 10472 https://doi.org/10.1007/s10472-007-9062-5 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10472-007-9062-5 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Ansótegui Carlos Department of Computer Science, Cornell University, 14853, Ithaca, NY, USA aut NATIONALLICENCE 700 1- Larrubia Jose Department of Computer Science, Universitat de LLeida, Jaume II 69, 25001, LLeida, Spain aut NATIONALLICENCE 700 1- Li Chu-Min LaRIA, Université de Picardie Jules Verne, 33 Rue Saint Leu, 80039, Amiens Cedex 01, France aut NATIONALLICENCE 700 1- Manyà Felip Artificial Intelligence Research Institute (IIIA-CSIC), Campus UAB, 08193, Bellaterra, Spain aut NATIONALLICENCE 773 0- Annals of Mathematics and Artificial Intelligence Springer Netherlands 49/1-4(2007-04-01), 191-205 1012-2443 49:1-4<191 2007 49 10472 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer