Search all library resources

Neural networks and the satisfiability problem

Neural networks and satisfiability (SAT) solvers are two of the crowning achievements of computer science, and have each brought vital improvements to diverse real-world problems. In the past few years, researchers have begun to apply increasingly sophisticated neural network architectures to increasingly challenging problems, with many encouraging results. In the SAT field, on the other hand, after two decades of consistent, staggering improvements in the performance of SAT solvers, the rate of improvement has declined significantly. Together these observations raise two critical scientific questions. First, what are the fundamental capabilities of neural networks? Second, can neural networks be leveraged to improve high-performance SAT solvers? We consider these two questions and make the following two contributions. First, we demonstrate a surprising capability of neural networks. We show that a simple neural network architecture trained in a certain way can learn to solve SAT problems on its own without the help of hard-coded search procedures, even after only end-to-end training with minimal supervision. Thus we establish that neural networks are capable of learning to perform discrete search. Second, we show that neural networks can indeed be leveraged to improve high-performance SAT solvers. We use the same neural network architecture to provide heuristic guidance to several state-of-the-art SAT solvers, and find that each enhanced solver solves substantially more problems than the original on a benchmark of challenging and diverse real-world SAT problems.