Automated Discovery of Composite SAT Variable-Selection Heuristics

Variants of GSAT and Walksat are among the most successful 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 primitives. We describe CLASS, an automated heuristic discovery system which generates new, effective variable selection heuristic functions using a simple composition operator. New heuristics discovered by CLASS are shown to be competitive 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.

Authors

• Alex Fukunaga The University of Tokyo

Keywords

No keywords are indexed for this paper.