Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs

TL;DR

This paper presents a reinforcement learning approach using GNNs to guide SAT solver heuristics, significantly improving solving speed and generalization over traditional methods.

Contribution

Introduces RLAF, a novel framework for training GNN-guided heuristics in SAT solvers using reinforcement learning and a generic variable weighting mechanism.

Findings

Achieves over 2x speedup in SAT solving times.

Generalizes well to larger, more complex problems.

Outperforms supervised heuristic learning methods.

Abstract

Boolean Satisfiability (SAT) solvers are foundational to computer science, yet their performance typically hinges on hand-crafted heuristics. This work introduces Reinforcement Learning from Algorithm Feedback (RLAF) as a paradigm for learning to guide SAT solver branching heuristics with Graph Neural Networks (GNNs). Central to our approach is a novel and generic mechanism for injecting inferred variable weights and polarities into the branching heuristics of existing SAT solvers. In a single forward pass, a GNN assigns these parameters to all variables. Casting this one-shot guidance as a reinforcement learning problem lets us train the GNN with off-the-shelf policy-gradient methods, such as GRPO, directly using the solver's computational cost as the sole reward signal. Extensive evaluations demonstrate that RLAF-trained policies significantly reduce the mean solve times of different base solvers across diverse SAT problem distributions, achieving more than a 2x speedup in some cases, while generalizing effectively to larger and harder problems after training. Notably, these policies consistently outperform expert-supervised approaches based on learning handcrafted weighting heuristics, offering a promising path towards data-driven heuristic design in combinatorial optimization.