Improving Performance of CDCL SAT Solvers by Automated Design of Variable Selection Heuristics
Abstract
Many real-world engineering and science problems can be mapped to Boolean satisfiability problems (SAT). CDCL SAT solvers are among the most efficient solvers. Previous work showed that instances derived from a particular problem class exhibit a unique underlying structure which impacts the effectiveness of a solver's variable selection scheme. Thus, customizing the variable scoring heuristic of a solver to a particular problem class can significantly enhance the solver's performance; however, manually performing such customization is very labor intensive. This paper presents a system for automating the design of variable scoring heuristics for CDCL solvers, making it feasible to tailor solvers to arbitrary problem classes. Experimental results are provided demonstrating that this system, which evolves variable scoring heuristics using an asynchronous parallel hyper-heuristics approach employing genetic programming, has the potential to create more efficient solvers for particular problem classes.
Recommended Citation
M. Illetskova and A. R. Bertels and J. M. Tuggle and A. Harter and S. Richter and D. R. Tauritz and S. Mulder and D. Bueno and M. Leger and W. M. Siever, "Improving Performance of CDCL SAT Solvers by Automated Design of Variable Selection Heuristics," Proceedings of the 2017 IEEE Symposium Series on Computational Intelligence (2017, Honolulu, HI), pp. 1 - 8, Institute of Electrical and Electronics Engineers (IEEE), Dec 2017.
The definitive version is available at https://doi.org/10.1109/SSCI.2017.8280953
Meeting Name
2017 IEEE Symposium Series on Computational Intelligence, SSCI 2017 (2017: Nov. 27-Dec. 1, Honolulu, HI)
Department(s)
Computer Science
Research Center/Lab(s)
Intelligent Systems Center
Keywords and Phrases
Artificial intelligence; Genetic algorithms; Genetic programming, Arbitrary problems; Asynchronous parallel; Automated design; Boolean satisfiability problems; Efficient solvers; Hyper-heuristics; Improving performance; Variable selection, Model checking
International Standard Book Number (ISBN)
978-153862725-9
Document Type
Article - Conference proceedings
Document Version
Citation
File Type
text
Language(s)
English
Rights
© 2017 Institute of Electrical and Electronics Engineers (IEEE), All rights reserved.
Publication Date
01 Dec 2017
