{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T16:52:06Z","timestamp":1773939126731,"version":"3.50.1"},"publisher-location":"Cham","reference-count":72,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720124","type":"print"},{"value":"9783030720131","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we present MachSMT, an algorithm selection tool for Satisfiability Modulo Theories (SMT) solvers. MachSMT supports the entirety of the SMT-LIB language. It employs machine learning (ML) methods to construct both empirical hardness models (EHMs) and pairwise ranking comparators (PWCs) over state-of-the-art SMT solvers. Given an SMT formula <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {I}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>I<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> as input, MachSMT leverages these learnt models to output a ranking of solvers based on predicted run time on the formula <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {I}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>I<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. We evaluate MachSMT on the solvers, benchmarks, and data obtained from SMT-COMP 2019 and 2020. We observe MachSMT frequently improves on competition winners, winning <jats:inline-formula><jats:alternatives><jats:tex-math>$$54$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mrow>\n                      <mml:mn>54<\/mml:mn>\n                    <\/mml:mrow>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> divisions outright and up to a <jats:inline-formula><jats:alternatives><jats:tex-math>$$198.4$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mrow>\n                      <mml:mn>198.4<\/mml:mn>\n                    <\/mml:mrow>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>% improvement in PAR-2 score, notably in logics that have broad applications (e.g., BV, LIA, NRA, etc.) in verification, program analysis, and software engineering. The MachSMT tool is designed to be easily tuned and extended to any suitable solver application by users. MachSMT is not a replacement for SMT solvers by any means. Instead, it is a tool that enables users to leverage the collective strength of the diverse set of algorithms implemented as part of these sophisticated solvers.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_16","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"303-325","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers"],"prefix":"10.1007","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":[[2021,3,23]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Agrawal, S., Agrawal, J.: Survey on anomaly detection using data mining techniques. Procedia Computer Science 60, 708\u2013713 (2015). https:\/\/doi.org\/10.1016\/j.procs.2015.08.220","DOI":"10.1016\/j.procs.2015.08.220"},{"key":"16_CR2","doi-asserted-by":"publisher","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","DOI":"10.1016\/j.asoc.2004.12.002"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Amadini, R., Gabbrielli, M., Mauro, J.: SUNNY: a lazy portfolio approach for constraint solving. Theory Pract. Log. Program. 14(4-5), 509\u2013524 (2014). https:\/\/doi.org\/10.1017\/S1471068414000179","DOI":"10.1017\/S1471068414000179"},{"key":"16_CR4","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: Bj\u00f8rner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. pp.\u00a01\u20139. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8602994","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"16_CR5","unstructured":"Balunovic, M., Bielik, P., Vechev, M.T.: Learning to solve SMT formulas. In: Bengio, S., Wallach, H.M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montr\u00e9al, Canada. pp. 10338\u201310349 (2018), http:\/\/papers.nips.cc\/paper\/8233-learning-to-solve-smt-formulas"},{"key":"16_CR6","unstructured":"Barbosa, H., Hyv\u00e4rinen, A., Hoenecke, J.: Smt-comp 2020. https:\/\/www.smt-comp.org\/2020 (2020)"},{"key":"16_CR7","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":"16_CR8","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshopon Satisfiability Modulo Theories (Edinburgh, UK) (2010)"},{"key":"16_CR9","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: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06806, 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":"16_CR10","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., de\u00a0Moura, L.M., Stump, A.: SMT-COMP: satisfiability modulo theories competition. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings. Lecture Notes in Computer Science, vol.\u00a03576, pp. 20\u201323. Springer (2005). https:\/\/doi.org\/10.1007\/11513988_4","DOI":"10.1007\/11513988_4"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Ben Khadra, M.A., Stoffel, D., Kunz, W.: gosat: Floating-point satisfiability as global optimization. In: Stewart, D., Weissen bacher, G. (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":"16_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Strategy selection for software verification based on boolean features - A 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":"16_CR13","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: Lerner, B.S., Bod\u00edk, R., Krishnamurthi, S. (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 - Leibniz-Zentrum f\u00fcrInformatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.SNAPL.2017.1, https:\/\/doi.org\/10.4230\/LIPIcs.SNAPL.2017.1","DOI":"10.4230\/LIPIcs.SNAPL.2017.1"},{"key":"16_CR14","doi-asserted-by":"publisher","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","DOI":"10.1007\/s10703-013-0203-7"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Brain, M., Schanda, F., Sun, Y.: Building better bit-blasting for floating-point problems. In: Vojnar, T., Zhang, L. (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":"16_CR16","doi-asserted-by":"publisher","unstructured":"Brain, M., Schanda, F., Sun, Y.: Building better bit-blasting for floating-point problems. In: Vojnar, T., Zhang, L. (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":"16_CR17","doi-asserted-by":"publisher","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\u201310:38 (2008). https:\/\/doi.org\/10.1145\/1455518.1455522","DOI":"10.1145\/1455518.1455522"},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 SMT solver. In: Piterman, N., Smolka, S.A. (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.\u00a07795, 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":"16_CR19","unstructured":"Drucker, H.: Improving regressors using boosting techniques. In: Fisher, D.H. (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)"},{"key":"16_CR20","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (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.\u00a08559, 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":"16_CR21","unstructured":"Freund, Y., Schapire, R., Abe, N.: A short introduction to boosting. Journal-Japanese Society For Artificial Intelligence 14(771-780),\u00a01612 (1999)"},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Fu, Z., Su, Z.: Xsat: A fast floating-point satisfiability solver. In: Chaudhuri, S., Farzan, A. (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.\u00a09780, 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":"16_CR23","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 - (competition contribution). In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (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":"16_CR24","doi-asserted-by":"publisher","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04590, 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":"16_CR25","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: Coelho, H., Studer, R., Wooldridge, M.J. (eds.) ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings. Frontiers in Artificial Intelligence and Applications, vol.\u00a0215, 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"},{"key":"16_CR26","doi-asserted-by":"publisher","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","DOI":"10.1145\/2093548.2093564"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Goues, C.L., Leino, K.R.M., Moskal, M.: The boogie verification debugger (toolpaper). In: Barthe, G., Pardo, A., Schneider, G. (eds.) Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a07041, 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":"16_CR28","doi-asserted-by":"publisher","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","DOI":"10.1136\/bmj.i1981"},{"key":"16_CR29","unstructured":"Grira, N., Crucianu, M., Boujemaa, N.: Unsupervised and semi-supervised clustering: a brief survey. A review of machine learning techniques for processing multimedia content 1, 9\u201316 (2004)"},{"key":"16_CR30","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"},{"key":"16_CR31","unstructured":"Hadarean, L., Hyv\u00e4rinen, A., Niemetz, A., Reger, G.: Smt-comp 2019. https:\/\/www.smt-comp.org\/2019 (2019)"},{"key":"16_CR32","doi-asserted-by":"publisher","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","DOI":"10.1137\/090771806"},{"key":"16_CR33","doi-asserted-by":"publisher","unstructured":"Healy, A., Monahan, R., Power, J.F.: Predicting SMT solver performance for software verification. In: Dubois, C., Masci, P., M\u00e9ry, D. (eds.) Proceedings of the Third Workshop on Formal Integrated Development Environment, F-IDE@FM 2016, Limassol, Cyprus, November 8, 2016. EPTCS, vol.\u00a0240, pp. 20\u201337 (2016). https:\/\/doi.org\/10.4204\/EPTCS.240.2","DOI":"10.4204\/EPTCS.240.2"},{"key":"16_CR34","doi-asserted-by":"publisher","unstructured":"Hurley, B., Kotthoff, L., Malitsky, Y., O\u2019Sullivan, B.: Proteus: A hierarchical portfolio of solvers and transformations. In: Simonis, H. (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.\u00a08451, 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"},{"key":"16_CR35","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: Majumdar, R., Kuncak, V. (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":"16_CR36","doi-asserted-by":"publisher","unstructured":"Kira, K., Rendell, L.A.: A practical approach to feature selection. In: Sleeman, D.H., Edwards, P. (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"},{"key":"16_CR37","doi-asserted-by":"publisher","unstructured":"Kotthoff, L.: Algorithm selection for combinatorial search problems: A survey. In: Bessiere, C., Raedt, L.D., Kotthoff, L., Nijssen, S., O\u2019Sullivan, B., Pedreschi, D. (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":"16_CR38","doi-asserted-by":"publisher","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","DOI":"10.1007\/s10586-017-1117-8"},{"key":"16_CR39","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Automating theorem proving with SMT. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07998, 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":"16_CR40","doi-asserted-by":"publisher","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Berre, D.L. (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.\u00a09710, 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":"16_CR41","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":"16_CR42","unstructured":"Marijn\u00a0Heule, Matti\u00a0J\u00e4rvisalo, M.S.: Sat race 2019 (2019), http:\/\/sat-race-2019.ciirc.cvut.cz\/"},{"key":"16_CR43","unstructured":"Moore, A.W.: Cross-validation for detecting and preventing overfitting. School of Computer Science Carneigie Mellon University (2001)"},{"key":"16_CR44","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (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.\u00a04963, 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"},{"key":"16_CR45","doi-asserted-by":"publisher","unstructured":"Nejati, S., Frioux, L.L., Ganesh, V.: A machine learning based splitting heuristic for divide-and-conquer solvers. In: Simonis, H. (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":"16_CR46","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla at the SMT-COMP 2020. CoRR abs\/2006.01621 (2020), https:\/\/arxiv.org\/abs\/2006.01621"},{"key":"16_CR47","doi-asserted-by":"publisher","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","DOI":"10.3233\/sat190101"},{"key":"16_CR48","doi-asserted-by":"publisher","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","DOI":"10.1007\/s10009-009-0118-1"},{"key":"16_CR49","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. Journal of Machine Learning Research 12, 2825\u20132830 (2011)"},{"key":"16_CR50","doi-asserted-by":"publisher","unstructured":"Pulina, L., Tacchella, A.: A multi-engine solver for quantified boolean formulas. In: Bessiere, C. (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.\u00a04741, 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":"16_CR51","doi-asserted-by":"publisher","unstructured":"Rice, J.R.: The algorithm selection problem. Adv. Comput. 15, 65\u2013118 (1976). https:\/\/doi.org\/10.1016\/S0065-2458(08)60520-3","DOI":"10.1016\/S0065-2458(08)60520-3"},{"key":"16_CR52","doi-asserted-by":"publisher","unstructured":"Richter, C., Wehrheim, H.: Pesco: Predicting sequential combinations of verifiers - (competition contribution). In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (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\u2013233. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_19","DOI":"10.1007\/978-3-030-17502-3_19"},{"key":"16_CR53","unstructured":"Rintanen, J.: Madagascar: Scalable planning with sat. Proceedings of the 8th International Planning Competition (IPC-2014) 21 (2014)"},{"key":"16_CR54","doi-asserted-by":"publisher","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","DOI":"10.1109\/TPAMI.2009.187"},{"key":"16_CR55","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: Badger, J.M., Rozier, K.Y. (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":"16_CR56","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"},{"key":"16_CR57","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":"16_CR58","doi-asserted-by":"publisher","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: Starexec: A cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (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.\u00a08562, 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":"16_CR59","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure - from CNF to th0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","DOI":"10.1007\/s10817-017-9407-7"},{"key":"16_CR60","doi-asserted-by":"publisher","unstructured":"Tierney, K., Malitsky, Y.: An algorithm selection benchmark of the container pre-marshalling problem. In: Dhaenens, C., Jourdan, L., Marmion, M. (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.\u00a08994, 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"},{"key":"16_CR61","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: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. Lecture Notes in Computer Science, vol.\u00a05195, 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":"16_CR62","doi-asserted-by":"publisher","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","DOI":"10.3233\/AIC-150671"},{"key":"16_CR63","unstructured":"Van Der\u00a0Maaten, L., Postma, E., Van\u00a0den Herik, J.: Dimensionality reduction: a comparative. J Mach Learn Res 10(66-71), \u00a013 (2009)"},{"key":"16_CR64","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 (01 2019). https:\/\/doi.org\/10.14722\/bar.2019.23080","DOI":"10.14722\/bar.2019.23080"},{"key":"16_CR65","unstructured":"Weston, J., Mukherjee, S., Chapelle, O., Pontil, M., Poggio, T.A., Vapnik, V.: Feature selection for svms. In: Leen, T.K., Dietterich, T.G., Tresp, V. (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":"16_CR66","doi-asserted-by":"crossref","unstructured":"Wold, S., Esbensen, K., Geladi, P.: Principal component analysis. Chemometrics and intelligent laboratory systems 2(1-3), 37\u201352 (1987)","DOI":"10.1016\/0169-7439(87)80084-9"},{"key":"16_CR67","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: Bessiere, C. (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.\u00a04741, 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":"16_CR68","doi-asserted-by":"publisher","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","DOI":"10.1613\/jair.2490"},{"key":"16_CR69","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla2009: an automatic algorithm portfolio for sat. SAT 4, 53\u201355 (2009)"},{"key":"16_CR70","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: Cimatti, A., Sebastiani, R. (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.\u00a07317, 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"},{"key":"16_CR71","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)"},{"key":"16_CR72","doi-asserted-by":"publisher","unstructured":"Xu, R., II, D.C.W.: Survey of clustering algorithms. IEEE Trans. Neural Networks 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"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72013-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:13:29Z","timestamp":1616436809000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":72,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}