Learning Interpretable Heuristics for WalkSAT
This work addresses the challenge of tuning heuristics for SAT solvers, which is incremental as it builds on existing methods to enhance performance for specific distributions.
The paper tackled the problem of optimizing heuristics for WalkSAT, a local search algorithm for SAT, by using reinforcement learning to learn specialized variable scoring functions and noise parameters for different instance distributions, resulting in improvements over both a WalkSAT baseline and another learned heuristic.
Local search algorithms are well-known methods for solving large, hard instances of the satisfiability problem (SAT). The performance of these algorithms crucially depends on heuristics for setting noise parameters and scoring variables. The optimal setting for these heuristics varies for different instance distributions. In this paper, we present an approach for learning effective variable scoring functions and noise parameters by using reinforcement learning. We consider satisfiability problems from different instance distributions and learn specialized heuristics for each of them. Our experimental results show improvements with respect to both a WalkSAT baseline and another local search learned heuristic.