Learning a SAT solver from single-bit supervision

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

Learning a SAT solver from single-bit supervision

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

Computer Science

Research output: Contribution to conference › Paper › peer-review

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.

Original language	English (US)
State	Published - 2019
Event	7th International Conference on Learning Representations, ICLR 2019 - New Orleans, United States Duration: May 6 2019 → May 9 2019

Conference

Conference	7th International Conference on Learning Representations, ICLR 2019
Country/Territory	United States
City	New Orleans
Period	5/6/19 → 5/9/19

ASJC Scopus subject areas

Education
Computer Science Applications
Linguistics and Language
Language and Linguistics

Cite this

@conference{a179b1c8d009487cbe4046eae9147238,

title = "Learning a SAT solver from single-bit supervision",

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.",

author = "Daniel Selsam and Matthew Lamm and Benedikt B{\"u}nz and Percy Liang and Dill, {David L.} and {De Moura}, Leonardo",

note = "Publisher Copyright: {\textcopyright} 7th International Conference on Learning Representations, ICLR 2019. All Rights Reserved.; 7th International Conference on Learning Representations, ICLR 2019 ; Conference date: 06-05-2019 Through 09-05-2019",

year = "2019",

language = "English (US)",

}

TY - CONF

T1 - Learning a SAT solver from single-bit supervision

AU - Selsam, Daniel

AU - Lamm, Matthew

AU - Bünz, Benedikt

AU - Liang, Percy

AU - Dill, David L.

AU - De Moura, Leonardo

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85083950252&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85083950252&partnerID=8YFLogxK

M3 - Paper

AN - SCOPUS:85083950252

T2 - 7th International Conference on Learning Representations, ICLR 2019

Y2 - 6 May 2019 through 9 May 2019

ER -

Learning a SAT solver from single-bit supervision

Abstract

Conference

ASJC Scopus subject areas

Other files and links

Fingerprint

Cite this