Elamur Research⌕
☰
home / papers / 2019 / Guiding High-Performance SAT Solvers with Unsat-Core Predictions

Guiding High-Performance SAT Solvers with Unsat-Core Predictions

Paper · 2019 · Daniel Selsam and Nikolaj Bjørner

Summary

The paper asks whether NeuroSAT, a graph neural network previously tested only on toy SAT instances, can make industrial-strength SAT solvers faster on real benchmarks. Rather than using it as a standalone solver, the authors train a simplified variant, called NeuroCore, to estimate how likely each variable is to belong to an unsatisfiable core. SATCOMP contains only about a thousand unsatisfiable problems, so they built a larger training set by repeatedly splitting existing instances into subproblems and labelling core variables from DRAT proofs. They then changed MiniSat, Glucose and Z3 so that, every so often, the solver discards its EVSIDS activity scores and resets them from NeuroCore's predictions over the whole formula, including learnt clauses. The authors call this "periodic refocusing." The solver's usual fast heuristic still makes all the individual branching decisions between these resets. All three modified solvers solve noticeably more SATCOMP-2018 instances than the unmodified versions. This is evidence that neural guidance can improve state-of-the-art solvers on practical problems.

Key points

  • Data generation: About 150,000 labelled datapoints were produced from SATCOMP problems (through 2017) plus a few hundred hard scheduling instances. The pipeline:
    • The ray framework distributed the work across many machines.
    • Z3 attempted each subproblem with a 60-second limit.
    • For unsatisfiable subproblems, DRAT-trim extracted the core.
    • Unsolved subproblems were split in two using the March heuristic and requeued.
  • Model: NeuroCore is built from three MLPs with embedding size d = 80. It operates on a sparse clause–literal matrix and passes messages between clause and literal embeddings.
  • Results on SATCOMP-2018 (5,000 s timeout): Compared with the original solvers, modified MiniSat solves 10% more problems, Glucose 4.1 solves 11% more, and Z3 solves 6% more.
  • Domain specialization: On the hard scheduling benchmark with a one-hour timeout, modified Glucose solves 20% more problems.
  • Other directions and code: The authors also report less successful experiments with imitating March, predicting variable phases, and reinforcement learning. Code is available at github.com/dselsam/neurocore-public.

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 States567 works · 335,190 citations🏢MicrosoftRedmond · United States403 works · 162,838 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 worksComputer Networks and Communications · 115 works

Cite

Cite as Daniel Selsam and Nikolaj Bjørner. 2019. Guiding High-Performance SAT Solvers with Unsat-Core Predictions. arXiv:1903.04671 (International Conference on Theory and Applications of Satisfiability Testing. Springer, Cham, 2019).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.1903.04671 · arXiv 1903.04671

@misc{selsam2019guiding,
  title = {{Guiding High-Performance SAT Solvers with Unsat-Core Predictions}},
  author = {Daniel Selsam and Nikolaj Bjørner},
  year = {2019},
  doi = {10.48550/arxiv.1903.04671},
  eprint = {1903.04671},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1903.04671}
}

References

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

  1. Abadi, M., Barham, P., Chen, J., Chen, Z., Davis, A., Dean, J., Devin, M., Ghemawat, S., Irving, G., Isard, M., et al.: Tensorflow: A system for large-scale machine learning. In: 12th USENIX Symposium on Operating Systems Design and Implementation OSDI 16. pp. 265–283 (2016)
  2. Balcan, M., Dick, T., Sandholm, T., Vitercik, E.: Learning to branch. In: Dy, J.G., Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmässan, Stockholm, Sweden, July 10-15, 2018. JMLR Workshop and Conference Proceedings, vol. 80, pp. 353–36… find
  3. Balunovic, M., Bielik, P., Vechev, M.T.: Learning to solve SMT formulas. In: Bengio, S., Wallach, H.M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 201… find
  4. Biere, A., Fröhlich, A.: Evaluating CDCL variable scoring schemes. In: International Conference on Theory and Applications of Satisfiability Testing. pp. 405– 422. Springer (2015) find
  5. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009) Guiding High-Performance SAT Solvers with Unsat-Core Predictions find
  6. De Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Automated Reasoning and Mathematics, pp. 15–44. Springer (2013) find
  7. Devlin, J., Uesato, J., Bhupatiraju, S., Singh, R., Mohamed, A.r., Kohli, P.: Robustfill: Neural program learning under noisy I/O. In: Proceedings of the 34th International Conference on Machine Learning-Volume 70. pp. 990–998. JMLR. org (2017) find
  8. Heule, M., van Maaren, H.: Look-ahead based SAT solvers. In: Biere et al. [5], pp. 155–184. https://doi.org/10.3233/978-1-58603-929-5-155 — [doi:10.3233/978-1-58603-929-5-155](https://doi.org/10.3233/978-1-58603-929-5-155) ↗
  9. Heule, M.J.: Schur number five. In: Thirty-Second AAAI Conference on Artificial Intelligence (2018) find
  10. Heule, M.J., Kullmann, O., Biere, A.: Cube-and-conquer for satisfiability. In: Handbook of Parallel Constraint Reasoning, pp. 31–59. Springer (2018) find
  11. Heule, M.J., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: International Conference on Theory and Applications of Satisfiability Testing. pp. 228–245. Springer (2016) find
  12. Proceedings of sat competition 2018; solver and benchmark descriptions (2018), http://hdl.handle.net/10138/237063 ↗
  13. Hinton, G., Deng, L., Yu, D., Dahl, G., Mohamed, A.r., Jaitly, N., Senior, A., Vanhoucke, V., Nguyen, P., Kingsbury, B., et al.: Deep neural networks for acoustic modeling in speech recognition. IEEE Signal processing magazine 29 (2012) find
  14. Hochreiter, S., Schmidhuber, J.: Long short-term memory. Neural Computation 9(8), 1735–1780 (1997) find
  15. Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9706, pp. 313–329. Springer… — [doi:10.1007/978-3-319-40229-1](https://doi.org/10.1007/978-3-319-40229-1) find
  16. Huang, D., Dhariwal, P., Song, D., Sutskever, I.: Gamepad: A learning environment for theorem proving. arXiv preprint arXiv:1806.00608 (2018)
  17. Irving, G., Szegedy, C., Alemi, A.A., Een, N., Chollet, F., Urban, J.: Deepmath-deep sequence models for premise selection. In: Advances in Neural Information Processing Systems. pp. 2235–2243 (2016)
  18. Kaliszyk, C., Chollet, F., Szegedy, C.: Holstep: A machine learning dataset for higher-order logic theorem proving. arXiv preprint arXiv:1703.00426 (2017)
  19. Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980 (2014)
  20. Knuth, D.E.: Estimating the efficiency of backtrack programs. Mathematics of computation 29(129), 122–136 (1975) find
  21. Knuth, D.E.: The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability (2015) find
  22. Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep convolutional neural networks. In: Advances in neural information processing systems. pp. 1097–1105 (2012)
  23. Kullback, S., Leibler, R.A.: On information and sufficiency. The annals of mathematical statistics 22(1), 79–86 (1951) find
  24. Kullmann, O.: Fundaments of branching heuristics. In: Biere et al. [5], pp. 205–244. https://doi.org/10.3233/978-1-58603-929-5-205 — [doi:10.3233/978-1-58603-929-5-205](https://doi.org/10.3233/978-1-58603-929-5-205) ↗
  25. Lawler, E.L., Wood, D.E.: Branch-and-bound methods: A survey. Operations research 14(4), 699–719 (1966) D. Selsam and N. Bjørner find
  26. Liang, J., K., H.G.V., Poupart, P., Czarnecki, K., Ganesh, V.: An empirical study of branching heuristics through the lens of global learning rate. In: Lang, J. (ed.) Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm,… — [doi:10.24963/ijcai.2018/745](https://doi.org/10.24963/ijcai.2018/745) find
  27. Loos, S.M., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017. EPiC Series in Computing, vol. 46, pp. 85–105.…
  28. Marques-Silva, J.P., Sakallah, K.A.: Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48(5), 506–521 (1999) find
  29. Mijnders, S., de Wilde, B., Heule, M.: Symbiosis of search and heuristics for random 3-sat. CoRR abs/1402.4455 (2010) — [arXiv:1402.4455](https://arxiv.org/abs/1402.4455) find
  30. Moritz, P., Nishihara, R., Wang, S., Tumanov, A., Liaw, R., Liang, E., Elibol, M., Yang, Z., Paul, W., Jordan, M.I., et al.: Ray: A distributed framework for emerging {AI} applications. In: 13th USENIX Symposium on Operating Systems Design and Implementation OSDI 18). pp. 561–577 (2018) find
  31. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proceedings of the 38th annual Design Automation Conference. pp. 530–535. ACM (2001)
  32. Oh, C.: Between SAT and UNSAT: the fundamental difference in CDCL SAT. In: Heule, M., Weaver, S. (eds.) Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9340, pp.… — [doi:10.1007/978-3-319-24318-4](https://doi.org/10.1007/978-3-319-24318-4) find
  33. Parisotto, E., Mohamed, A.r., Singh, R., Li, L., Zhou, D., Kohli, P.: Neuro-symbolic program synthesis. arXiv preprint arXiv:1611.01855 (2016)
  34. Ryan, L.: Efficient algorithms for clause-learning SAT solvers (2004), masters thesis find
  35. Schulz, S.: E–a brainiac theorem prover. Ai Communications 15(2, 3), 111–126 (2002) find
  36. Schulz, S.: We know (nearly) nothing! but can we learn? In: Reger, G., Traytel, D. (eds.) ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017. EPiC Series in Computing, vol. 51, pp. 29–32. E… find
  37. Selsam, D., Lamm, M., Bünz, B., Liang, P., de Moura, L., Dill, D.L.: Learning a SAT solver from single-bit supervision. In: International Conference on Learning Representations (2019), https://openreview.net/forum?id=HJMC_iA5tm ↗
  38. Silver, D., Schrittwieser, J., Simonyan, K., Antonoglou, I., Huang, A., Guez, A., Hubert, T., Baker, L., Lai, M., Bolton, A., et al.: Mastering the game of go without human knowledge. Nature 550(7676), 354–359 (2017) find
  39. Sutcliffe, G.: The CADE ATP System Competition - CASC. AI Magazine 37(2), 99–101 (2016) find
  40. Tammet, T.: Gandalf. J. Autom. Reasoning 18(2), 199–204 (1997). https://doi.org/10.1023/A:1005887414560 — [doi:10.1023/a:1005887414560](https://doi.org/10.1023/a:1005887414560) ↗
  41. Urban, J., Sutcliffe, G., Pudlák, P., Vyskocil, J.: Malarea SG1- machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Guiding High-Performance SAT Solvers with Unsat-Core Predictions Conferenc… — [doi:10.1007/978-3-540-71070-7](https://doi.org/10.1007/978-3-540-71070-7) find
  42. Wang, M., Tang, Y., Wang, J., Deng, J.: Premise selection for theorem proving by deep graph embedding. In: Advances in Neural Information Processing Systems. pp. 2786–2796 (2017)
  43. Wetzler, N., Heule, M.J., Hunt, W.A.: Drat-trim: Efficient checking and trimming using expressive clausal proofs. In: International Conference on Theory and Applications of Satisfiability Testing. pp. 422–429. Springer (2014) find
  44. Whalen, D.: Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644 (2016)
  45. Wu, Y., Schuster, M., Chen, Z., Le, Q.V., Norouzi, M., Macherey, W., Krikun, M., Cao, Y., Gao, Q., Macherey, K., et al.: Google’s neural machine translation system: Bridging the gap between human and machine translation. arXiv preprint arXiv:1609.08144 (2016) find
  46. Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565–606 (2008). https://doi.org/10.1613/jair.2490 — [doi:10.1613/jair.2490](https://doi.org/10.1613/jair.2490) ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/selsam-2019-guiding-high-performance-sat-solvers/