这是indexloc提供的服务，不要输入任何密码
Skip to main content
Springer Nature Link
Log in

Algorithm selection for SMT

MachSMT: machine learning driven algorithm selection for SMT solvers

  • General
  • Special Issue: TACAS 2021
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

A Publisher Correction to this article was published on 14 August 2023

This article has been updated

Abstract

This paper presents MachSMT, an algorithm selection tool for Satisfiability Modulo Theories (SMT) solvers. MachSMT supports the entirety of the SMT-LIB language and standardized SMT-LIB theories, and is easy to extend with support for new theories. MachSMT deploys machine learning methods to construct both empirical hardness models and pairwise ranking comparators over state-of-the-art SMT solvers. Given an input formula in SMT-LIB format, MachSMT leverages these learnt models to output a ranking of solvers based on predicted runtimes. We provide an extensive empirical evaluation of MachSMT to demonstrate the efficiency and efficacy of MachSMT over three broad usage scenarios on theories and theory combinations of practical relevance (e.g., bit-vectors, (non)linear integer and real arithmetic, arrays, and floating-point arithmetic). First, we deploy MachSMT on state-of-the-art solvers in SMT-COMP 2019 and 2020. We observe MachSMT frequently improves on the best performing solvers in the competition, winning \(57\) divisions outright, with up to a \(99.4\)% improvement in PAR-2 score. Second, we evaluate MachSMT to select configurations from a single underlying solver. We observe that MachSMT solves \(898\) more benchmarks and up to a \(93.4\%\) improvement in PAR-2 score across 23 configurations of the SMT solver cvc5. Last, we evaluate MachSMT on domain-specific problems, namely network verification with simple domain-specific features, and observe an improvement of \(77.3\%\) in PAR-2  score.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+
from $39.99 /Month
  • Starting from 10 chapters or articles per month
  • Access and download chapters and articles from more than 300k books and 2,500 journals
  • Cancel anytime
View plans

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Explore related subjects

Discover the latest articles, books and news in related subjects, suggested using machine learning.

Change history

Notes

  1. \(\frac{x - \mu }{\sigma }\), where x is a feature sample, \(\mu \) is the mean across the specific feature on the training set, and \(\sigma \) is the deviation across the specific feature on the training set.

  2. https://github.com/cvc5/cvc5/blob/master/contrib/competitions/smt-comp/run-script-smtcomp2021

  3. sklearn.linear_model.RidgeCV

References

  1. Niemetz, A., Preiner, M.: Bitwuzla at the SMT-COMP 2020. CoRR abs/2006.01621 (2020). https://arxiv.org/abs/2006.01621

  2. Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0. J. Satisf. Boolean Model. Comput. 9(1), 53–58 (2014). https://doi.org/10.3233/sat190101

    Article  Google Scholar 

  3. Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: G. Gopalakrishnan, S. Qadeer (eds.) Computer Aided Verification—23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6806, pp. 171–177. Springer (2011). https://doi.org/10.1007/978-3-642-22110-1_14

  4. Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: D. Fisman, G. Rosu (eds.) Tools and Algorithms for the Construction and Analysis of Systems—28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, Lecture Notes in Computer Science, vol. 13243, pp. 415–442. Springer (2022). https://doi.org/10.1007/978-3-030-99524-9_24

  5. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 SMT solver. In: N. Piterman, S.A. Smolka (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7795, pp. 93–107. Springer (2013). https://doi.org/10.1007/978-3-642-36742-7_7

  6. Christ, J., Hoenicke, J., Nutz, A.: Smtinterpol: An interpolating SMT solver. In: A.F. Donaldson, D. Parker (eds.) Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7385, pp. 248–254. Springer (2012). https://doi.org/10.1007/978-3-642-31759-0_19. https://doi.org/10.1007/978-3-642-31759-0_19

  7. Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: W. Damm, H. Hermanns (eds.) Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4590, pp. 519–531. Springer (2007). https://doi.org/10.1007/978-3-540-73368-3_52

  8. Dutertre, B.: Yices 2.2. In: A. Biere, R. Bloem (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8559, pp. 737–744. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_49

  9. de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: C.R. Ramakrishnan, J. Rehof (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008). https://doi.org/10.1007/978-3-540-78800-3_24

  10. Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. 12(2), 10:1-10:38 (2008). https://doi.org/10.1145/1455518.1455522

    Article  Google Scholar 

  11. Pasareanu, C.S., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. Int. J. Softw. Tools Technol. Transf. 11(4), 339–353 (2009). https://doi.org/10.1007/s10009-009-0118-1

    Article  Google Scholar 

  12. Gadelha, M.Y.R., Monteiro, F.R., Cordeiro, L.C., Nicole, D.A.: ESBMC v6.0: Verifying C programs using k-induction and invariant inference—(competition contribution). In: D. Beyer, M. Huisman, F. Kordon, B. Steffen (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, Lecture Notes in Computer Science, vol. 11429, pp. 209–213. Springer (2019). https://doi.org/10.1007/978-3-030-17502-3_15

  13. Brain, M., Schanda, F., Sun, Y.: Building better bit-blasting for floating-point problems. In: T. Vojnar, L. Zhang (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, Lecture Notes in Computer Science, vol. 11427, pp. 79–98. Springer (2019). https://doi.org/10.1007/978-3-030-17462-0_5

  14. Goues, C.L., Leino, K.R.M., Moskal, M.: The boogie verification debugger (tool paper). In: G. Barthe, A. Pardo, G. Schneider (eds.) Software Engineering and Formal Methods—9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings, Lecture Notes in Computer Science, vol. 7041, pp. 407–414. Springer (2011). https://doi.org/10.1007/978-3-642-24690-6_28

  15. Leino, K.R.M.: Automating theorem proving with SMT. In: S. Blazy, C. Paulin-Mohring, D. Pichardie (eds.) Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7998, pp. 2–16. Springer (2013). https://doi.org/10.1007/978-3-642-39634-2_2

  16. Rintanen, J.: Madagascar: Scalable planning with sat. Proceedings of the 8th International Planning Competition (IPC-2014) 21 (2014)

  17. Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: R. Majumdar, V. Kuncak (eds.) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, Lecture Notes in Computer Science, vol. 10426, pp. 97–117. Springer (2017). https://doi.org/10.1007/978-3-319-63387-9_5

  18. Guidotti, D., Barrett, C., Katz, G., Pulina, L., Narodyska, N., Tacchella, A.: The VNN-LIB standard. http://www.vnnlib.org/wp-content/uploads/2020/07/main-1.pdf

  19. Godefroid, P., Levin, M.Y., Molnar, D.A.: SAGE: whitebox fuzzing for security testing. Commun. ACM 55(3), 40–44 (2012). https://doi.org/10.1145/2093548.2093564

    Article  Google Scholar 

  20. Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K.S., Rungta, N., Tkachuk, O., Varming, C.: Semantic-based automated reasoning for AWS access policies using SMT. In: N. Bjørner, A. Gurfinkel (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30–November 2, 2018, pp. 1–9. IEEE (2018). https://doi.org/10.23919/FMCAD.2018.8602994

  21. Bhargavan, K., Bond, B., Delignat-Lavaud, A., Fournet, C., Hawblitzel, C., Hritcu, C., Ishtiaq, S., Kohlweiss, M., Leino, R., Lorch, J.R., Maillard, K., Pan, J., Parno, B., Protzenko, J., Ramananandro, T., Rane, A., Rastogi, A., Swamy, N., Thompson, L., Wang, P., Béguelin, S.Z., Zinzindohoue, J.K.: Everest: Towards a verified, drop-in replacement of HTTPS. In: B.S. Lerner, R. Bodík, S. Krishnamurthi (eds.) 2nd Summit on Advances in Programming Languages, SNAPL 2017, May 7-10, 2017, Asilomar, CA, USA, LIPIcs, vol. 71, pp. 1:1–1:12. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2017). https://doi.org/10.4230/LIPIcs.SNAPL.2017.1

  22. Hadarean, L., Hyvärinen, A., Niemetz, A., Reger, G.: Smt-comp 2019. https://www.smt-comp.org/2019 (2019)

  23. Weber, T., Conchon, S., Déharbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015–2018. J. Satisf. Boolean Model. Comput. 11(1), 221–259 (2019). https://doi.org/10.3233/SAT190123

    Article  MathSciNet  Google Scholar 

  24. Brain, M., Schanda, F., Sun, Y.: Building better bit-blasting for floating-point problems. In: T. Vojnar, L. Zhang (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, Lecture Notes in Computer Science, vol. 11427, pp. 79–98. Springer (2019). https://doi.org/10.1007/978-3-030-17462-0_5

  25. Brain, M., D’Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods Syst. Des. 45(2), 213–245 (2014). https://doi.org/10.1007/s10703-013-0203-7

    Article  MATH  Google Scholar 

  26. Salvia, R., Titolo, L., Feliú, M.A., Moscato, M.M., Muñoz, C.A., Rakamaric, Z.: A mixed real and floating-point solver. In: J.M. Badger, K.Y. Rozier (eds.) NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11460, pp. 363–370. Springer (2019). https://doi.org/10.1007/978-3-030-20652-9_25

  27. Fu, Z., Su, Z.: Xsat: A fast floating-point satisfiability solver. In: S. Chaudhuri, A. Farzan (eds.) Computer Aided Verification—28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, Lecture Notes in Computer Science, vol. 9780, pp. 187–209. Springer (2016). https://doi.org/10.1007/978-3-319-41540-6_11

  28. Ben Khadra, M.A., Stoffel, D., Kunz, W.: gosat: Floating-point satisfiability as global optimization. In: D. Stewart, G. Weissenbacher (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017, pp. 11–14. IEEE (2017). https://doi.org/10.23919/FMCAD.2017.8102235

  29. Scott, J., Panju, M., Ganesh, V.: LGML: logic guided machine learning (student abstract). In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pp. 13909–13910. AAAI Press (2020). https://aaai.org/ojs/index.php/AAAI/article/view/7227

  30. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: A. Gupta, D. Kroening (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK) (2010)

  31. Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2020)

  32. Pedregosa, F., Varoquaux, G., Gramfort, A., Michel, V., Thirion, B., Grisel, O., Blondel, M., Prettenhofer, P., Weiss, R., Dubourg, V., Vanderplas, J., Passos, A., Cournapeau, D., Brucher, M., Perrot, M., Duchesnay, E.: Scikit-learn: machine learning in Python. J. Mach. Learn. Res. 12, 2825–2830 (2011)

    MathSciNet  MATH  Google Scholar 

  33. Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., Killeen, T., Lin, Z., Gimelshein, N., Antiga, L., et al.: Pytorch: an imperative style, high-performance deep learning library. Adv. Neural Inf. Process. Syst. 32, 8026–8037 (2019)

    Google Scholar 

  34. Pulina, L., Tacchella, A.: A multi-engine solver for quantified boolean formulas. In: C. Bessiere (ed.) Principles and Practice of Constraint Programming—CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4741, pp. 574–589. Springer (2007). https://doi.org/10.1007/978-3-540-74970-7_41

  35. Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla-07: The design and analysis of an algorithm portfolio for SAT. In: C. Bessiere (ed.) Principles and Practice of Constraint Programming - CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4741, pp. 712–727. Springer (2007). https://doi.org/10.1007/978-3-540-74970-7_50

  36. Scott, J., Poupart, P., Ganesh, V.: An algorithm selection approach for QF_FP solvers. In: 17th International Workshop on Satisfiability Modulo Theories (2019)

  37. Balunovic, M., Bielik, P., Vechev, M.T.: Learning to solve SMT formulas. In: S. Bengio, H.M. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, R. Garnett (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, pp. 10338–10349 (2018). http://papers.nips.cc/paper/8233-learning-to-solve-smt-formulas

  38. Wen, S.H., Mow, W.L., Chen, W.N., Wang, C.Y., Hsiao, H.C.: Enhancing symbolic execution by machine learning based solver selection (2019). https://doi.org/10.14722/bar.2019.23080

  39. MachSMT GitHub repository. https://github.com/machsmt/machsmt (2022)

  40. Scott, J., Niemetz, A., Preiner, M., Nejati, S., Ganesh, V.: Machsmt: A machine learning-based algorithm selector for SMT solvers. In: J.F. Groote, K.G. Larsen (eds.) Tools and Algorithms for the Construction and Analysis of Systems—27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, Lecture Notes in Computer Science, vol. 12652, pp. 303–325. Springer (2021). https://doi.org/10.1007/978-3-030-72013-1_16. https://doi.org/10.1007/978-3-030-72013-1_16

  41. Barrett, C., Stump, A., Tinelli, C., et al.: The smt-lib standard: Version 2.0. In: Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England), vol. 13, p. 14 (2010)

  42. Rice, J.R.: The algorithm selection problem. Adv. Comput. 15, 65–118 (1976). https://doi.org/10.1016/S0065-2458(08)60520-3

    Article  Google Scholar 

  43. 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

    Article  MATH  Google Scholar 

  44. Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Evaluating component solver contributions to portfolio-based algorithm selectors. In: A. Cimatti, R. Sebastiani (eds.) Theory and Applications of Satisfiability Testing—SAT 2012—15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7317, pp. 228–241. Springer (2012). https://doi.org/10.1007/978-3-642-31612-8_18

  45. Freund, Y., Schapire, R., Abe, N.: A short introduction to boosting. J. Jpn. Soc. Artif. Intel. 14(771–780), 1612 (1999)

    Google Scholar 

  46. Li, X., Wang, L., Sung, E.: A study of adaboost with svm based weak learners. In: Proceedings. 2005 IEEE International Joint Conference on Neural Networks, 2005., vol. 1, pp. 196–201. IEEE (2005)

  47. Drucker, H.: Improving regressors using boosting techniques. In: D.H. Fisher (ed.) Proceedings of the Fourteenth International Conference on Machine Learning (ICML 1997), Nashville, Tennessee, USA, July 8-12, 1997, pp. 107–115. Morgan Kaufmann (1997)

  48. LeCun, Y., Bengio, Y., Hinton, G.: Deep learning. Nature 521(7553), 436–444 (2015)

    Article  Google Scholar 

  49. Goodfellow, I., Bengio, Y., Courville, A.: Deep learning. MIT press (2016)

  50. Greenland, S., Mansournia, M.A., Altman, D.G.: Sparse data bias: a problem hiding in plain sight. bmj 352, i1981 (2016). https://doi.org/10.1136/bmj.i1981

    Article  Google Scholar 

  51. Weston, J., Mukherjee, S., Chapelle, O., Pontil, M., Poggio, T.A., Vapnik, V.: Feature selection for svms. In: T.K. Leen, T.G. Dietterich, V. Tresp (eds.) Advances in Neural Information Processing Systems 13, Papers from Neural Information Processing Systems (NIPS) 2000, Denver, CO, USA, pp. 668–674. MIT Press (2000). https://proceedings.neurips.cc/paper/2000/hash/8c3039bd5842dca3d944faab91447818-Abstract.html

  52. Kira, K., Rendell, L.A.: A practical approach to feature selection. In: D.H. Sleeman, P. Edwards (eds.) Proceedings of the Ninth International Workshop on Machine Learning (ML 1992), Aberdeen, Scotland, UK, July 1-3, 1992, pp. 249–256. Morgan Kaufmann (1992). https://doi.org/10.1016/b978-1-55860-247-2.50037-1

  53. Rodríguez, J.D., Martínez, A.P., Lozano, J.A.: Sensitivity analysis of k-fold cross validation in prediction error estimation. IEEE Trans. Pattern Anal. Mach. Intell. 32(3), 569–575 (2010). https://doi.org/10.1109/TPAMI.2009.187

    Article  Google Scholar 

  54. Moore, A.W.: Cross-validation for detecting and preventing overfitting. School of Computer Science Carneigie Mellon University (2001)

  55. Wold, S., Esbensen, K., Geladi, P.: Principal component analysis. Chemom. Intel. Lab. Syst. 2(1–3), 37–52 (1987)

    Article  Google Scholar 

  56. Van Der Maaten, L., Postma, E., Van den Herik, J.: Dimensionality reduction: a comparative. J. Mach. Learn. Res. 10(66–71), 13 (2009)

    Google Scholar 

  57. Grira, N., Crucianu, M., Boujemaa, N.: Unsupervised and semi-supervised clustering: a brief survey. Rev. Mach. Learn. Techn. Process. Multimed. Content 1, 9–16 (2004)

    MATH  Google Scholar 

  58. Xu, R., II, Wunsch, D.: Survey of clustering algorithms. IEEE Trans. Neural Netw. 16(3), 645–678 (2005). https://doi.org/10.1109/TNN.2005.845141. https://doi.org/10.1109/TNN.2005.845141

  59. Kwon, D., Kim, H., Kim, J., Suh, S.C., Kim, I., Kim, K.J.: A survey of deep learning-based network anomaly detection. Clust. Comput. 22(Suppl 1), 949–961 (2019). https://doi.org/10.1007/s10586-017-1117-8

    Article  Google Scholar 

  60. Agrawal, S., Agrawal, J.: Survey on anomaly detection using data mining techniques. Procedia Comput. Sci. 60, 708–713 (2015). https://doi.org/10.1016/j.procs.2015.08.220

    Article  Google Scholar 

  61. Halko, N., Martinsson, P., Tropp, J.A.: Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions. SIAM Rev. 53(2), 217–288 (2011). https://doi.org/10.1137/090771806

    Article  MathSciNet  MATH  Google Scholar 

  62. Xu, L., Hutter, F., Shen, J., Hoos, H.H., Leyton-Brown, K.: Satzilla2012: Improved algorithm selection based on cost-sensitive classification models. Proceedings of SAT Challenge pp. 57–58 (2012)

  63. Harris, C.R., Millman, K.J., van der Walt, S.J., Gommers, R., Virtanen, P., Cournapeau, D., Wieser, E., Taylor, J., Berg, S., Smith, N.J., et al.: Array programming with numpy. Nature 585(7825), 357–362 (2020)

    Article  Google Scholar 

  64. Chen, T., Guestrin, C.: XGBoost: A scalable tree boosting system. In: Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD ’16, pp. 785–794. ACM, New York, NY, USA (2016). https://doi.org/10.1145/2939672.2939785. http://doi.acm.org/10.1145/2939672.2939785

  65. Barbosa, H., Hyvärinen, A., Hoenecke, J.: Smt-comp 2020. https://www.smt-comp.org/2020 (2020)

  66. Stump, A., Sutcliffe, G., Tinelli, C.: Starexec: A cross-community infrastructure for logic solving. In: S. Demri, D. Kapur, C. Weidenbach (eds.) Automated Reasoning—7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8562, pp. 367–373. Springer (2014). https://doi.org/10.1007/978-3-319-08587-6_28

  67. Marijn Heule Matti Järvisalo, M.S.: Sat race 2019 (2019). http://sat-race-2019.ciirc.cvut.cz/

  68. Nötzli, A., Reynolds, A., Barbosa, H., Niemetz, A., Preiner, M., Barrett, C.W., Tinelli, C.: Syntax-guided rewrite rule enumeration for SMT solvers. In: M. Janota, I. Lynce (eds.) Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11628, pp. 279–297. Springer (2019). https://doi.org/10.1007/978-3-030-24258-9_20. https://doi.org/10.1007/978-3-030-24258-9_20

  69. Jayaraman, K., Bjørner, N., Outhred, G., Kaufman, C.: Automated analysis and debugging of network connectivity policies. Microsoft Research pp. 1–11 (2014)

  70. Baldwin, S.: Compute canada: advancing computational research. In: Journal of Physics: Conference Series, vol. 341, p. 012001. IOP Publishing (2012)

  71. Lundberg, S.M., Lee, S.I.: A unified approach to interpreting model predictions. In: I. Guyon, U.V. Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, R. Garnett (eds.) Advances in Neural Information Processing Systems 30, pp. 4765–4774. Curran Associates, Inc. (2017). http://papers.nips.cc/paper/7062-a-unified-approach-to-interpreting-model-predictions.pdf

  72. Ali, S., Smith, K.A.: On learning algorithm selection for classification. Appl. Soft Comput. 6(2), 119–138 (2006). https://doi.org/10.1016/j.asoc.2004.12.002

    Article  Google Scholar 

  73. Kotthoff, L.: Algorithm selection for combinatorial search problems: A survey. In: C. Bessiere, L.D. Raedt, L. Kotthoff, S. Nijssen, B. O’Sullivan, D. Pedreschi (eds.) Data Mining and Constraint Programming - Foundations of a Cross-Disciplinary Approach, Lecture Notes in Computer Science, vol. 10101, pp. 149–190. Springer (2016). https://doi.org/10.1007/978-3-319-50137-6_7

  74. Tierney, K., Malitsky, Y.: An algorithm selection benchmark of the container pre-marshalling problem. In: C. Dhaenens, L. Jourdan, M. Marmion (eds.) Learning and Intelligent Optimization - 9th International Conference, LION 9, Lille, France, January 12-15, 2015. Revised Selected Papers, Lecture Notes in Computer Science, vol. 8994, pp. 17–22. Springer (2015). https://doi.org/10.1007/978-3-319-19084-6_2

  75. Vallati, M., Chrpa, L., Kitchin, D.E.: Portfolio-based planning: state of the art, common practice and open challenges. AI Commun. 28(4), 717–733 (2015). https://doi.org/10.3233/AIC-150671

    Article  MathSciNet  Google Scholar 

  76. O’Mahony, E., Hebrard, E., Holland, A., Nugent, C., O’Sullivan, B.: Using Case-based Reasoning in an Algorithm Portfolio for Constraint Solving. In: Irish conference on artificial intelligence and cognitive science, pp. 210–216 (2008). https://homepages.laas.fr/ehebrard/papers/aics2008.pdf

  77. Malitsky, Y.: Evolving instance-specific algorithm configuration. In: Instance-Specific Algorithm Configuration, pp. 93–105. Springer (2014). https://doi.org/10.1007/978-3-319-11230-5. https://doi.org/10.1007/978-3-319-11230-5

  78. Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla 2009: an automatic algorithm portfolio for sat. SAT 4, 53–55 (2009)

    MATH  Google Scholar 

  79. Gent, I.P., Jefferson, C., Kotthoff, L., Miguel, I., Moore, N.C.A., Nightingale, P., Petrie, K.E.: Learning when to use lazy learning in constraint solving. In: H. Coelho, R. Studer, M.J. Wooldridge (eds.) ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings, Frontiers in Artificial Intelligence and Applications, vol. 215, pp. 873–878. IOS Press (2010). https://doi.org/10.3233/978-1-60750-606-5-873

  80. Amadini, R., Gabbrielli, M., Mauro, J.: SUNNY: a lazy portfolio approach for constraint solving. Theory Pract. Log. Program. 14(4–5), 509–524 (2014). https://doi.org/10.1017/S1471068414000179

    Article  MATH  Google Scholar 

  81. Hurley, B., Kotthoff, L., Malitsky, Y., O’Sullivan, B.: Proteus: A hierarchical portfolio of solvers and transformations. In: H. Simonis (ed.) Integration of AI and OR Techniques in Constraint Programming - 11th International Conference, CPAIOR 2014, Cork, Ireland, May 19-23, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8451, pp. 301–317. Springer (2014). https://doi.org/10.1007/978-3-319-07046-9_22

  82. Kotthoff, L., Gent, I.P., Miguel, I.: An evaluation of machine learning in algorithm selection for search problems. AI Commun. 25(3), 257–270 (2012). https://doi.org/10.3233/AIC-2012-0533

    Article  MathSciNet  Google Scholar 

  83. Sutcliffe, G.: The TPTP problem library and associated infrastructure–from CNF to th0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483–502 (2017). https://doi.org/10.1007/s10817-017-9407-7

    Article  MathSciNet  MATH  Google Scholar 

  84. Urban, J., Sutcliffe, G., Pudlák, P., Vyskocil, J.: Malarea SG1- machine learner for automated reasoning with semantic guidance. In: A. Armando, P. Baumgartner, G. Dowek (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5195, pp. 441–456. Springer (2008). https://doi.org/10.1007/978-3-540-71070-7_37

  85. Healy, A., Monahan, R., Power, J.F.: Predicting SMT solver performance for software verification. In: C. Dubois, P. Masci, D. Méry (eds.) Proceedings of the Third Workshop on Formal Integrated Development Environment, F-IDE@FM 2016, Limassol, Cyprus, November 8, 2016, EPTCS, vol. 240, pp. 20–37 (2016). https://doi.org/10.4204/EPTCS.240.2

  86. Beyer, D., Dangl, M.: Strategy selection for software verification based on boolean features—a simple but effective approach 11245, 144–159 (2018). https://doi.org/10.1007/978-3-030-03421-4_11

  87. Richter, C., Wehrheim, H.: Pesco: Predicting sequential combinations of verifiers—(competition contribution). In: D. Beyer, M. Huisman, F. Kordon, B. Steffen (eds.) Tools and Algorithms for the Construction and Analysis of Systems—25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, Lecture Notes in Computer Science, vol. 11429, pp. 229–233. Springer (2019). https://doi.org/10.1007/978-3-030-17502-3_19

  88. Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: N. Creignou, D.L. Berre (eds.) Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9710, pp. 123–140. Springer (2016). https://doi.org/10.1007/978-3-319-40970-2_9

  89. Nejati, S., Frioux, L.L., Ganesh, V.: A machine learning based splitting heuristic for divide-and-conquer solvers. In: H. Simonis (ed.) Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12333, pp. 899–916. Springer (2020). https://doi.org/10.1007/978-3-030-58475-7_52

  90. Pimpalkhare, N., Mora, F., Polgreen, E., Seshia, S.A.: Medleysolver: Online SMT algorithm selection. In: C. Li, F. Manyà (eds.) Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, Lecture Notes in Computer Science, vol. 12831, pp. 453–470. Springer (2021). https://doi.org/10.1007/978-3-030-80223-3_31. https://doi.org/10.1007/978-3-030-80223-3_31

  91. Hula, J., Mojzísek, D., Janota, M.: Graph neural networks for scheduling of SMT solvers. In: 33rd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2021, Washington, DC, USA, November 1-3, 2021, pp. 447–451. IEEE (2021). https://doi.org/10.1109/ICTAI52525.2021.00072. https://doi.org/10.1109/ICTAI52525.2021.00072

Download references

Acknowledgements

We would like to thank Karthick Jayaraman for his assistance in obtaining the benchmarks used in Sect. 6. We would like to thank Vineel Nagisetty, Laura Graves, Murphy Berzish, Federico Mora, and the SMT and TACAS communities for their feedback on earlier versions of this work.

Author information

Authors and Affiliations

  1. 200 University Ave W, Waterloo, Ontario, Canada

    Joseph Scott, Saeed Nejati & Vijay Ganesh

  2. 450 Jane Stanford Way, Stanford, CA, 94305, USA

    Aina Niemetz & Mathias Preiner

Authors
  1. Joseph Scott
    View author publications

    Search author on:PubMed Google Scholar

  2. Aina Niemetz
    View author publications

    Search author on:PubMed Google Scholar

  3. Mathias Preiner
    View author publications

    Search author on:PubMed Google Scholar

  4. Saeed Nejati
    View author publications

    Search author on:PubMed Google Scholar

  5. Vijay Ganesh
    View author publications

    Search author on:PubMed Google Scholar

Corresponding author

Correspondence to Joseph Scott.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

The original online version of this article was revised: Figure 4 was not correct.

This work was supported in part by DARPA (award no. FA8650-18-2-7861) and ONR (award no. N68335-17-C-0558).

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Scott, J., Niemetz, A., Preiner, M. et al. Algorithm selection for SMT. Int J Softw Tools Technol Transfer 25, 219–239 (2023). https://doi.org/10.1007/s10009-023-00696-0

Download citation

  • Accepted:

  • Published:

  • Version of record:

  • Issue date:

  • DOI: https://doi.org/10.1007/s10009-023-00696-0

Keywords

Profiles

  1. Aina Niemetz View author profile
  2. Vijay Ganesh View author profile