Skip to main content
Article
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)
  • Marketa Illetskova
  • Alex R. Bertels
  • Joshua M. Tuggle
  • Adam Harter
  • Samuel Richter
  • Daniel R. Tauritz, Missouri University of Science and Technology
  • Samuel Mulder
  • Denis Bueno
  • Michelle Leger
  • William M. Siever
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.

Meeting Name
2017 IEEE Symposium Series on Computational Intelligence, SSCI 2017 (2017: Nov. 27-Dec. 1, Honolulu, HI)
Department(s)
Computer Science
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
12-1-2017
Disciplines
Citation Information
Marketa Illetskova, Alex R. Bertels, Joshua M. Tuggle, Adam Harter, et al.. "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) (2017) p. 1 - 8
Available at: http://works.bepress.com/daniel-tauritz/68/