---
title: "Learning a SAT Solver from Single-Bit Supervision — Selsam 2018"
description: "They build NeuroSAT, a message passing neural network (MPNN). 27 references, cited by 56 papers here."
authors: ["Daniel Selsam", "Matthew Lamm", "Benedikt Bünz", "Percy Liang", "Leonardo de Moura", "David L. Dill"]
year: 2018
venue: "arXiv:1802.03685"
source: "https://arxiv.org/abs/1802.03685"
doi: "10.48550/arxiv.1802.03685"
arxiv: "1802.03685"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/selsam-2018-learning-sat-solver-single-bit/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/selsam-2018-learning-sat-solver-single-bit/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2018](https://md.research.elamur.ai/free/en/papers/2018/page/3/) / Learning a SAT Solver from Single-Bit Supervision

# Learning a SAT Solver from Single-Bit Supervision

**Authors:** [Daniel Selsam](https://md.research.elamur.ai/free/en/authors/daniel-selsam/), [Matthew Lamm](https://md.research.elamur.ai/free/en/authors/matthew-lamm/), Benedikt Bünz, [Percy Liang](https://md.research.elamur.ai/free/en/authors/percy-liang/), [Leonardo de Moura](https://md.research.elamur.ai/free/en/authors/leonardo-de-moura/) and David L. Dill · **Year:** 2018 · **Venue:** arXiv:1802.03685 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/1802.03685) · [PDF](https://arxiv.org/pdf/1802.03685v4) · [DOI 10.48550/arxiv.1802.03685](https://doi.org/10.48550/arxiv.1802.03685) · [arXiv 1802.03685](https://arxiv.org/abs/1802.03685) · [OpenAlex](https://openalex.org/W2786776430)

**Citations:** 176 citations (OpenAlex, 2026-10-14) · [56](https://md.research.elamur.ai/free/en/papers/selsam-2018-learning-sat-solver-single-bit/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Selsam et al. ask whether a neural network can learn to solve propositional satisfiability (SAT), an NP-complete problem, when it is told only whether each instance is satisfiable. They build NeuroSAT, a message passing neural network (MPNN). It represents a CNF formula as a graph of literal and clause nodes and updates their embeddings with layer-norm LSTMs. The design respects the symmetries of SAT: reordering variables, clauses or literals, or flipping the sign of a variable, cannot change its output. Training uses the SR(n) generator, which produces pairs of random problems: one satisfiable and one unsatisfiable, differing in a single literal. On satisfiable inputs the network shows a sudden phase transition to confident "sat" votes, and a satisfying assignment can usually be read from its activations. This makes NeuroSAT an end-to-end solver. Running more iterations lets it solve larger, harder problems than those seen in training, and it transfers to other encoded problems. It is still far weaker than conventional solvers. The work matters because it suggests neural networks can learn genuine search procedures from minimal supervision.

## Key points
- **Supervision:** each training example gives only one bit, satisfiable or not. Labels come from an existing SAT solver run on SR(n) instances.
- **SR(n) generator:** clause sizes are sampled with a mean slightly above 4. This blocks shortcuts based on crude statistics, because paired sat/unsat problems differ by negating a single literal occurrence.
- **Architecture:**
  - Learned initial vectors L_init and C_init.
  - Three MLPs: L_msg, C_msg and L_vote.
  - Two layer-norm LSTMs: L_u and C_u.
  - A Flip operator that exchanges messages between complementary literals.
  - The prediction is the mean of per-literal votes, trained with sigmoid cross-entropy.
  - No parameter depends on problem size.
- **Iterations:** training uses a few dozen message-passing rounds, while at test time the model keeps finding solutions after hundreds or thousands of rounds.
- **Generalization and NeuroUNSAT:** trained only on random SAT, NeuroSAT solves small random-graph instances of four other encoded problems: coloring a graph, finding a clique, finding a dominating set and finding a vertex cover. A variant trained on different data, NeuroUNSAT, instead pinpoints the variables of small contradictions, which can speed up building resolution proofs.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Stanford University](https://md.research.elamur.ai/free/en/universities/stanford-university/) — University, Stanford, United States · 506 works · 330,053 citations
- [Microsoft](https://md.research.elamur.ai/free/en/companies/microsoft/) — Company, Redmond, United States · 378 works · 161,630 citations

📚 Shelves (4): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 18,614 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 17,965 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 321 works · [🌐 Computer Networks and Communications](https://md.research.elamur.ai/free/en/shelves/computer-science/computer-networks-and-communications/) · 100 works

## Cite

Cite as: Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura and David L. Dill. 2018. Learning a SAT Solver from Single-Bit Supervision. arXiv:1802.03685.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{selsam2018learning,
  title = {{Learning a SAT Solver from Single-Bit Supervision}},
  author = {Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo {de Moura} and David L. Dill},
  year = {2018},
  doi = {10.48550/arxiv.1802.03685},
  eprint = {1802.03685},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1802.03685}
}
```

- [← previous Harvesting Paragraph-level Question-Answer Pairs from Wikipedia](https://md.research.elamur.ai/free/en/papers/du-2018-harvesting-paragraph-level-question-answer/)
- [next → Findings of the Third Shared Task on Multimodal Machine Translation](https://md.research.elamur.ai/free/en/papers/barrault-2018-findings-third-shared-task-multimodal/)
- [↑ back to papers of 2018](https://md.research.elamur.ai/free/en/papers/2018/page/3/)

## References

27 references, 3 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Jimmy Lei Ba, Jamie Ryan Kiros, and Geoffrey E Hinton. [Layer normalization](https://md.research.elamur.ai/free/en/papers/ba-2016-layer-normalization/). arXiv preprint arXiv:1607.06450, 2016.
2. Irwan Bello, Hieu Pham, Quoc V Le, Mohammad Norouzi, and Samy Bengio. Neural combinatorial optimization with reinforcement learning. arXiv preprint arXiv:1611.09940, 2016. [find](https://scholar.google.com/scholar?q=Irwan+Bello%2C+Hieu+Pham%2C+Quoc+V+Le%2C+Mohammad+Norouzi%2C+and+Samy+Bengio%2E+Neural+combinatorial+optimization+with+reinforcement+learning%2E+arXiv+preprint+arXiv%3A1611%2E09940%2C+2016%2E)
3. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. Conflict-driven clause learning sat solvers. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pp. 131–153, 2009. [find](https://scholar.google.com/scholar?q=Armin+Biere%2C+Marijn+Heule%2C+Hans+van+Maaren%2C+and+Toby+Walsh%2E+Conflict%2Ddriven+clause+learning+sat+solvers%2E+Handbook+of+Satisfiability%2C+Frontiers+in+Artificial+Intelligence+and+Applications%2C+pp%2E+131%E2%80%93153%2C)
4. Alfredo Braunstein, Marc Mézard, and Riccardo Zecchina. Survey propagation: An algorithm for satisfiability. Random Structures & Algorithms, 27(2):201–226, 2005. [find](https://scholar.google.com/scholar?q=Alfredo+Braunstein%2C+Marc+Me%CC%81zard%2C+and+Riccardo+Zecchina%2E+Survey+propagation%3A+An+algorithm+for+satisfiability%2E+Random+Structures+%26+Algorithms%2C+27%282%29%3A201%E2%80%93226%2C+2005%2E)
5. Stephen A Cook. The complexity of theorem-proving procedures. In Proceedings of the third annual ACM symposium on Theory of computing, pp. 151–158. ACM, 1971. [find](https://scholar.google.com/scholar?q=Stephen+A+Cook%2E+The+complexity+of+theorem%2Dproving+procedures%2E+In+Proceedings+of+the+third+annual+ACM+symposium+on+Theory+of+computing%2C+pp%2E+151%E2%80%93158%2E+ACM%2C+1971%2E)
6. Hanjun Dai, Elias B Khalil, Yuyu Zhang, Bistra Dilkina, and Le Song. Learning combinatorial optimization algorithms over graphs. arXiv preprint arXiv:1704.01665, 2017. [find](https://scholar.google.com/scholar?q=Hanjun+Dai%2C+Elias+B+Khalil%2C+Yuyu+Zhang%2C+Bistra+Dilkina%2C+and+Le+Song%2E+Learning+combinatorial+optimization+algorithms+over+graphs%2E+arXiv+preprint+arXiv%3A1704%2E01665%2C+2017%2E)
7. Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment? arXiv preprint arXiv:1802.08535, 2018. [find](https://scholar.google.com/scholar?q=Richard+Evans%2C+David+Saxton%2C+David+Amos%2C+Pushmeet+Kohli%2C+and+Edward+Grefenstette%2E+Can+neural+networks+understand+logical+entailment%3F+arXiv+preprint+arXiv%3A1802%2E08535%2C+2018%2E)
8. Alex Flint and Matthew Blaschko. Perceptron learning of sat. In Advances in Neural Information Processing Systems, pp. 2771–2779, 2012. [find](https://scholar.google.com/scholar?q=Alex+Flint+and+Matthew+Blaschko%2E+Perceptron+learning+of+sat%2E+In+Advances+in+Neural+Information+Processing+Systems%2C+pp%2E+2771%E2%80%932779%2C+2012%2E)
9. Justin Gilmer, Samuel S Schoenholz, Patrick F Riley, Oriol Vinyals, and George E Dahl. [Neural message passing for quantum chemistry](https://md.research.elamur.ai/free/en/papers/gilmer-2017-neural-message-passing-quantum-chemistry/). arXiv preprint arXiv:1704.01212, 2017.
10. Carla P Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. Satisfiability solvers. Foundations of Artificial Intelligence, 3:89–134, 2008. [find](https://scholar.google.com/scholar?q=Carla+P+Gomes%2C+Henry+Kautz%2C+Ashish+Sabharwal%2C+and+Bart+Selman%2E+Satisfiability+solvers%2E+Foundations+of+Artificial+Intelligence%2C+3%3A89%E2%80%93134%2C+2008%2E)
11. Cristian Grozea and Marius Popescu. Can machine learning learn a decision oracle for np problems? a test on sat. Fundamenta Informaticae, 131(3-4):441–450, 2014. [find](https://scholar.google.com/scholar?q=Cristian+Grozea+and+Marius+Popescu%2E+Can+machine+learning+learn+a+decision+oracle+for+np+problems%3F+a+test+on+sat%2E+Fundamenta+Informaticae%2C+131%283%2D4%29%3A441%E2%80%93450%2C+2014%2E)
12. Shai Haim and Toby Walsh. Restart strategy selection using machine learning techniques. CoRR, abs/0907.5032, 2009. — [arXiv:0907.5032](https://arxiv.org/abs/0907.5032) [find](https://scholar.google.com/scholar?q=Shai+Haim+and+Toby+Walsh%2E+Restart+strategy+selection+using+machine+learning+techniques%2E+CoRR%2C+abs%2F0907%2E5032%2C+2009%2E+%E2%80%94+%5BarXiv%3A0907%2E5032%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F0907%2E5032%29)
13. S. Hochreiter and J. Schmidhuber. Long short-term memory. Neural Computation, 9(8):1735–1780, 1997. [find](https://scholar.google.com/scholar?q=S%2E+Hochreiter+and+J%2E+Schmidhuber%2E+Long+short%2Dterm+memory%2E+Neural+Computation%2C+9%288%29%3A1735%E2%80%931780%2C+1997%2E)
14. Diederik Kingma and Jimmy Ba. [Adam: A method for stochastic optimization](https://md.research.elamur.ai/free/en/papers/kingma-2014-adam-method-stochastic-optimization/). arXiv preprint arXiv:1412.6980, 2014.
15. Donald E Knuth. The art of computer programming, volume 4, fascicle 6: Satisfiability, 2015. [find](https://scholar.google.com/scholar?q=Donald+E+Knuth%2E+The+art+of+computer+programming%2C+volume+4%2C+fascicle+6%3A+Satisfiability%2C+2015%2E)
16. Harry R Lewis. Computers and intractability. a guide to the theory of np-completeness, 1983. [find](https://scholar.google.com/scholar?q=Harry+R+Lewis%2E+Computers+and+intractability%2E+a+guide+to+the+theory+of+np%2Dcompleteness%2C+1983%2E)
17. Yujia Li, Daniel Tarlow, Marc Brockschmidt, and Richard Zemel. Gated graph sequence neural networks. arXiv preprint arXiv:1511.05493, 2015. [find](https://scholar.google.com/scholar?q=Yujia+Li%2C+Daniel+Tarlow%2C+Marc+Brockschmidt%2C+and+Richard+Zemel%2E+Gated+graph+sequence+neural+networks%2E+arXiv+preprint+arXiv%3A1511%2E05493%2C+2015%2E)
18. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for sat solvers. In International Conference on Theory and Applications of Satisfiability Testing, pp. 123–140. Springer, 2016. [find](https://scholar.google.com/scholar?q=Jia+Hui+Liang%2C+Vijay+Ganesh%2C+Pascal+Poupart%2C+and+Krzysztof+Czarnecki%2E+Learning+rate+based+branching+heuristic+for+sat+solvers%2E+In+International+Conference+on+Theory+and+Applications+of+Satisfiability+)
19. Mark Newman. Networks: an introduction. Oxford university press, 2010. [find](https://scholar.google.com/scholar?q=Mark+Newman%2E+Networks%3A+an+introduction%2E+Oxford+university+press%2C+2010%2E)
20. Rasmus Berg Palm, Ulrich Paquet, and Ole Winther. Recurrent relational networks for complex relational reasoning. arXiv preprint arXiv:1711.08028, 2017. — [arXiv:1711.08028](https://arxiv.org/abs/1711.08028) [find](https://scholar.google.com/scholar?q=Rasmus+Berg+Palm%2C+Ulrich+Paquet%2C+and+Ole+Winther%2E+Recurrent+relational+networks+for+complex+relational+reasoning%2E+arXiv+preprint+arXiv%3A1711%2E08028%2C+2017%2E+%E2%80%94+%5BarXiv%3A1711%2E08028%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1711)
21. Razvan Pascanu, Tomas Mikolov, and Yoshua Bengio. Understanding the exploding gradient problem. CoRR, abs/1211.5063, 2012. [find](https://scholar.google.com/scholar?q=Razvan+Pascanu%2C+Tomas+Mikolov%2C+and+Yoshua+Bengio%2E+Understanding+the+exploding+gradient+problem%2E+CoRR%2C+abs%2F1211%2E5063%2C+2012%2E)
22. Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model. IEEE Transactions on Neural Networks, 20(1):61–80, 2009. [find](https://scholar.google.com/scholar?q=Franco+Scarselli%2C+Marco+Gori%2C+Ah+Chung+Tsoi%2C+Markus+Hagenbuchner%2C+and+Gabriele+Monfardini%2E+The+graph+neural+network+model%2E+IEEE+Transactions+on+Neural+Networks%2C+20%281%29%3A61%E2%80%9380%2C+2009%2E)
23. Rishabh Singh, Joseph P Near, Vijay Ganesh, and Martin Rinard. Avatarsat: An auto-tuning boolean sat solver. 2009. [find](https://scholar.google.com/scholar?q=Rishabh+Singh%2C+Joseph+P+Near%2C+Vijay+Ganesh%2C+and+Martin+Rinard%2E+Avatarsat%3A+An+auto%2Dtuning+boolean+sat+solver%2E+2009%2E)
24. Niklas Sorensson and Niklas Een. Minisat v1. 13-a sat solver with conflict-clause minimization. SAT, 2005(53):1–2, 2005. [find](https://scholar.google.com/scholar?q=Niklas+Sorensson+and+Niklas+Een%2E+Minisat+v1%2E+13%2Da+sat+solver+with+conflict%2Dclause+minimization%2E+SAT%2C+2005%2853%29%3A1%E2%80%932%2C+2005%2E)
25. G Tseitin. On the complexity ofderivation in propositional calculus. Studies in Constrained Mathematics and Mathematical Logic, 1968. [find](https://scholar.google.com/scholar?q=G+Tseitin%2E+On+the+complexity+ofderivation+in+propositional+calculus%2E+Studies+in+Constrained+Mathematics+and+Mathematical+Logic%2C+1968%2E)
26. O. Vinyals, M. Fortunato, and N. Jaitly. Pointer networks. In Advances in Neural Information Processing Systems (NIPS), pp. 2674–2682, 2015. [find](https://scholar.google.com/scholar?q=O%2E+Vinyals%2C+M%2E+Fortunato%2C+and+N%2E+Jaitly%2E+Pointer+networks%2E+In+Advances+in+Neural+Information+Processing+Systems+%28NIPS%29%2C+pp%2E+2674%E2%80%932682%2C+2015%2E)
27. L. Xu, F. Hutter, H. H. Hoos, and K. Leyton-Brown. SATzilla: portfolio-based algorithm selection for SAT. Journal of Artificial Intelligence Research (JAIR), 32:565–606, 2008. [find](https://scholar.google.com/scholar?q=L%2E+Xu%2C+F%2E+Hutter%2C+H%2E+H%2E+Hoos%2C+and+K%2E+Leyton%2DBrown%2E+SATzilla%3A+portfolio%2Dbased+algorithm+selection+for+SAT%2E+Journal+of+Artificial+Intelligence+Research+%28JAIR%29%2C+32%3A565%E2%80%93606%2C+2008%2E)

*Updated 2 November 2026*