Improving Performance of CDCL SAT Solvers by Automated Design of Variable Selection Heuristics


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)


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)


Document Type

Article - Conference proceedings

Document Version


File Type





© 2017 Institute of Electrical and Electronics Engineers (IEEE), All rights reserved.

Publication Date

01 Dec 2017