PaperlayerView exact revision on arXiv

Source-linked AI summary

Learning a SAT Solver from Single-Bit Supervision

Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill

arXiv:1802.03685v4cs.AIcs.LGcs.LO

TL;DR

The paper asks whether a neural network can learn to solve SAT rather than merely classify it. NeuroSAT uses message passing over a structured SAT graph and receives only satisfiability labels during training. It can solve harder and larger problems with more iterations and generalizes from random SAT instances to several new encoded domains, while remaining less reliable than state-of-the-art solvers.

  • Problem

    The paper investigates whether neural networks can learn discrete SAT search from minimal supervision while respecting the structural invariances of propositional logic.

  • Method

    NeuroSAT is a message-passing neural network trained as a satisfiability classifier on random SAT problems using only one bit of supervision per problem.

  • Results

    NeuroSAT solves substantially larger and harder problems with more iterations and generalizes from random SAT training to graph coloring, clique detection, dominating set, and vertex cover encodings.

  • Takeaways & Limitations

    The results establish that neural networks can learn discrete search without hard-coded search procedures, even with end-to-end minimal supervision.

  • Takeaways & Limitations

    As an end-to-end SAT solver, NeuroSAT remains vastly less reliable than state-of-the-art solvers, and the authors see no obvious path to beating them.

Abstract

from arXiv · show

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.

1 INTRODUCTION

NeuroSAT is trained with only satisfiability labels yet can extract satisfying assignments and solve larger, harder, and cross-domain SAT problems. A related model can identify variables in small unsatisfiable cores to support more efficient resolution-proof construction.

  • 1 INTRODUCTION: NeuroSAT learns to solve SAT by training only as a satisfiability classifier with one-bit supervision per problem.When it predicts satisfiable, a satisfying assignment can almost always be decoded from its activations.
  • 1 INTRODUCTION: It can solve substantially larger and more difficult problems than those seen during training by running additional message-passing iterations.The model continues finding solutions after hundreds or thousands of iterations, despite training for only a few dozen.
  • 1 INTRODUCTION: After training on random SAT problems, NeuroSAT solves SAT encodings of graph coloring, clique detection, dominating set, and vertex cover across distributions of small random graphs.This tests generalization to domains not represented in the training generator.
  • 1 INTRODUCTION: NeuroUNSAT identifies variables in small unsatisfiable cores, which can enable more efficient construction of resolution proofs.The same architecture is trained on problems whose unsatisfiability comes from a small contradiction.

2 PROBLEM SETUP

SAT is the task of determining whether a conjunctive-normal-form formula is satisfiable and, when it is, producing a satisfying assignment. The setup first frames satisfiability prediction as binary classification while retaining solving as the ultimate goal.

  • 2 PROBLEM SETUP: A CNF formula is a conjunction of clauses, each clause is a disjunction of literals, and satisfiability requires every clause to contain a true literal.A SAT problem asks whether such a formula is satisfiable and, if so, to produce a satisfying assignment.
  • 2 PROBLEM SETUP: The classification task learns φ(P), the satisfiability label, from problem-label pairs sampled from a SAT distribution and solved using an existing solver.At test time, only P is provided; the broader objective also includes finding solutions to satisfiable problems.
  • 2 PROBLEM SETUP: CNF conversion can be performed in linear time with only linear growth in the resulting formula size.This supports using CNF as the standard representation for SAT problems.

3 MODEL

NeuroSAT represents SAT instances as graphs and iteratively passes messages among literal, clause, and complementary-literal nodes. Its votes evolve from uncertain unsatisfiable predictions to a high-confidence satisfiable state on the illustrated problem.

  • 3 MODEL: NeuroSAT encodes each SAT instance as a graph with literal and clause nodes, literal-clause edges, and complementary-literal edges.This representation supports message passing without imposing an ordering on nodes or edges.
  • 3 MODEL: Each iteration first updates clause embeddings from neighboring literals, then updates literal embeddings from neighboring clauses and complementary literals.Figure 2 depicts these two message-passing stages on a small example.
  • 3 MODEL: The model uses learned multilayer perceptrons and layer-normalized LSTMs to update literal and clause embeddings over time.The embeddings are initialized from learned vectors and recurrently refined at each time step.
  • 3 MODEL: After T iterations, NeuroSAT converts final literal embeddings into scalar votes, averages them, and trains the resulting logit against the satisfiability label.The vote computation and sigmoid cross-entropy objective connect iterative inference to classification.
  • 3 MODEL: On the illustrated satisfiable problem, most literals initially vote unsatisfiable with low confidence before a phase transition produces uniformly high-confidence satisfiable votes.The final votes often encode one bit per variable, although they do not reliably form a satisfying assignment in general.
  • 3 MODEL: The learned parameters are independent of problem size, allowing one model to process inputs with varying numbers of literals and clauses.Aggregation over graph neighborhoods handles size variation.

4 TRAINING DATA

The training-data design aims to prevent satisfiability from being predicted using crude statistics, encouraging NeuroSAT to learn structure that may transfer across problem domains.

  • 4 TRAINING DATA: The authors construct SAT-problem distributions intended to force the network to learn substantive structure rather than exploit simple statistical cues.This design targets generalization beyond the generator used for training.

5 PREDICTING SATISFIABILITY

NeuroSAT was trained as a satisfiability classifier on random SR(40)-type problems using 26 message-passing iterations. It achieved 85% test accuracy despite the task's subtle examples.

  • NeuroSAT was trained as a classifier on random SAT problems from SR(U(10, 40)), using 26 message-passing iterations.The model used 128-dimensional embeddings and ADAM optimization.
  • Each SR(40) problem has 40 variables and nearly 200 clauses, while positive and negative examples differ by only one literal occurrence.This made the classification task highly non-trivial from a machine-learning perspective.
  • 85% test accuracy was achieved after training on the SR(U(10, 40)) distribution.

6 DECODING SATISFYING ASSIGNMENTS

NeuroSAT's internal dynamics evolve from low-confidence unsatisfiability votes to a sharp satisfiability phase transition. Its embeddings can reveal assignments, but direct vote decoding is unreliable, motivating clustering-based extraction.

  • 6 DECODING SATISFYING ASSIGNMENTS: Literal votes remain mostly low-confidence for unsatisfiable guesses, whereas correctly solved satisfiable problems undergo a phase transition to high-confidence satisfiability.After the transition, the votes converge and the network stops evolving.
  • 6 DECODING SATISFYING ASSIGNMENTS: At convergence, literal votes encode approximately one bit per variable, but those bits do not reliably form a satisfying assignment.The learned projection from embeddings to votes can fail to preserve the assignment structure.
  • 6 DECODING SATISFYING ASSIGNMENTS: Clustering the literal embeddings and trying both truth-value mappings decoded satisfying assignments for over 70% of satisfiable SR(40) test problems.Table 1 reports 73% correct satisfiability guesses and 70% assignment decoding on satisfiable problems.
  • 6 DECODING SATISFYING ASSIGNMENTS: PCA embeddings remain mixed and inseparable until the phase transition, then form two clusters corresponding to literals set to 0 and 1.

7 EXTRAPOLATING TO OTHER PROBLEM DISTRIBUTIONS

NeuroSAT extrapolated beyond its training size and distribution: more iterations enabled solving substantially larger SR(n) problems, while the same trained model solved encoded graph problems from new random-graph distributions.

  • 7.1 BIGGER PROBLEMS: For n = 200, NeuroSAT solved 25% of satisfiable SR(200) problems using four times more iterations than during training, despite 2160 times more possible assignments.With the training iteration budget, it solved under 10% of these problems.
  • 7.1 BIGGER PROBLEMS: Success on larger SR(n) problems increased when NeuroSAT was run for more iterations, including sizes much larger than those seen during training.Figure 5 plots success rate against iteration count across several n values.
  • 7.2 DIFFERENT PROBLEMS: NeuroSAT was tested on SAT encodings of graph coloring, clique detection, dominating set, and vertex cover across six random graph distributions.The generated graphs averaged ten nodes and seventeen edges.
  • 7.2 DIFFERENT PROBLEMS: 85% of 4,888 satisfiable encoded graph problems yielded successfully decoded solutions after 512 iterations.Survey Propagation did not independently converge to a satisfying assignment on any of these problems.

8 FINDING UNSAT CORES

NeuroUNSAT learns to recognize small unsatisfiable cores and can expose their literals, supporting more efficient resolution-proof construction when the core is small. Its recognition is highly accurate on the test distribution but is not expected to generalize to arbitrary unsat cores.

  • NeuroUNSAT learns to detect small unsat cores instead of searching for satisfying assignments.The literals involved in the core can be decoded from its internal activations.
  • When the unsat core is small relative to the formula, identifying its literals can enable more efficient resolution-proof construction.
  • 100% test accuracy shows that NeuroUNSAT predicts satisfiability on the SRC test set.The model appears to do so by recognizing the planted unsat cores.
  • The model distinguishes a satisfiable problem containing the modified core u′ from an unsatisfiable problem containing the core u.In the latter case, it votes unsat with high confidence.
  • 98% of test problems place the small core literals in their own cluster after 2-clustering the higher-dimensional literal embeddings.Clustering is more reliable than directly decoding the final literal votes.
  • NeuroUNSAT is not expected to generalize to arbitrary unsat cores because it may memorize specific subgraphs rather than learn a generic proof procedure.

9 RELATED WORK

Prior SAT-learning work mainly improves components of existing solvers, whereas NeuroSAT aims to solve SAT problems directly. Related neural approaches address structured prediction, entailment, or optimization, but differ in search capability or reasoning demands.

  • Earlier statistical-learning approaches target restart strategies, branching heuristics, parameter tuning, or solver selection.
  • These approaches assist existing SAT solvers rather than solving SAT problems on their own.
  • Palm et al. showed that an MPNN can predict unique Sudoku solutions, the closest machine-learning work identified by the paper.
  • Evans et al. predict propositional entailment by sampling candidate assignments, but their network does not perform heuristic search and handles only simple tractable problems.
  • Neural methods for combinatorial optimization learn useful heuristics, but finding low-cost solutions requires less precise reasoning than finding satisfying assignments.

10 DISCUSSION

The paper’s main scientific contribution is evidence that neural networks can perform discrete search independently after end-to-end training with minimal supervision. Practical SAT-solving impact remains uncertain because NeuroSAT is far less reliable than state-of-the-art solvers.

  • The study establishes that neural networks can perform discrete search without hard-coded search procedures or more than minimal supervision.
  • The authors frame this finding as contributing to understanding neural networks’ capabilities and limitations.
  • NeuroSAT remains vastly less reliable than state-of-the-art SAT solvers as an end-to-end solver.
  • The paper sees no obvious path to beating existing SAT solvers, while suggesting harder training problems or integration with traditional solvers as possible directions.
Loading 1802.03685v4…