{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:08Z","timestamp":1776333488455,"version":"3.51.2"},"reference-count":91,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T00:00:00Z","timestamp":1676419200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T00:00:00Z","timestamp":1676419200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2023,4]]},"DOI":"10.1007\/s10009-023-00696-0","type":"journal-article","created":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T07:35:58Z","timestamp":1676619358000},"page":"219-239","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Algorithm selection for SMT"],"prefix":"10.1007","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4145-1612","authenticated-orcid":false,"given":"Joseph","family":"Scott","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2600-5283","authenticated-orcid":false,"given":"Aina","family":"Niemetz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7142-6258","authenticated-orcid":false,"given":"Mathias","family":"Preiner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1473-3630","authenticated-orcid":false,"given":"Saeed","family":"Nejati","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6029-2047","authenticated-orcid":false,"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,2,15]]},"reference":[{"key":"696_CR1","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla at the SMT-COMP 2020. CoRR abs\/2006.01621 (2020). https:\/\/arxiv.org\/abs\/2006.01621"},{"issue":"1","key":"696_CR2","doi-asserted-by":"publisher","first-page":"53","DOI":"10.3233\/sat190101","volume":"9","author":"A Niemetz","year":"2014","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0. J. Satisf. Boolean Model. Comput. 9(1), 53\u201358 (2014). https:\/\/doi.org\/10.3233\/sat190101","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"696_CR3","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: G.\u00a0Gopalakrishnan, S.\u00a0Qadeer (eds.) Computer Aided Verification\u201423rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6806, pp. 171\u2013177. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"696_CR4","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: D.\u00a0Fisman, G.\u00a0Rosu (eds.) Tools and Algorithms for the Construction and Analysis of Systems\u201428th 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\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"696_CR5","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 SMT solver. In: N.\u00a0Piterman, 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\u2013107. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"696_CR6","doi-asserted-by":"publisher","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: Smtinterpol: An interpolating SMT solver. In: A.F. Donaldson, D.\u00a0Parker (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\u2013254. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31759-0_19. https:\/\/doi.org\/10.1007\/978-3-642-31759-0_19","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"696_CR7","doi-asserted-by":"publisher","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: W.\u00a0Damm, H.\u00a0Hermanns (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\u2013531. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_52","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"696_CR8","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: A.\u00a0Biere, R.\u00a0Bloem (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\u2013744. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"696_CR9","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: C.R. Ramakrishnan, J.\u00a0Rehof (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\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"696_CR10","doi-asserted-by":"publisher","first-page":"10:1","DOI":"10.1145\/1455518.1455522","volume":"12","author":"C Cadar","year":"2008","unstructured":"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","journal-title":"ACM Trans. Inf. Syst. Secur."},{"issue":"4","key":"696_CR11","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","volume":"11","author":"CS Pasareanu","year":"2009","unstructured":"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\u2013353 (2009). https:\/\/doi.org\/10.1007\/s10009-009-0118-1","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"696_CR12","doi-asserted-by":"publisher","unstructured":"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\u2014(competition contribution). In: D.\u00a0Beyer, M.\u00a0Huisman, F.\u00a0Kordon, B.\u00a0Steffen (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\u2013213. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_15","DOI":"10.1007\/978-3-030-17502-3_15"},{"key":"696_CR13","doi-asserted-by":"publisher","unstructured":"Brain, M., Schanda, F., Sun, Y.: Building better bit-blasting for floating-point problems. In: T.\u00a0Vojnar, L.\u00a0Zhang (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\u201398. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_5","DOI":"10.1007\/978-3-030-17462-0_5"},{"key":"696_CR14","doi-asserted-by":"publisher","unstructured":"Goues, C.L., Leino, K.R.M., Moskal, M.: The boogie verification debugger (tool paper). In: G.\u00a0Barthe, A.\u00a0Pardo, G.\u00a0Schneider (eds.) Software Engineering and Formal Methods\u20149th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings, Lecture Notes in Computer Science, vol. 7041, pp. 407\u2013414. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-24690-6_28","DOI":"10.1007\/978-3-642-24690-6_28"},{"key":"696_CR15","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Automating theorem proving with SMT. In: S.\u00a0Blazy, C.\u00a0Paulin-Mohring, D.\u00a0Pichardie (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\u201316. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_2","DOI":"10.1007\/978-3-642-39634-2_2"},{"key":"696_CR16","unstructured":"Rintanen, J.: Madagascar: Scalable planning with sat. Proceedings of the 8th International Planning Competition (IPC-2014) 21 (2014)"},{"key":"696_CR17","doi-asserted-by":"publisher","unstructured":"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.\u00a0Majumdar, V.\u00a0Kuncak (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\u2013117. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"696_CR18","unstructured":"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"},{"issue":"3","key":"696_CR19","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/2093548.2093564","volume":"55","author":"P Godefroid","year":"2012","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: SAGE: whitebox fuzzing for security testing. Commun. ACM 55(3), 40\u201344 (2012). https:\/\/doi.org\/10.1145\/2093548.2093564","journal-title":"Commun. ACM"},{"key":"696_CR20","doi-asserted-by":"publisher","unstructured":"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.\u00a0Bj\u00f8rner, A.\u00a0Gurfinkel (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30\u2013November 2, 2018, pp. 1\u20139. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8602994","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"696_CR21","doi-asserted-by":"publisher","unstructured":"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\u00e9guelin, S.Z., Zinzindohoue, J.K.: Everest: Towards a verified, drop-in replacement of HTTPS. In: B.S. Lerner, R.\u00a0Bod\u00edk, S.\u00a0Krishnamurthi (eds.) 2nd Summit on Advances in Programming Languages, SNAPL 2017, May 7-10, 2017, Asilomar, CA, USA, LIPIcs, vol.\u00a071, pp. 1:1\u20131:12. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.SNAPL.2017.1","DOI":"10.4230\/LIPIcs.SNAPL.2017.1"},{"key":"696_CR22","unstructured":"Hadarean, L., Hyv\u00e4rinen, A., Niemetz, A., Reger, G.: Smt-comp 2019. https:\/\/www.smt-comp.org\/2019 (2019)"},{"issue":"1","key":"696_CR23","doi-asserted-by":"publisher","first-page":"221","DOI":"10.3233\/SAT190123","volume":"11","author":"T Weber","year":"2019","unstructured":"Weber, T., Conchon, S., D\u00e9harbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015\u20132018. J. Satisf. Boolean Model. Comput. 11(1), 221\u2013259 (2019). https:\/\/doi.org\/10.3233\/SAT190123","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"696_CR24","doi-asserted-by":"publisher","unstructured":"Brain, M., Schanda, F., Sun, Y.: Building better bit-blasting for floating-point problems. In: T.\u00a0Vojnar, L.\u00a0Zhang (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\u201398. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_5","DOI":"10.1007\/978-3-030-17462-0_5"},{"issue":"2","key":"696_CR25","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10703-013-0203-7","volume":"45","author":"M Brain","year":"2014","unstructured":"Brain, M., D\u2019Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods Syst. Des. 45(2), 213\u2013245 (2014). https:\/\/doi.org\/10.1007\/s10703-013-0203-7","journal-title":"Formal Methods Syst. Des."},{"key":"696_CR26","doi-asserted-by":"publisher","unstructured":"Salvia, R., Titolo, L., Feli\u00fa, M.A., Moscato, M.M., Mu\u00f1oz, 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\u2013370. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_25","DOI":"10.1007\/978-3-030-20652-9_25"},{"key":"696_CR27","doi-asserted-by":"publisher","unstructured":"Fu, Z., Su, Z.: Xsat: A fast floating-point satisfiability solver. In: S.\u00a0Chaudhuri, A.\u00a0Farzan (eds.) Computer Aided Verification\u201428th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, Lecture Notes in Computer Science, vol. 9780, pp. 187\u2013209. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_11","DOI":"10.1007\/978-3-319-41540-6_11"},{"key":"696_CR28","doi-asserted-by":"publisher","unstructured":"Ben Khadra, M.A., Stoffel, D., Kunz, W.: gosat: Floating-point satisfiability as global optimization. In: D.\u00a0Stewart, G.\u00a0Weissenbacher (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017, pp. 11\u201314. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102235","DOI":"10.23919\/FMCAD.2017.8102235"},{"key":"696_CR29","doi-asserted-by":"crossref","unstructured":"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\u201313910. AAAI Press (2020). https:\/\/aaai.org\/ojs\/index.php\/AAAI\/article\/view\/7227","DOI":"10.1609\/aaai.v34i10.7227"},{"key":"696_CR30","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: A.\u00a0Gupta, D.\u00a0Kroening (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK) (2010)"},{"key":"696_CR31","doi-asserted-by":"crossref","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2020)","DOI":"10.3233\/FAIA201017"},{"key":"696_CR32","first-page":"2825","volume":"12","author":"F Pedregosa","year":"2011","unstructured":"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\u20132830 (2011)","journal-title":"J. Mach. Learn. Res."},{"key":"696_CR33","first-page":"8026","volume":"32","author":"A Paszke","year":"2019","unstructured":"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\u20138037 (2019)","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"696_CR34","doi-asserted-by":"publisher","unstructured":"Pulina, L., Tacchella, A.: A multi-engine solver for quantified boolean formulas. In: C.\u00a0Bessiere (ed.) Principles and Practice of Constraint Programming\u2014CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4741, pp. 574\u2013589. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-74970-7_41","DOI":"10.1007\/978-3-540-74970-7_41"},{"key":"696_CR35","doi-asserted-by":"publisher","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla-07: The design and analysis of an algorithm portfolio for SAT. In: C.\u00a0Bessiere (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\u2013727. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-74970-7_50","DOI":"10.1007\/978-3-540-74970-7_50"},{"key":"696_CR36","unstructured":"Scott, J., Poupart, P., Ganesh, V.: An algorithm selection approach for QF_FP solvers. In: 17th International Workshop on Satisfiability Modulo Theories (2019)"},{"key":"696_CR37","unstructured":"Balunovic, M., Bielik, P., Vechev, M.T.: Learning to solve SMT formulas. In: S.\u00a0Bengio, H.M. Wallach, H.\u00a0Larochelle, K.\u00a0Grauman, N.\u00a0Cesa-Bianchi, R.\u00a0Garnett (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montr\u00e9al, Canada, pp. 10338\u201310349 (2018). http:\/\/papers.nips.cc\/paper\/8233-learning-to-solve-smt-formulas"},{"key":"696_CR38","doi-asserted-by":"publisher","unstructured":"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","DOI":"10.14722\/bar.2019.23080"},{"key":"696_CR39","unstructured":"MachSMT GitHub repository. https:\/\/github.com\/machsmt\/machsmt (2022)"},{"key":"696_CR40","doi-asserted-by":"publisher","unstructured":"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\u201427th 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\u2013325. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_16. https:\/\/doi.org\/10.1007\/978-3-030-72013-1_16","DOI":"10.1007\/978-3-030-72013-1_16"},{"key":"696_CR41","unstructured":"Barrett, C., Stump, A., Tinelli, C., et\u00a0al.: The smt-lib standard: Version 2.0. In: Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England), vol.\u00a013, p.\u00a014 (2010)"},{"key":"696_CR42","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0065-2458(08)60520-3","volume":"15","author":"JR Rice","year":"1976","unstructured":"Rice, J.R.: The algorithm selection problem. Adv. Comput. 15, 65\u2013118 (1976). https:\/\/doi.org\/10.1016\/S0065-2458(08)60520-3","journal-title":"Adv. Comput."},{"key":"696_CR43","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565\u2013606 (2008). https:\/\/doi.org\/10.1613\/jair.2490","journal-title":"J. Artif. Intell. Res."},{"key":"696_CR44","doi-asserted-by":"publisher","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Evaluating component solver contributions to portfolio-based algorithm selectors. In: A.\u00a0Cimatti, R.\u00a0Sebastiani (eds.) Theory and Applications of Satisfiability Testing\u2014SAT 2012\u201415th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7317, pp. 228\u2013241. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_18","DOI":"10.1007\/978-3-642-31612-8_18"},{"issue":"771\u2013780","key":"696_CR45","first-page":"1612","volume":"14","author":"Y Freund","year":"1999","unstructured":"Freund, Y., Schapire, R., Abe, N.: A short introduction to boosting. J. Jpn. Soc. Artif. Intel. 14(771\u2013780), 1612 (1999)","journal-title":"J. Jpn. Soc. Artif. Intel."},{"key":"696_CR46","unstructured":"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.\u00a01, pp. 196\u2013201. IEEE (2005)"},{"key":"696_CR47","unstructured":"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\u2013115. Morgan Kaufmann (1997)"},{"issue":"7553","key":"696_CR48","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1038\/nature14539","volume":"521","author":"Y LeCun","year":"2015","unstructured":"LeCun, Y., Bengio, Y., Hinton, G.: Deep learning. Nature 521(7553), 436\u2013444 (2015)","journal-title":"Nature"},{"key":"696_CR49","unstructured":"Goodfellow, I., Bengio, Y., Courville, A.: Deep learning. MIT press (2016)"},{"key":"696_CR50","doi-asserted-by":"publisher","first-page":"i1981","DOI":"10.1136\/bmj.i1981","volume":"352","author":"S Greenland","year":"2016","unstructured":"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","journal-title":"bmj"},{"key":"696_CR51","unstructured":"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.\u00a0Tresp (eds.) Advances in Neural Information Processing Systems 13, Papers from Neural Information Processing Systems (NIPS) 2000, Denver, CO, USA, pp. 668\u2013674. MIT Press (2000). https:\/\/proceedings.neurips.cc\/paper\/2000\/hash\/8c3039bd5842dca3d944faab91447818-Abstract.html"},{"key":"696_CR52","doi-asserted-by":"publisher","unstructured":"Kira, K., Rendell, L.A.: A practical approach to feature selection. In: D.H. Sleeman, P.\u00a0Edwards (eds.) Proceedings of the Ninth International Workshop on Machine Learning (ML 1992), Aberdeen, Scotland, UK, July 1-3, 1992, pp. 249\u2013256. Morgan Kaufmann (1992). https:\/\/doi.org\/10.1016\/b978-1-55860-247-2.50037-1","DOI":"10.1016\/b978-1-55860-247-2.50037-1"},{"issue":"3","key":"696_CR53","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1109\/TPAMI.2009.187","volume":"32","author":"JD Rodr\u00edguez","year":"2010","unstructured":"Rodr\u00edguez, J.D., Mart\u00ednez, 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\u2013575 (2010). https:\/\/doi.org\/10.1109\/TPAMI.2009.187","journal-title":"IEEE Trans. Pattern Anal. Mach. Intell."},{"key":"696_CR54","unstructured":"Moore, A.W.: Cross-validation for detecting and preventing overfitting. School of Computer Science Carneigie Mellon University (2001)"},{"issue":"1\u20133","key":"696_CR55","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0169-7439(87)80084-9","volume":"2","author":"S Wold","year":"1987","unstructured":"Wold, S., Esbensen, K., Geladi, P.: Principal component analysis. Chemom. Intel. Lab. Syst. 2(1\u20133), 37\u201352 (1987)","journal-title":"Chemom. Intel. Lab. Syst."},{"issue":"66\u201371","key":"696_CR56","first-page":"13","volume":"10","author":"L Van Der Maaten","year":"2009","unstructured":"Van Der Maaten, L., Postma, E., Van den Herik, J.: Dimensionality reduction: a comparative. J. Mach. Learn. Res. 10(66\u201371), 13 (2009)","journal-title":"J. Mach. Learn. Res."},{"key":"696_CR57","first-page":"9","volume":"1","author":"N Grira","year":"2004","unstructured":"Grira, N., Crucianu, M., Boujemaa, N.: Unsupervised and semi-supervised clustering: a brief survey. Rev. Mach. Learn. Techn. Process. Multimed. Content 1, 9\u201316 (2004)","journal-title":"Rev. Mach. Learn. Techn. Process. Multimed. Content"},{"key":"696_CR58","doi-asserted-by":"publisher","unstructured":"Xu, R., II, Wunsch, D.: Survey of clustering algorithms. IEEE Trans. Neural Netw. 16(3), 645\u2013678 (2005). https:\/\/doi.org\/10.1109\/TNN.2005.845141. https:\/\/doi.org\/10.1109\/TNN.2005.845141","DOI":"10.1109\/TNN.2005.845141"},{"issue":"Suppl 1","key":"696_CR59","doi-asserted-by":"publisher","first-page":"949","DOI":"10.1007\/s10586-017-1117-8","volume":"22","author":"D Kwon","year":"2019","unstructured":"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\u2013961 (2019). https:\/\/doi.org\/10.1007\/s10586-017-1117-8","journal-title":"Clust. Comput."},{"key":"696_CR60","doi-asserted-by":"publisher","first-page":"708","DOI":"10.1016\/j.procs.2015.08.220","volume":"60","author":"S Agrawal","year":"2015","unstructured":"Agrawal, S., Agrawal, J.: Survey on anomaly detection using data mining techniques. Procedia Comput. Sci. 60, 708\u2013713 (2015). https:\/\/doi.org\/10.1016\/j.procs.2015.08.220","journal-title":"Procedia Comput. Sci."},{"issue":"2","key":"696_CR61","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1137\/090771806","volume":"53","author":"N Halko","year":"2011","unstructured":"Halko, N., Martinsson, P., Tropp, J.A.: Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions. SIAM Rev. 53(2), 217\u2013288 (2011). https:\/\/doi.org\/10.1137\/090771806","journal-title":"SIAM Rev."},{"key":"696_CR62","unstructured":"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\u201358 (2012)"},{"issue":"7825","key":"696_CR63","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1038\/s41586-020-2649-2","volume":"585","author":"CR Harris","year":"2020","unstructured":"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\u2013362 (2020)","journal-title":"Nature"},{"key":"696_CR64","doi-asserted-by":"publisher","unstructured":"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 \u201916, pp. 785\u2013794. ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2939672.2939785. http:\/\/doi.acm.org\/10.1145\/2939672.2939785","DOI":"10.1145\/2939672.2939785"},{"key":"696_CR65","unstructured":"Barbosa, H., Hyv\u00e4rinen, A., Hoenecke, J.: Smt-comp 2020. https:\/\/www.smt-comp.org\/2020 (2020)"},{"key":"696_CR66","doi-asserted-by":"publisher","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: Starexec: A cross-community infrastructure for logic solving. In: S.\u00a0Demri, D.\u00a0Kapur, C.\u00a0Weidenbach (eds.) Automated Reasoning\u20147th 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\u2013373. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"696_CR67","unstructured":"Marijn\u00a0Heule Matti\u00a0J\u00e4rvisalo, M.S.: Sat race 2019 (2019). http:\/\/sat-race-2019.ciirc.cvut.cz\/"},{"key":"696_CR68","doi-asserted-by":"publisher","unstructured":"N\u00f6tzli, A., Reynolds, A., Barbosa, H., Niemetz, A., Preiner, M., Barrett, C.W., Tinelli, C.: Syntax-guided rewrite rule enumeration for SMT solvers. In: M.\u00a0Janota, I.\u00a0Lynce (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\u2013297. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_20. https:\/\/doi.org\/10.1007\/978-3-030-24258-9_20","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"696_CR69","unstructured":"Jayaraman, K., Bj\u00f8rner, N., Outhred, G., Kaufman, C.: Automated analysis and debugging of network connectivity policies. Microsoft Research pp. 1\u201311 (2014)"},{"key":"696_CR70","doi-asserted-by":"crossref","unstructured":"Baldwin, S.: Compute canada: advancing computational research. In: Journal of Physics: Conference Series, vol. 341, p. 012001. IOP Publishing (2012)","DOI":"10.1088\/1742-6596\/341\/1\/012001"},{"key":"696_CR71","unstructured":"Lundberg, S.M., Lee, S.I.: A unified approach to interpreting model predictions. In: I.\u00a0Guyon, U.V. Luxburg, S.\u00a0Bengio, H.\u00a0Wallach, R.\u00a0Fergus, S.\u00a0Vishwanathan, R.\u00a0Garnett (eds.) Advances in Neural Information Processing Systems 30, pp. 4765\u20134774. Curran Associates, Inc. (2017). http:\/\/papers.nips.cc\/paper\/7062-a-unified-approach-to-interpreting-model-predictions.pdf"},{"issue":"2","key":"696_CR72","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.asoc.2004.12.002","volume":"6","author":"S Ali","year":"2006","unstructured":"Ali, S., Smith, K.A.: On learning algorithm selection for classification. Appl. Soft Comput. 6(2), 119\u2013138 (2006). https:\/\/doi.org\/10.1016\/j.asoc.2004.12.002","journal-title":"Appl. Soft Comput."},{"key":"696_CR73","doi-asserted-by":"publisher","unstructured":"Kotthoff, L.: Algorithm selection for combinatorial search problems: A survey. In: C.\u00a0Bessiere, L.D. Raedt, L.\u00a0Kotthoff, S.\u00a0Nijssen, B.\u00a0O\u2019Sullivan, D.\u00a0Pedreschi (eds.) Data Mining and Constraint Programming - Foundations of a Cross-Disciplinary Approach, Lecture Notes in Computer Science, vol. 10101, pp. 149\u2013190. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-50137-6_7","DOI":"10.1007\/978-3-319-50137-6_7"},{"key":"696_CR74","doi-asserted-by":"publisher","unstructured":"Tierney, K., Malitsky, Y.: An algorithm selection benchmark of the container pre-marshalling problem. In: C.\u00a0Dhaenens, L.\u00a0Jourdan, M.\u00a0Marmion (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\u201322. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-19084-6_2","DOI":"10.1007\/978-3-319-19084-6_2"},{"issue":"4","key":"696_CR75","doi-asserted-by":"publisher","first-page":"717","DOI":"10.3233\/AIC-150671","volume":"28","author":"M Vallati","year":"2015","unstructured":"Vallati, M., Chrpa, L., Kitchin, D.E.: Portfolio-based planning: state of the art, common practice and open challenges. AI Commun. 28(4), 717\u2013733 (2015). https:\/\/doi.org\/10.3233\/AIC-150671","journal-title":"AI Commun."},{"key":"696_CR76","unstructured":"O\u2019Mahony, E., Hebrard, E., Holland, A., Nugent, C., O\u2019Sullivan, B.: Using Case-based Reasoning in an Algorithm Portfolio for Constraint Solving. In: Irish conference on artificial intelligence and cognitive science, pp. 210\u2013216 (2008). https:\/\/homepages.laas.fr\/ehebrard\/papers\/aics2008.pdf"},{"key":"696_CR77","doi-asserted-by":"publisher","unstructured":"Malitsky, Y.: Evolving instance-specific algorithm configuration. In: Instance-Specific Algorithm Configuration, pp. 93\u2013105. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11230-5. https:\/\/doi.org\/10.1007\/978-3-319-11230-5","DOI":"10.1007\/978-3-319-11230-5"},{"key":"696_CR78","first-page":"53","volume":"4","author":"L Xu","year":"2009","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla 2009: an automatic algorithm portfolio for sat. SAT 4, 53\u201355 (2009)","journal-title":"SAT"},{"key":"696_CR79","doi-asserted-by":"publisher","unstructured":"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.\u00a0Coelho, R.\u00a0Studer, 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\u2013878. IOS Press (2010). https:\/\/doi.org\/10.3233\/978-1-60750-606-5-873","DOI":"10.3233\/978-1-60750-606-5-873"},{"issue":"4\u20135","key":"696_CR80","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1017\/S1471068414000179","volume":"14","author":"R Amadini","year":"2014","unstructured":"Amadini, R., Gabbrielli, M., Mauro, J.: SUNNY: a lazy portfolio approach for constraint solving. Theory Pract. Log. Program. 14(4\u20135), 509\u2013524 (2014). https:\/\/doi.org\/10.1017\/S1471068414000179","journal-title":"Theory Pract. Log. Program."},{"key":"696_CR81","doi-asserted-by":"publisher","unstructured":"Hurley, B., Kotthoff, L., Malitsky, Y., O\u2019Sullivan, B.: Proteus: A hierarchical portfolio of solvers and transformations. In: H.\u00a0Simonis (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\u2013317. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-07046-9_22","DOI":"10.1007\/978-3-319-07046-9_22"},{"issue":"3","key":"696_CR82","doi-asserted-by":"publisher","first-page":"257","DOI":"10.3233\/AIC-2012-0533","volume":"25","author":"L Kotthoff","year":"2012","unstructured":"Kotthoff, L., Gent, I.P., Miguel, I.: An evaluation of machine learning in algorithm selection for search problems. AI Commun. 25(3), 257\u2013270 (2012). https:\/\/doi.org\/10.3233\/AIC-2012-0533","journal-title":"AI Commun."},{"issue":"4","key":"696_CR83","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure\u2013from CNF to th0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","journal-title":"J. Autom. Reason."},{"key":"696_CR84","doi-asserted-by":"publisher","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vyskocil, J.: Malarea SG1- machine learner for automated reasoning with semantic guidance. In: A.\u00a0Armando, P.\u00a0Baumgartner, G.\u00a0Dowek (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\u2013456. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_37","DOI":"10.1007\/978-3-540-71070-7_37"},{"key":"696_CR85","doi-asserted-by":"publisher","unstructured":"Healy, A., Monahan, R., Power, J.F.: Predicting SMT solver performance for software verification. In: C.\u00a0Dubois, P.\u00a0Masci, D.\u00a0M\u00e9ry (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\u201337 (2016). https:\/\/doi.org\/10.4204\/EPTCS.240.2","DOI":"10.4204\/EPTCS.240.2"},{"key":"696_CR86","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Strategy selection for software verification based on boolean features\u2014a simple but effective approach 11245, 144\u2013159 (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_11","DOI":"10.1007\/978-3-030-03421-4_11"},{"key":"696_CR87","doi-asserted-by":"publisher","unstructured":"Richter, C., Wehrheim, H.: Pesco: Predicting sequential combinations of verifiers\u2014(competition contribution). In: D.\u00a0Beyer, M.\u00a0Huisman, F.\u00a0Kordon, B.\u00a0Steffen (eds.) Tools and Algorithms for the Construction and Analysis of Systems\u201425 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\u2013233. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_19","DOI":"10.1007\/978-3-030-17502-3_19"},{"key":"696_CR88","doi-asserted-by":"publisher","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: N.\u00a0Creignou, 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\u2013140. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_9","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"696_CR89","doi-asserted-by":"publisher","unstructured":"Nejati, S., Frioux, L.L., Ganesh, V.: A machine learning based splitting heuristic for divide-and-conquer solvers. In: H.\u00a0Simonis (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\u2013916. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_52","DOI":"10.1007\/978-3-030-58475-7_52"},{"key":"696_CR90","doi-asserted-by":"publisher","unstructured":"Pimpalkhare, N., Mora, F., Polgreen, E., Seshia, S.A.: Medleysolver: Online SMT algorithm selection. In: C.\u00a0Li, F.\u00a0Many\u00e0 (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\u2013470. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_31. https:\/\/doi.org\/10.1007\/978-3-030-80223-3_31","DOI":"10.1007\/978-3-030-80223-3_31"},{"key":"696_CR91","doi-asserted-by":"publisher","unstructured":"Hula, J., Mojz\u00edsek, 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\u2013451. IEEE (2021). https:\/\/doi.org\/10.1109\/ICTAI52525.2021.00072. https:\/\/doi.org\/10.1109\/ICTAI52525.2021.00072","DOI":"10.1109\/ICTAI52525.2021.00072"}],"updated-by":[{"DOI":"10.1007\/s10009-023-00714-1","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2023,8,14]],"date-time":"2023-08-14T00:00:00Z","timestamp":1691971200000}}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00696-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-023-00696-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00696-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,14]],"date-time":"2023-08-14T16:03:03Z","timestamp":1692028983000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-023-00696-0"}},"subtitle":["MachSMT: machine learning driven algorithm selection for SMT solvers"],"short-title":[],"issued":{"date-parts":[[2023,2,15]]},"references-count":91,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4]]}},"alternative-id":["696"],"URL":"https:\/\/doi.org\/10.1007\/s10009-023-00696-0","relation":{"correction":[{"id-type":"doi","id":"10.1007\/s10009-023-00714-1","asserted-by":"object"}]},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,2,15]]},"assertion":[{"value":"13 January 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 February 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 August 2023","order":3,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":4,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":5,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s10009-023-00714-1","URL":"https:\/\/doi.org\/10.1007\/s10009-023-00714-1","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}