Effective Heuristics Learning via Program Synthesis
Heuristic algorithms are largely used in solving NP-hard problems due to their fundamental intractability. In this work, we introduce a program synthesis method for generating new heuristics, in particular, variable scoring heuristics for Conflict-Driven Clause Learning (CDCL) SAT solvers. A genetic programming approach is leveraged to search through the space of heuristics defined with an expressive Domain Specific Language (DSL). We develop a pipeline transforming a DSL program into a piece of C++ program embedded within CaDiCaL, a state-of-the-art SAT solver. This pipeline automates the procedure of designing and evaluating heuristics and evolving from existing results. Our evaluation on the SAT Competition 2018 benchmark indicates that the synthesized heuristics are comparable to the manually designed state-of-the-art heuristics.