{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:00Z","timestamp":1776333480514,"version":"3.51.2"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030802226","type":"print"},{"value":"9783030802233","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:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_31","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"453-470","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["MedleySolver: Online SMT Algorithm Selection"],"prefix":"10.1007","author":[{"given":"Nikhil","family":"Pimpalkhare","sequence":"first","affiliation":[]},{"given":"Federico","family":"Mora","sequence":"additional","affiliation":[]},{"given":"Elizabeth","family":"Polgreen","sequence":"additional","affiliation":[]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"31_CR1","unstructured":"Agrawal, S., Goyal, N.: Analysis of Thompson sampling for the multi-armed bandit problem. In: COLT. JMLR Proceedings, vol. 23, pp. 39.1\u201339.26. JMLR.org (2012)"},{"key":"31_CR2","unstructured":"Agrawal, S., Goyal, N.: Thompson sampling for contextual bandits with linear payoffs. In: ICML (3). JMLR Workshop and Conference Proceedings, vol. 28, pp. 127\u2013135. JMLR.org (2013)"},{"issue":"1","key":"31_CR3","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1137\/S0097539701398375","volume":"32","author":"P Auer","year":"2002","unstructured":"Auer, P., Cesa-Bianchi, N., Freund, Y., Schapire, R.E.: The nonstochastic multiarmed bandit problem. SIAM J. Comput. 32(1), 48\u201377 (2002)","journal-title":"SIAM J. Comput."},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Backes, J., et al.: Semantic-based automated reasoning for AWS access policies using SMT. In: FMCAD, pp. 1\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"31_CR5","unstructured":"Balunovic, M., Bielik, P., Vechev, M.T.: Learning to solve SMT formulas. In: NeurIPS, pp. 10338\u201310349 (2018)"},{"key":"31_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"31_CR7","unstructured":"Barth, M., Dietsch, D., Fichtner, L., Heizmann, M.: Ultimate eliminator: a quantifier upgrade for smt solvers at smt-comp 2019 (2019)"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N.: SMT solvers for testing, program analysis and verification at microsoft. In: SYNASC, p. 15. IEEE Computer Society (2009)","DOI":"10.1109\/SYNASC.2009.64"},{"key":"31_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The MathSAT\u00a04 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299\u2013303. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_28"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-540-71209-1_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RE Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 358\u2013372. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_28"},{"key":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"RE Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78\u201392. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_7"},{"issue":"1","key":"31_CR12","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1023\/A:1007372016040","volume":"26","author":"EF Castillo","year":"1997","unstructured":"Castillo, E.F., Hadi, A.S., Solares, C.: Learning and updating of uncertainty in dirichlet models. Mach. Learn. 26(1), 43\u201363 (1997)","journal-title":"Mach. Learn."},{"key":"31_CR13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511546921","volume-title":"Prediction, Learning, and Games","author":"N Cesa-Bianchi","year":"2006","unstructured":"Cesa-Bianchi, N., Lugosi, G.: Prediction, Learning, and Games. Cambridge University Press, Cambridge (2006)"},{"key":"31_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"31_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"31_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25"},{"key":"31_CR17","unstructured":"Hansen, T.: A constraint solver and its application to machine code test generation. Ph.D. thesis, University of Melbourne, Australia (2012). http:\/\/hdl.handle.net\/11343\/37952"},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"Healy, A., Monahan, R., Power, J.F.: Predicting SMT solver performance for software verification. In: F-IDE@FM. EPTCS, vol. 240, pp. 20\u201337 (2016)","DOI":"10.4204\/EPTCS.240.2"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Hutter, F., Babic, D., Hoos, H.H., Hu, A.J.: Boosting verification by automatic tuning of decision procedures. In: 7th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 27\u201334 (2007)","DOI":"10.1109\/FMCAD.2007.4401979"},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1007\/978-3-642-02658-4_53","volume-title":"Computer Aided Verification","author":"S Jha","year":"2009","unstructured":"Jha, S., Limaye, R., Seshia, S.A.: Beaver: engineering an efficient SMT solver for bit-vector arithmetic. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 668\u2013674. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_53"},{"key":"31_CR21","unstructured":"Johnson, J.D., Li, J., Chen, Z.: Reinforcement Learning: An Introduction: Sutton, R.S., Barto, A.G. MIT press, Cambridge, MA 1998, 322, ISBN 0-262-19398-1. Neurocomputing 35(1-4), 205\u2013206 (2000)"},{"key":"31_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-319-40970-2_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"M Jon\u00e1\u0161","year":"2016","unstructured":"Jon\u00e1\u0161, M., Strej\u010dek, J.: Solving quantified bit-vector formulas using binary decision diagrams. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 267\u2013283. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_17"},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 260\u2013270 (2017)","DOI":"10.1145\/3009837.3009887"},{"key":"31_CR24","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3","volume-title":"Decision Procedures - An Algorithmic Point of View","author":"D Kroening","year":"2016","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series, Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-540-74105-3"},{"key":"31_CR25","unstructured":"Lazaar, N., Hamadi, Y., Jabbour, S., Sebag, M.: BESS: Bandit Ensemble for parallel SAT Solving. Research Report RR-8070 (2012). https:\/\/hal.inria.fr\/hal-00733282"},{"key":"31_CR26","doi-asserted-by":"crossref","unstructured":"Li, L., Chu, W., Langford, J., Schapire, R.E.: A contextual-bandit approach to personalized news article recommendation. In: Proceedings of the 19th international conference on World Wide Web, pp. 661\u2013670. ACM (2010)","DOI":"10.1145\/1772690.1772758"},{"key":"31_CR27","doi-asserted-by":"crossref","unstructured":"L\u00f6ding, C., Madhusudan, P., Pe\u00f1a, L.: Foundations for natural proofs and quantifier instantiation. In: Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, pp. 1\u201330 (2017)","DOI":"10.1145\/3158098"},{"key":"31_CR28","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/j.procs.2017.05.140","volume":"108","author":"T Menouer","year":"2017","unstructured":"Menouer, T., Baarir, S.: Parallel learning portfolio-based solvers. Procedia Comput. Sci. 108, 335\u2013344 (2017)","journal-title":"Procedia Comput. Sci."},{"issue":"1","key":"31_CR29","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/S0022-2496(02)00028-7","volume":"47","author":"IJ Myung","year":"2003","unstructured":"Myung, I.J.: Tutorial on maximum likelihood estimation. J. Math. Psychol. 47(1), 90\u2013100 (2003). https:\/\/doi.org\/10.1016\/S0022-2496(02)00028-7","journal-title":"J. Math. Psychol."},{"key":"31_CR30","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla at the SMT-COMP 2020 (2020). CoRR abs\/2006.01621, https:\/\/arxiv.org\/abs\/2006.01621"},{"key":"31_CR31","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"},{"issue":"4","key":"31_CR32","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/s10462-011-9290-2","volume":"40","author":"M Nikolic","year":"2013","unstructured":"Nikolic, M., Maric, F., Janicic, P.: Simple algorithm portfolio for SAT. Artif. Intell. Rev. 40(4), 457\u2013465 (2013)","journal-title":"Artif. Intell. Rev."},{"key":"31_CR33","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)"},{"key":"31_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-319-21668-3_12","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 198\u2013216. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_12"},{"key":"31_CR35","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: Groote, J.F., Larsen, K.G. (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, 27 March\u20131 April 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12652, pp. 303\u2013325. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_16","DOI":"10.1007\/978-3-030-72013-1_16"},{"key":"31_CR36","unstructured":"Seshia, S.A.: Adaptive Eager Boolean Encoding for Arithmetic Reasoning in Verification. Ph.D. thesis, Carnegie Mellon University (2005)"},{"key":"31_CR37","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Subramanyan, P.: UCLID5: integrating modeling, verification, synthesis and learning. In: MEMOCODE, pp. 1\u201310. IEEE (2018)","DOI":"10.1109\/MEMCOD.2018.8556946"},{"key":"31_CR38","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415. ACM (2006)","DOI":"10.1145\/1168919.1168907"},{"key":"31_CR39","unstructured":"Wattez, H., Koriche, F., Lecoutre, C., Paparrizou, A., Tabary, S.: Learning variable ordering heuristics with multi-armed bandits and restarts. In: ECAI. Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 371\u2013378. IOS Press (2020)"},{"key":"31_CR40","unstructured":"Weber, T.: Par4 system description. https:\/\/smt-comp.github.io\/2019\/system-descriptions\/Par4.pdf"},{"issue":"1","key":"31_CR41","first-page":"221","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)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"31_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"715","DOI":"10.1007\/978-3-642-02658-4_60","volume-title":"Computer Aided Verification","author":"CM Wintersteiger","year":"2009","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.: A concurrent portfolio approach to SMT solving. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 715\u2013720. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_60"},{"key":"31_CR43","doi-asserted-by":"crossref","unstructured":"Xia, W., Yap, R.H.C.: Learning robust search strategies using a bandit-based approach. In: AAAI, pp. 6657\u20136665. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.12211"},{"key":"31_CR44","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)","journal-title":"J. Artif. Intell. Res."},{"key":"31_CR45","unstructured":"Zhou, D., Li, L., Gu, Q.: Neural contextual bandits with upper confidence bound-based exploration (2019). CoRR abs\/1911.04462"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T09:45:26Z","timestamp":1672652726000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_31","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":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","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":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}