- author = "Marketa Illetskova and Alex R. Bertels and Joshua M. Tuggle and Adam Harter and Samuel Richter and Daniel R. Tauritz and Samuel Mulder and Denis Bueno and Michelle Leger and William M. Siever",
- booktitle = "2017 IEEE Symposium Series on Computational Intelligence (SSCI)",
- title = "Improving performance of {CDCL SAT} solvers by automated design of variable selection heuristics",
- year = "2017",
- address = "Honolulu, Hawaii, U.S.A.",
- month = nov # " 27-" # dec # " 1",
- keywords = "genetic algorithms, genetic programming, Hyper-heuristics, ADSSEC",
-
DOI = "
doi:10.1109/SSCI.2017.8280953",
- size = "8 pages",
- 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 labour 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.",
-
notes = "ibm-18 cactus plot. MiniSat for the unif-k5.
Also known as \cite{8280953}",
