Learning a SAT Solver from Single-Bit Supervision
This work addresses the challenge of learning SAT solvers with minimal supervision, though it is incremental as it is not competitive with state-of-the-art solvers.
The authors tackled the problem of solving SAT problems using a neural network trained only to predict satisfiability, resulting in NeuroSAT, which can solve larger and more difficult problems than seen during training and generalizes to novel distributions like graph coloring and clique detection.
We present NeuroSAT, a message passing neural network that learns to solve SAT problems after only being trained as a classifier to predict satisfiability. Although it is not competitive with state-of-the-art SAT solvers, NeuroSAT can solve problems that are substantially larger and more difficult than it ever saw during training by simply running for more iterations. Moreover, NeuroSAT generalizes to novel distributions; after training only on random SAT problems, at test time it can solve SAT problems encoding graph coloring, clique detection, dominating set, and vertex cover problems, all on a range of distributions over small random graphs.