Elamur Research⌕
☰
home / papers / 2018 / Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning

Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning

Paper · 2018 · Gil Lederman, Markus N. Rabe, Edward A. Lee et al.

Summary

The paper asks whether deep reinforcement learning can produce better branching heuristics for solvers of quantified Boolean formulas (QBF), specifically 2QBF of the form ∀X.∃Y.ϕ with ϕ in CNF. The authors turn CADET, an open-source solver based on Incremental Determinization, into an RL environment. The agent picks which variable to branch on and which value to assign, while the solver does everything else. CADET can emit proofs that an independent tool checks, so the agent cannot score well by exploiting solver bugs. Each formula becomes a graph linking variables (or literals) to the clauses they appear in. A Graph Neural Network then builds per-formula variable embeddings, and a policy network scores candidate decisions. Because the parameter count stays small and fixed, the method scales to large formulas. On a family of hard benchmark formulas, the learned heuristic solves noticeably more instances than the handwritten VSIDS heuristic, even though neural inference slows decisions considerably. This shows that learned heuristics embedded inside a symbolic solver can push past existing state-of-the-art tools.

Key points

  • Neural decisions cut the solver's decision rate by at least 10x. The learned choices must therefore be far better than VSIDS to pay off in wall-clock time.
  • A model trained on the Words dataset was tested without retraining on Words30, whose formulas average 186.6 variables. It kept similar relative performance against VSIDS and Random, so it generalizes to larger and harder formulas. Transfer across different benchmark families remains limited.
  • A GNN with a single iteration worked best in real time. Two or three iterations reduced decision counts only slightly and slowed inference.
  • With zero GNN iterations (no neighborhood information), the model beat Random but fell short of VSIDS. This indicates that the 1-hop graph neighborhood is crucial.
  • The best model did not use VSIDS activity scores. Adding them sped up training but slightly hurt test results, especially on harder problems.

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

🏢GoogleMountain View · United States533 works · 443,885 citations🎓University of California, BerkeleyBerkeley · United States243 works · 251,774 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 Gil Lederman, Markus N. Rabe, Edward A. Lee and Sanjit A. Seshia. 2018. Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning. arXiv:1807.08058.

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

@misc{lederman2018learning,
  title = {{Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning}},
  author = {Gil Lederman, Markus N. Rabe, Edward A. Lee and Sanjit A. Seshia},
  year = {2018},
  doi = {10.48550/arxiv.1807.08058},
  eprint = {1807.08058},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1807.08058}
}

References

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

  1. Miltiadis Allamanis, Pankajan Chanthirasegaran, Pushmeet Kohli, and Charles Sutton. Learning continuous semantic representations of symbolic expressions. arXiv preprint arXiv:1611.01423, 2016.
  2. Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD…
  3. Saeed Amizadeh, Sergiy Matusevych, and Markus Weimer. Learning to solve circuit-sat: An unsupervised differentiable approach. In ICLR, 2019. find
  4. Gilles Audemard and Laurent Simon. Glucose in the SAT 2014 competition. find
  5. SAT COMPETITION 2014, pp. 31, 2014. find
  6. Lei Jimmy Ba, Ryan Kiros, and Geoffrey E. Hinton. Layer normalization. CoRR, abs/1607.06450, 2016. URL http://arxiv.org/abs/1607.06450. ↗
  7. Mislav Balunovic, Pavol Bielik, and Martin Vechev. Learning to solve smt formulas. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (eds.), Advances in Neural Information Processing Systems 31, pp. 10317–10328. Curran Associates, Inc., 2018. URL http://papers.nips… ↗
  8. Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher-order theorem proving (extended version). CoRR, abs/1904.03241, 2019. URL http://arxiv.org/abs/1904.03241. ↗
  9. Armin Biere. Resolve and expand. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 59–70. Springer, 2004. find
  10. Armin Biere. Lingeling, plingeling, picosat and precosat at sat race 2010. FMV Report Series Technical Report, 10(1), 2010. find
  11. Armin Biere, Alessandro Cimatti, Edmund M Clarke, Ofer Strichman, Yunshan Zhu, et al. Bounded model checking. Advances in computers, 58(11):117–148, 2003. find
  12. Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185. IOS press, 2009. find
  13. Samuel R Bowman, Christopher Potts, and Christopher D Manning. Recursive neural networks can learn logical semantics. arXiv preprint arXiv:1406.1827, 2014. find
  14. Junyoung Chung, Çaglar Gülçehre, KyungHyun Cho, and Yoshua Bengio. Empirical evaluation of gated recurrent neural networks on sequence modeling. CoRR, abs/1412.3555, 2014. URL http://arxiv.org/abs/1412.3555. ↗
  15. Byron Cook, Daniel Kroening, Philipp Rümmer, and Christoph M Wintersteiger. Ranking function synthesis for bit-vector relations. Formal methods in system design, 43(1):93–120, 2013. find
  16. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM (JACM), 7(3):201–215, 1960. find
  17. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, 1962. find
  18. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 502–518. Springer, 2003.
  19. Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment? arXiv preprint arXiv:1802.08535, 2018.
  20. Peter Faymonville, Bernd Finkbeiner, Markus N Rabe, and Leander Tentrup. Encodings of bounded synthesis. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 354–370. Springer, 2017. find
  21. Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. QUBE: A system for deciding quantified boolean formulas satisfiability. In International Joint Conference on Automated Reasoning, pp. 364–369. Springer, 2001. find
  22. Eugene Goldberg and Yakov Novikov. Berkmin: A fast and robust sat-solver. Discrete Applied Mathematics, 155(12):1549–1561, 2007. find
  23. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. In Advances in Neural Information Processing Systems, pp. 2235–2243, 2016.
  24. Mikoláš Janota. Towards generalization in QBF solving via machine learning. In AAAI Conference on Artificial Intelligence, 2018a. find
  25. Mikoláš Janota. Circuit-based search space pruning in QBF. In International Conference on Theory and Applications of Satisfiability Testing (SAT). Springer, 2018b. find
  26. Mikoláš Janota and Joao Marques-Silva. Abstraction-based algorithm for 2QBF. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 230–244. Springer, 2011. find
  27. Mikolás Janota and Joao Marques-Silva. Solving QBF by clause selection. In IJCAI, pp. 325–331, 2015. find
  28. Mikoláš Janota, William Klieber, Joao Marques-Silva, and Edmund Clarke. Solving QBF with counterexample guided refinement. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 114–128. Springer, 2012. find
  29. Robert G Jeroslow and Jinchang Wang. Solving propositional satisfiability problems. Annals of mathematics and Artificial Intelligence, 1(1-4):167–187, 1990. find
  30. Charles Jordan and Łukasz Kaiser. Experiments with reduction finding. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 192–207. Springer, 2013. find
  31. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Mirek Olšák. Reinforcement learning of theorem proving. arXiv preprint arXiv:1805.07563, 2018.
  32. William Klieber. Ghostq QBF solver system description, 2012. find
  33. Mitsuru Kusumoto, Keisuke Yahata, and Masahiro Sakai. Automated theorem proving in intuitionistic propositional logic by deep reinforcement learning. arXiv preprint arXiv:1811.00796, 2018.
  34. 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 (SAT), pp. 123–140. Springer, 2016. find
  35. Florian Lonsing and Armin Biere. DepQBF: A dependency-aware QBF solver. JSAT, 7(2-3):71–76, 2010. find
  36. Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. arXiv preprint arXiv:1701.06972, 2017.
  37. João P Marques-Silva and Karem A Sakallah. GRASP - A new search algorithm for satisfiability. In Computer Aided Design, pp. 220–227. IEEE, 1997. find
  38. Tomas Mikolov, Kai Chen, Greg Corrado, and Jeffrey Dean. Efficient estimation of word representations in vector space. arXiv preprint arXiv:1301.3781, 2013.
  39. Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th annual Design Automation Conference, pp. 530–535. ACM, 2001a.
  40. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings DAC, pp. 530–535. ACM, 2001b. ISBN 1-58113-297-2. doi: 10.1145/378239.379017.
  41. Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. CoRR, abs/1905.10006, 2019. URL http://arxiv.org/abs/1905.10006. ↗
  42. Florian Pigorsch and Christoph Scholl. An AIG-based QBF-solver using SAT for preprocessing. In Proceedings of the 47th Design Automation Conference, pp. 170–175. ACM, 2010. find
  43. Luca Pulina. The ninth QBF solvers evaluation-preliminary report. In QBF@ SAT, pp. 1–13, 2016. find
  44. Markus N Rabe and Sanjit A Seshia. Incremental determinization. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 375–392. Springer International Publishing, 2016. find
  45. Markus N Rabe and Leander Tentrup. CAQE: A certifying QBF solver. In Formal Methods in Computer-Aided Design (FMCAD), 2015, pp. 136–143. find
  46. Markus N Rabe, Leander Tentrup, Cameron Rasmussen, and Sanjit A Seshia. Understanding and extending incremental determinization for 2QBF. In International Conference on Computer Aided Verification (accepted), 2018. find
  47. Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model. Trans. Neur. Netw., 20(1):61– 80, January 2009. ISSN 1045-9227. doi: 10.1109/TNN.2008.2005605. URL http://dx.doi.org/10.1109/TNN.2008.2005605. — [doi:10.1109/tnn.2008.2005605](https://doi.org/10.1109/tnn.2008.2005605) ↗
  48. Daniel Selsam and Nikolaj Bjørner. Neurocore: Guiding high-performance SAT solvers with unsat-core predictions. CoRR, abs/1903.04671, 2019. URL http://arxiv.org/abs/1903.04671. ↗
  49. Daniel Selsam, Matthew Lamm, Benedikt Bunz, Percy Liang, Leonardo de Moura, and David L Dill. Learning a SAT solver from single-bit supervision. arXiv preprint arXiv:1802.03685, 2018.
  50. Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. Combinatorial sketching for finite programs. ACM Sigplan Notices, 41(11):404–415, 2006. find
  51. Mate Soos. Cryptominisat v4. SAT Competition, pp. 23, 2014. find
  52. Leander Tentrup. Non-prenex QBF solving using abstraction. In International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 393–401. Springer, 2016. find
  53. Leander Tentrup. On expansion and resolution in CEGAR based QBF solving. In International Conference on Computer Aided Verification, pp. 475–494. Springer, 2017. find
  54. Grigori S Tseitin. On the complexity of derivation in propositional calculus. Studies in constructive mathematics and mathematical logic, 2(115-125):10–13, 1968. find
  55. Ronald J Williams. Simple statistical gradient-following algorithms for connectionist reinforcement learning. Machine learning, 8(3-4):229–256, 1992. find
  56. Lin Xu, Frank Hutter, Holger H Hoos, and Kevin Leyton-Brown. Satzilla: portfolio-based algorithm selection for sat. Journal of artificial intelligence research, 32:565–606, 2008. find
  57. Zhanfu Yang, Fei Wang, Ziliang Chen, Guannan Wei, and Tiark Rompf. Graph neural reasoning for 2-quantified boolean formula solvers. arXiv preprint arXiv:1904.12084, 2019. — [arXiv:1904.12084](https://arxiv.org/abs/1904.12084) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/lederman-2018-learning-heuristics-quantified-boolean-formulas/