Document Open Access Logo

Learning Unified Graph and Language Representations for SMT Algorithm Selection

Authors Zhengyang Lu , Paul Sarnighausen-Cahn , Jiahao Chen , Arie Gurfinkel , Florin Manea , Vijay Ganesh

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.41.pdf
  • Filesize: 0.9 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Logic and verification
  • Computing methodologies → Machine learning approaches
Keywords
  • satisfiability modulo theories
  • algorithm selection
  • multimodal learning
  • neuro-symbolic AI

Metrics

Abstract

Algorithm selection is important in satisfiability and constraint solving, since no single solver performs best across all instances. Traditional learning-based approaches represent problem instances using expert-designed features to predict solver performance, while recent work explores graph representations derived from ASTs. However, most existing approaches overlook high-level contextual information, such as the application domain or the benchmark origin. In practice, such cues often help practitioners choose an appropriate solver.
We present SMT-Select, a multimodal framework for SMT algorithm selection. It learns graph representations from formula ASTs and textual representations from natural-language context descriptions. These representations are then combined to guide solver selection. Evaluated across nine SMT logics, SMT-Select consistently outperforms existing selectors and SMT-COMP winning solvers. Across all evaluated logics, it closes at least 30% of the performance gap between the competition winner and the virtual best solver (VBS), and nearly matches the VBS in two logics.

Cite As Get BibTex

Zhengyang Lu, Paul Sarnighausen-Cahn, Jiahao Chen, Arie Gurfinkel, Florin Manea, and Vijay Ganesh. Learning Unified Graph and Language Representations for SMT Algorithm Selection. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 41:1-41:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.41

Author Details

Zhengyang Lu
  • University of Waterloo, Canada
Paul Sarnighausen-Cahn
  • University of Göttingen and CIDAS, Göttingen, Germany
Jiahao Chen
  • Georgia Institute of Technology, Atlanta, GA, USA
Arie Gurfinkel
  • University of Waterloo, Canada
Florin Manea
  • University of Göttingen and CIDAS, Göttingen, Germany
Vijay Ganesh
  • Georgia Institute of Technology, Atlanta, GA, USA

Funding

Florin Manea and Paul Sarnighausen-Cahn are supported by the German Research Foundation (DFG) through the Heisenberg project 466789228 and research project 562495345.
  • Lu, Zhengyang: NSERC Canada Graduate Scholarship - Doctoral (CGS-D)

Acknowledgements

We thank Po-Chun Chien and Nian-Ze Lee for their help in checking the correctness of our enriched natural language descriptions for the SV-COMP benchmarks.

Supplementary Materials

References

  1. Roberto Amadini, Maurizio Gabbrielli, and Jacopo Mauro. SUNNY: a lazy portfolio approach for constraint solving. Theory Pract. Log. Program., 14(4-5):509-524, 2014. URL: https://doi.org/10.1017/S1471068414000179.
  2. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016. Google Scholar
  3. Clark W. Barrett, Leonardo Mendonça de Moura, and Aaron Stump. SMT-COMP: satisfiability modulo theories competition. In Computer Aided Verification, 17th International Conference, CAV 2005, volume 3576 of Lecture Notes in Computer Science, pages 20-23. Springer, 2005. URL: https://doi.org/10.1007/11513988_4.
  4. Dirk Beyer. Automatic verification of C and Java programs: SV-COMP 2019. In Tools and Algorithms for the Construction and Analysis of Systems, pages 133-155. Springer International Publishing, 2019. URL: https://doi.org/10.1007/978-3-030-17502-3_9.
  5. Dirk Beyer. Competition on software verification and witness validation: SV-COMP 2023. In Tools and Algorithms for the Construction and Analysis of Systems, pages 495-522. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_29.
  6. Miquel Bofill, Joan Espasa, and Mateu Villaret. Relaxed exists-step plans in planning as SMT. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, pages 563-570, 2017. URL: https://doi.org/10.24963/ijcai.2017/79.
  7. Derek Bridge, Eoin O'Mahony, and Barry O'Sullivan. Case-Based Reasoning for Autonomous Constraint Solving, pages 73-95. Springer Berlin Heidelberg, Berlin, Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-21434-9_4.
  8. Martin Bromberger, François Bobot, and Martin Jonáš. SMT-COMP 2024. https://smt-comp.github.io/2024/, 2024. Accessed: 2025-12-22. Google Scholar
  9. Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI'08, pages 209-224, 2008. URL: http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf.
  10. Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. EXE: Automatically generating inputs of death. ACM Trans. Inf. Syst. Secur., 12(2), December 2008. URL: https://doi.org/10.1145/1455518.1455522.
  11. Michael Cashmore, Daniele Magazzeni, and Parisa Zehtabi. Planning for hybrid systems via Satisfiability Modulo Theories. Journal of Artificial Intelligence Research, 67:235-283, February 2020. URL: https://doi.org/10.1613/jair.1.11751.
  12. Leonardo De Moura and Nikolaj Bjørner. Satisfiability modulo theories: introduction and applications. Communications of the ACM, 54(9):69-77, 2011. URL: https://doi.org/10.1145/1995376.1995394.
  13. Leonardo de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In 2008 Tools and Algorithms for Construction and Analysis of Systems, pages 337-340. Springer, Berlin, Heidelberg, March 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  14. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: pre-training of deep bidirectional transformers for language understanding. CoRR, abs/1810.04805, 2018. URL: https://doi.org/10.48550/arXiv.1810.04805.
  15. Alan M. Frisch, Warwick Harvey, Christopher Jefferson, Bernadette Martínez Hernández, and Ian Miguel. Essence : A constraint language for specifying combinatorial problems. Constraints An Int. J., 13(3):268-306, 2008. URL: https://doi.org/10.1007/S10601-008-9047-Y.
  16. Marco Gario and Andrea Micheli. PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In SMT Workshop 2015, 2015. Google Scholar
  17. Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. The SeaHorn verification framework. In Computer Aided Verification, pages 343-361, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-21690-4_20.
  18. Will Hamilton, Zhitao Ying, and Jure Leskovec. Inductive representation learning on large graphs. In Advances in Neural Information Processing Systems, volume 30, 2017. URL: https://proceedings.neurips.cc/paper_files/paper/2017/file/5dd9db5e033da9c6fb5ba83c7a7ebea9-Paper.pdf.
  19. Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, and Andreas Podelski. Ultimate Automizer and the search for perfect interpolants. In Tools and Algorithms for the Construction and Analysis of Systems, pages 447-451. Springer International Publishing, 2018. URL: https://doi.org/10.1007/978-3-319-89963-3_30.
  20. Jan Hůla, David Mojžíšek, and Mikoláš Janota. Graph neural networks for scheduling of SMT solvers. In 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI), pages 447-451, 2021. URL: https://doi.org/10.1109/ICTAI52525.2021.00072.
  21. Haniye Kashgarani and Lars Kotthoff. Automatic parallel portfolio selection. In ECAI 2023 - 26th European Conference on Artificial Intelligence, volume 372 of Frontiers in Artificial Intelligence and Applications, pages 1215-1222. IOS Press, 2023. URL: https://doi.org/10.3233/FAIA230398.
  22. Pascal Kerschke, Holger H. Hoos, Frank Neumann, and Heike Trautmann. Automated algorithm selection: Survey and perspectives. Evol. Comput., 27(1):3-45, March 2019. URL: https://doi.org/10.1162/evco_a_00242.
  23. Thomas N. Kipf and Max Welling. Semi-supervised classification with graph convolutional networks. In 5th International Conference on Learning Representations, ICLR 2017. OpenReview.net, 2017. URL: https://openreview.net/forum?id=SJU4ayYgl.
  24. Lars Kotthoff. Algorithm selection for combinatorial search problems: A survey. AI Mag., 35(3):48-60, September 2014. URL: https://doi.org/10.1609/aimag.v35i3.2460.
  25. Daniel Kroening and Ofer Strichman. Decision Procedures - An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-50497-0.
  26. Mitja Kulczynski, Kevin Lotz, Florin Manea, Danny Bøgsted Poulsen, and Paul Sarnighausen-Cahn. SMTQuery: Analysing SMT-LIB string benchmarks. In Formal Methods: Foundations and Applications, pages 22-34, Cham, 2025. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-78116-2_2.
  27. Erdem Kus, Özgür Akgün, Nguyen Dang, and Ian Miguel. Frugal algorithm selection (short paper). In 30th International Conference on Principles and Practice of Constraint Programming, CP 2024, volume 307 of LIPIcs, pages 38:1-38:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CP.2024.38.
  28. Will Leeson and Matthew B. Dwyer. Algorithm selection for software verification using graph neural networks. ACM Trans. Softw. Eng. Methodol., 33(3), March 2024. URL: https://doi.org/10.1145/3637225.
  29. Will Leeson, Matthew B Dwyer, and Antonio Filieri. Sibyl: Improving software engineering tools with SMT selection. In Proceedings of the 45th International Conference on Software Engineering, pages 2185-2197. IEEE Press, 2023. URL: https://doi.org/10.1109/ICSE48619.2023.00184.
  30. Zhengyang Lu. AlphaSMT: A reinforcement learning guided SMT solver. Master’s thesis, University of Waterloo, 2023. Google Scholar
  31. Zhengyang Lu, Po-Chun Chien, Nian-Ze Lee, Arie Gurfinkel, and Vijay Ganesh. Btor2-Select: machine learning based algorithm selection for hardware model checking. In Computer Aided Verification, pages 296-311, Cham, 2025. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-98668-0_15.
  32. Zhengyang Lu, Paul Sarnighausen-Cahn, Jiahao Chen, Arie Gurfinkel, Florin Manea, and Vijay Ganesh. Learning SMT algorithm selection with high-level natural-language descriptions. In Foundations of Information and Knowledge Systems - Poster Track, pages 353-358, Cham, 2026. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-032-21540-6_23.
  33. Zhengyang Lu, Stefan Siemer, Piyush Jha, Joel Day, Florin Manea, and Vijay Ganesh. Layered and staged Monte Carlo Tree Search for SMT strategy synthesis. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24, pages 1907-1915, 2024. URL: https://doi.org/10.24963/ijcai.2024/211.
  34. Zhengyang John Lu, Joel Day, Piyush Jha, Paul Sarnighausen-Cahn, Stefan Siemer, Florin Manea, and Vijay Ganesh. Novel tree-search method for synthesizing SMT strategies. Acta Informatica, 62(3):28, 2025. URL: https://doi.org/10.1007/s00236-025-00495-x.
  35. Chuan Luo, Shaoke Cui, Jianping Song, Xindi Zhang, Wei Wu, Chanjuan Liu, Shaowei Cai, and Chunming Hu. SMTgazer: Learning to schedule SMT algorithms via Bayesian optimization. In 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 1273-1285, 2025. URL: https://doi.org/10.1109/ASE63991.2025.00109.
  36. Alessio Pellegrino, Özgür Akgün, Nguyen Dang, Zeynep Kiziltan, and Ian Miguel. Transformer-Based Feature Learning for Algorithm Selection in Combinatorial Optimisation. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025), volume 340 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:22, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CP.2025.31.
  37. Nikhil Pimpalkhare, Federico Mora, Elizabeth Polgreen, and Sanjit A. Seshia. MedleySolver: Online SMT algorithm selection. In Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 453-470. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_31.
  38. Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, and Sanjit A. Seshia. UCLID5: Multi-modal formal modeling, verification, and synthesis. In Computer Aided Verification: 34th International Conference, CAV 2022, pages 538-551, Berlin, Heidelberg, 2022. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-13185-1_27.
  39. Nils Reimers and Iryna Gurevych. Sentence-BERT: Sentence embeddings using Siamese BERT-Networks. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing. Association for Computational Linguistics, November 2019. URL: https://doi.org/10.48550/arXiv.1908.10084.
  40. John R. Rice. The algorithm selection problem. Adv. Comput., 15:65-118, 1976. URL: https://doi.org/10.1016/S0065-2458(08)60520-3.
  41. Cedric Richter, Eyke Hüllermeier, Marie-Christine Jakobs, and Heike Wehrheim. Algorithm selection for software validation based on graph kernels. Automated Software Engg., 27(1–2):153-186, June 2020. URL: https://doi.org/10.1007/s10515-020-00270-x.
  42. Cedric Richter and Heike Wehrheim. Attend and represent: a novel view on algorithm selection for software verification. In Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, ASE '20, pages 1016-1028, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3324884.3416633.
  43. Hans-Jörg Schurr and François Bobot. Klammerhammer. https://github.com/SMT-LIB/SMT-LIB-db/tree/main/klhm, 2025. Accessed: 2026-02-26.
  44. Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Clark Barrett, Pascal Fontaine, and Cesare Tinelli. Exploring the SMT-LIB benchmark library. In Tools and Algorithms for the Construction and Analysis of Systems, pages 150-169, Cham, 2026. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-032-22752-2_8.
  45. Hans-Jörg Schurr, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine, and Cesare Tinelli. SMT-LIB catalog 2025 (version 1), July 2025. Accessed on 2025-12-16. URL: https://doi.org/10.5281/zenodo.16290040.
  46. Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, and Vijay Ganesh. MachSMT: A machine learning-based algorithm selector for SMT solvers. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, volume 12652 of Lecture Notes in Computer Science, pages 303-325, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_16.
  47. Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, and Vijay Ganesh. Algorithm selection for SMT. Int. J. Softw. Tools Technol. Transf., 25(2):219-239, 2023. URL: https://doi.org/10.1007/S10009-023-00696-0.
  48. Alexander Tornede, Marcel Wever, and Eyke Hüllermeier. Extreme algorithm selection with dyadic feature representation. In Discovery Science, pages 309-324, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-61527-7_21.
  49. Sentence Transformers. all-mpnet-base-v2, 2021. URL: https://huggingface.co/sentence-transformers/all-mpnet-base-v2.
  50. Lewis Tunstall, Nils Reimers, Unso Eun Seo Jo, Luke Bates, Daniel Korat, Moshe Wasserblat, and Oren Pereg. Efficient few-shot learning without prompts, 2022. URL: https://doi.org/10.48550/arXiv.2209.11055.
  51. Felix Ulrich-Oltean, Peter Nightingale, and James Alfred Walker. Learning to select SAT encodings for pseudo-boolean and linear integer constraints. Constraints An Int. J., 28(3):397-426, November 2023. URL: https://doi.org/10.1007/s10601-023-09364-1.
  52. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in Neural Information Processing Systems, volume 30. Curran Associates, Inc., 2017. URL: https://proceedings.neurips.cc/paper_files/paper/2017/file/3f5ee243547dee91fbd053c1c4a845aa-Paper.pdf.
  53. Petar Veličković, Guillem Cucurull, Arantxa Casanova, Adriana Romero, Pietro Liò, and Yoshua Bengio. Graph attention networks. In International Conference on Learning Representations, 2018. URL: https://openreview.net/forum?id=rJXMpikCZ.
  54. Boris Weisfeiler and A. A. Lehman. A reduction of a graph to a canonical form and an algebra arising during this reduction. Nauchno-Technicheskaya Informatsiya, 2(9):12-16, 1968. Google Scholar
  55. Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura. A concurrent portfolio approach to SMT solving. In Computer Aided Verification, pages 715-720, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-02658-4_60.
  56. Xingyu Wu, Yan Zhong, Jibin Wu, Bingbing Jiang, and Kay Chen Tan. Large language model-enhanced algorithm selection: Towards comprehensive algorithm representation. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24, pages 5235-5244. International Joint Conferences on Artificial Intelligence Organization, 2024. URL: https://doi.org/10.24963/ijcai.2024/579.
  57. Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful are graph neural networks? In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL: https://openreview.net/forum?id=ryGs6iA5Km.
  58. L. Xu, F. Hutter, H. H. Hoos, and K. Leyton-Brown. Evaluating component solver contributions to portfolio-based algorithm selectors. In Proc. SAT, LNCS 7317, pages 228-241. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_18.
  59. Lin Xu, Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. SATzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res., 32:565-606, 2008. URL: https://doi.org/10.1613/jair.2490.
  60. Rex Ying, Jiaxuan You, Christopher Morris, Xiang Ren, William L. Hamilton, and Jure Leskovec. Hierarchical graph representation learning with differentiable pooling. In Proceedings of the 32nd International Conference on Neural Information Processing Systems, NIPS'18, pages 4805-4815, Red Hook, NY, USA, 2018. Curran Associates Inc. URL: https://proceedings.neurips.cc/paper/2018/hash/e77dbaf6759253c7c6d0efc5690369c7-Abstract.html.
  61. Yanzhao Zhang, Mingxin Li, Dingkun Long, Xin Zhang, Huan Lin, Baosong Yang, Pengjun Xie, An Yang, Dayiheng Liu, Junyang Lin, Fei Huang, and Jingren Zhou. Qwen3 embedding: Advancing text embedding and reranking through foundation models. arXiv preprint arXiv:2506.05176, 2025. URL: https://doi.org/10.48550/arXiv.2506.05176.
  62. Zhanguang Zhang, Didier Chételat, Joseph Cotnareanu, Amur Ghose, Wenyi Xiao, Hui-Ling Zhen, Yingxue Zhang, Jianye Hao, Mark Coates, and Mingxuan Yuan. GraSS: Combining graph neural networks with expert knowledge for SAT solver selection. In Proceedings of the 30th ACM SIGKDD Conference on Knowledge Discovery and Data Mining, KDD 2024, pages 6301-6311. ACM, 2024. URL: https://doi.org/10.1145/3637528.3671627.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact