Neural networks and the satisfiability problem
Abstract/Contents
- Abstract
- 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.
Description
| Type of resource | text |
|---|---|
| Form | electronic resource; remote; computer; online resource |
| Extent | 1 online resource. |
| Place | California |
| Place | [Stanford, California] |
| Publisher | [Stanford University] |
| Copyright date | 2019; ©2019 |
| Publication date | 2019; 2019 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Author | Selsam, Daniel |
|---|---|
| Degree supervisor | Dill, David L |
| Degree supervisor | Liang, Percy |
| Thesis advisor | Dill, David L |
| Thesis advisor | Liang, Percy |
| Thesis advisor | Ré, Christopher |
| Degree committee member | Ré, Christopher |
| Associated with | Stanford University, Computer Science Department. |
Subjects
| Genre | Theses |
|---|---|
| Genre | Text |
Bibliographic information
| Statement of responsibility | Daniel Selsam. |
|---|---|
| Note | Submitted to the Computer Science Department. |
| Thesis | Thesis Ph.D. Stanford University 2019. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2019 by Daniel Selsam
- License
- This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).
Also listed in
Loading usage metrics...