Learning a SAT Solver from Single-Bit Supervision

TL;DR

NeuroSAT is a neural network that learns to classify SAT problems and can generalize to larger, more complex problems and different problem types beyond its training distribution, demonstrating flexible problem-solving capabilities.

Contribution

This work introduces NeuroSAT, a neural network that learns to solve SAT problems from single-bit supervision and generalizes to larger and different problem distributions.

Findings

NeuroSAT can solve larger and more complex SAT problems with more iterations.

It generalizes to different problem types like graph coloring and clique detection.

It performs well on various distributions of small random graphs.

Abstract

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.