Automated Discovery of Composite SAT Variable-Selection Heuristics
Alex S. Fukunaga · 2002
Variants of GSAT and Walksat are among the most suc-cessful SAT local search algorithms. We show that several well-known SAT local search algorithms are the result of novel combininations of a set of variable selection primi-tives. We describe CLASS, an automated heuristic discov-ery system which generates new, effective variable selection heuristic functions using a simple composition operator. New heuristics discovered by CLASS are shown to be competi-tive with the best Walksat variants, including Novelty+ and R-Novelty+. We also analyze the local search behavior of the learned heuristics using the depth, mobility, and coverage metrics recently proposed by Schuurmans and Southey. 1