Automated Discovery of Composite SAT Variable-Selection Heuristics

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 18

Satisfiability

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.