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. The propositional satisfiability problem (SAT) is one of the most fundamental problems of computer science. BID4 showed that the problem is NP-complete, which means that searching for any kind of efficiently-checkable certificate in any context can be reduced to finding a satisfying assignment of a propositional formula. In practice, search problems arising from a wide range of domains such as hardware and software verification, test pattern generation, planning, scheduling, and combinatorics are all routinely solved by constructing an appropriate SAT problem and then calling a SAT solver BID9 . Modern SAT solvers based on backtracking search are extremely well-engineered and have been able to solve problems of practical interest with millions of variables BID2 ).We consider the question: can a neural network learn to solve SAT problems? To answer, we develop a novel message passing neural network (MPNN) BID21 BID16 BID8 , NeuroSAT, and train it as a classifier to predict satisfiability on a dataset of random SAT problems. We provide NeuroSAT with only a single bit of supervision for each SAT problem that indicates whether or not the problem is satisfiable. When making a prediction about a new SAT problem, we find that NeuroSAT guesses unsatisfiable with low confidence until it finds a solution, at which point it converges and guesses satisfiable with very high confidence. The solution itself can almost always be automatically decoded from the network's activations, making NeuroSAT an end-to-end SAT solver. See Figure 1 for an illustration of the train and test regimes.Although it is not competitive with state-of-the-art SAT solvers, NeuroSAT can solve SAT problems that are substantially larger and more difficult than it ever saw during training by simply performing more iterations of message passing. Despite only running for a few dozen iterations during training, at test time NeuroSAT continues to find solutions to harder problems after hundreds and even thousands of iterations. The learning process has yielded not a traditional classifier but rather a procedure that can be run indefinitely to search for solutions to problems of varying difficulty. Our main motivation has been scientific: to better understand the extent to which neural networks are capable of precise, logical reasoning. Our work has definitively established that neural networks can learn to perform discrete search on their own without the help of hard-coded search procedures, even after only end-to-end training with minimal supervision. We found this result surprising and think it constitutes an important contribution to the community's evolving understanding of the capabilities and limitations of neural networks.Although not our primary concern, we also hope that our findings eventually lead to improvements in practical SAT solving. As we stressed early on, as an end-to-end SAT solver the trained NeuroSAT system discussed in this paper is still vastly less reliable than the state-of-the-art. We concede that we see no obvious path to beating existing SAT solvers. One approach might be to continue to train NeuroSAT as an end-to-end solver on increasingly difficult problems. A second approach might be to use a system like NeuroSAT to help guide decisions within a more traditional SAT solver, though it is not clear that NeuroSAT provides any useful information before it finds a satisfying assignment. However, as we discussed in §8, when we trained our architecture on different data it learned an entirely different procedure. In a separate experiment omitted for space reasons, we also trained our architecture to predict whether there is a satisfying assignment involving each individual literal in the problem and found that it was able to predict these bits with high accuracy as well. Unlike NeuroSAT, it made both type I and type II errors, had no discernable phase transition, and could make reasonable predictions within only a few rounds. We believe that architectures descended from NeuroSAT will be able to learn very different mechanisms and heuristics depending on the data they are trained on and the details of their objective functions. We are cautiously optimistic that a descendant of NeuroSAT will one day lead to improvements to the state-of-the-art.
We train a graph network to predict boolean satisfiability and show that it learns to search for solutions, and that the solutions it finds can be decoded from its activations. The paper describes a general neural network architecture for predicting satisfiability This paper presents the NeuroSAT architecture which uses a deep message passing neural net for predicting the satisfiability of CNF instances