Elamur Research⌕
☰
home / papers / 2018 / Learning a SAT Solver from Single-Bit Supervision

Learning a SAT Solver from Single-Bit Supervision

Paper · 2018 · Daniel Selsam, Matthew Lamm, Benedikt Bünz et al.

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 UniversityStanford · United States506 works · 330,052 citations🏢MicrosoftRedmond · United States378 works · 161,630 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksComputational Theory and Mathematics · 321 worksComputer 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. DOI 10.48550/arxiv.1802.03685 · arXiv 1802.03685

@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}
}

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. 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
  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
  4. Alfredo Braunstein, Marc Mézard, and Riccardo Zecchina. Survey propagation: An algorithm for satisfiability. Random Structures & Algorithms, 27(2):201–226, 2005. find
  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
  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
  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
  8. Alex Flint and Matthew Blaschko. Perceptron learning of sat. In Advances in Neural Information Processing Systems, pp. 2771–2779, 2012. find
  9. Justin Gilmer, Samuel S Schoenholz, Patrick F Riley, Oriol Vinyals, and George E Dahl. Neural message passing for 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
  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
  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
  13. S. Hochreiter and J. Schmidhuber. Long short-term memory. Neural Computation, 9(8):1735–1780, 1997. find
  14. Diederik Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980, 2014.
  15. Donald E Knuth. The art of computer programming, volume 4, fascicle 6: Satisfiability, 2015. find
  16. Harry R Lewis. Computers and intractability. a guide to the theory of np-completeness, 1983. find
  17. Yujia Li, Daniel Tarlow, Marc Brockschmidt, and Richard Zemel. Gated graph sequence neural networks. arXiv preprint arXiv:1511.05493, 2015. find
  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
  19. Mark Newman. Networks: an introduction. Oxford university press, 2010. find
  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
  21. Razvan Pascanu, Tomas Mikolov, and Yoshua Bengio. Understanding the exploding gradient problem. CoRR, abs/1211.5063, 2012. find
  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
  23. Rishabh Singh, Joseph P Near, Vijay Ganesh, and Martin Rinard. Avatarsat: An auto-tuning boolean sat solver. 2009. find
  24. Niklas Sorensson and Niklas Een. Minisat v1. 13-a sat solver with conflict-clause minimization. SAT, 2005(53):1–2, 2005. find
  25. G Tseitin. On the complexity ofderivation in propositional calculus. Studies in Constrained Mathematics and Mathematical Logic, 1968. find
  26. O. Vinyals, M. Fortunato, and N. Jaitly. Pointer networks. In Advances in Neural Information Processing Systems (NIPS), pp. 2674–2682, 2015. find
  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

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/selsam-2018-learning-sat-solver-single-bit/