{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:06:52Z","timestamp":1742911612796,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031660634"},{"type":"electronic","value":"9783031660641"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-66064-1_1","type":"book-chapter","created":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T10:02:00Z","timestamp":1721988120000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Picky CDCL: SMT-Solving with\u00a0Flexible Literal Selection"],"prefix":"10.1007","author":[{"given":"Konstantin I.","family":"Britikov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antti E. J.","family":"Hyv\u00e4rinen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,27]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-29613-5_1","volume-title":"Verified Software: Theories, Tools, and Experiments","author":"L Alt","year":"2016","unstructured":"Alt, L., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: A proof-sensitive approach for small propositional interpolants. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 1\u201318. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29613-5_1"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: Flexible proof production in an industrial-strength SMT solver. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Proceedings of the 11th International Joint Conference on Automated Reasoning, IJCAR 2022, Haifa, Israel, 8\u201310 August 2022. LNCS, vol. 13385, pp. 15\u201335. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_3","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11513988_4","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2005","unstructured":"Barrett, C., de Moura, L., Stump, A.: SMT-COMP: satisfiability modulo theories competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 20\u201323. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_4"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Barrett","year":"2006","unstructured":"Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512\u2013526. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11916277_35"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Blicha, M., Britikov, K., Sharygina, N.: The golem Horn solver. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, CAV 2023. LNCS, vol. 13965, pp. 209\u2013223. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_10","DOI":"10.1007\/978-3-031-37703-7_10"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Blicha, M., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Split transition power abstraction for unbounded safety. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, 17\u201321 October 2022, pp. 349\u2013358. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_42","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_42"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-17462-0_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Blicha","year":"2019","unstructured":"Blicha, M., Hyv\u00e4rinen, A.E.J., Kofro\u0148, J., Sharygina, N.: Decomposing Farkas interpolants. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019, Part I. LNCS, vol. 11427, pp. 3\u201320. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_1"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/BF02127976","volume":"17","author":"M B\u00f6hm","year":"1996","unstructured":"B\u00f6hm, M., Speckenmeyer, E.: A fast parallel SAT-solver - efficient workload balancing. Ann. Math. Artif. Intell. 17, 381\u2013400 (1996). https:\/\/doi.org\/10.1007\/BF02127976","journal-title":"Ann. Math. Artif. Intell."},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-12002-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150\u2013153. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_12"},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22, 269\u2013285 (1957). https:\/\/doi.org\/10.2307\/2963594","journal-title":"J. Symb. Log."},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5, 394\u2013397 (1962). https:\/\/doi.org\/10.1145\/368273.368557","journal-title":"Commun. ACM"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"De Angelis, E., Hari Govind, V.K.: CHC-COMP 2022: competition report. In: Hamilton, G.W., Kahsai, T., Proietti, M. (eds.) Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation, HCVS\/VPT@ETAPS 2022 and 10th International Workshop on Verification and Program Transformation, Munich, Germany, 3 April 2022, EPTCS, vol.\u00a0373, pp. 44\u201362 (2022). https:\/\/doi.org\/10.4204\/EPTCS.373.5","DOI":"10.4204\/EPTCS.373.5"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-642-11957-6_11","volume-title":"Programming Languages and Systems","author":"V D\u2019Silva","year":"2010","unstructured":"D\u2019Silva, V.: Propositional interpolation and abstract interpretation. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 185\u2013204. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_11"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A.: Program verification with constrained horn clauses (invited paper). In: Shoham, S., Vizel, Y. (eds.) Proceedings of the 34th International Conference on Computer Aided Verification, CAV 2022, Part I. LNCS, Haifa, Israel, 7\u201310 August 2022, vol. 13371, pp. 19\u201329. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_2","DOI":"10.1007\/978-3-031-13185-1_2"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"MJH Heule","year":"2012","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50\u201365. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_8"},{"key":"1_CR16","unstructured":"Heule, M.J.H.: The DRAT format and drat-trim checker. CoRR abs\/1610.06229 (2016)"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., van Maaren, H.: Look-ahead based SAT solvers, 2nd edn. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 183\u2013212. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA200988","DOI":"10.3233\/FAIA200988"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA horn solver. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, 30 October\u20132 November 2018, pp.\u00a01\u20137. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-319-40970-2_35","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"AEJ Hyv\u00e4rinen","year":"2016","unstructured":"Hyv\u00e4rinen, A.E.J., Marescotti, M., Alt, L., Sharygina, N.: OpenSMT2: an SMT solver for multi-core and cloud computing. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 547\u2013553. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_35"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Hyv\u00e4rinen, A.E.J., Marescotti, M., Sadigova, P., Chockler, H., Sharygina, N.: Lookahead-based SMT solving. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-22. EPiC Series in Computing, Awassa, Ethiopia, 16\u201321 November 2018, vol.\u00a057, pp. 418\u2013434. EasyChair (2018). https:\/\/doi.org\/10.29007\/gzzf","DOI":"10.29007\/gzzf"},{"key":"1_CR21","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Meth. Syst. Des. 48, 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Formal Meth. Syst. Des."},{"issue":"4","key":"1_CR22","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/s00165-019-00486-z","volume":"31","author":"I Konnov","year":"2019","unstructured":"Konnov, I.: Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds):Handbook of model checking. Formal Aspects Comput. 31(4), 455\u2013456 (2019). https:\/\/doi.org\/10.1007\/s00165-019-00486-z","journal-title":"Formal Aspects Comput."},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of Craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1\u201312. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_1"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_14"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, 18\u201322 June 2001, pp. 530\u2013535. ACM (2001). https:\/\/doi.org\/10.1145\/378239.379017","DOI":"10.1145\/378239.379017"},{"key":"1_CR27","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":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-319-94144-8_7","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"A Nadel","year":"2018","unstructured":"Nadel, A., Ryvchin, V.: Chronological backtracking. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 111\u2013121. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_7"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-24318-4_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"C Oh","year":"2015","unstructured":"Oh, C.: Between SAT and UNSAT: the fundamental difference in CDCL SAT. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 307\u2013323. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_23"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Otoni, R., Blicha, M., Eugster, P., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Theory-specific proof steps witnessing correctness of SMT executions. In: 58th ACM\/IEEE Design Automation Conference, DAC 2021, San Francisco, CA, USA, 5\u20139 December 2021, pp. 541\u2013546. IEEE (2021). https:\/\/doi.org\/10.1109\/DAC18074.2021.9586272","DOI":"10.1109\/DAC18074.2021.9586272"},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Silva, J.P.M., Sakallah, K.A.: Conflict analysis in search algorithms for satisfiability. In: Eigth International Conference on Tools with Artificial Intelligence, ICTAI \u201996, Toulouse, France, 16\u201319 November 1996, pp. 467\u2013469. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/TAI.1996.560789","DOI":"10.1109\/TAI.1996.560789"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"},{"issue":"7","key":"1_CR33","doi-asserted-by":"publisher","first-page":"72103:1","DOI":"10.1007\/s11432-017-9467-7","volume":"62","author":"F Xiao","year":"2019","unstructured":"Xiao, F., Li, C.-M., Luo, M., Many\u00e0, F., L\u00fc, Z., Li, Yu.: A branching heuristic for SAT solvers based on complete implication graphs. Sci. China Inf. Sci. 62(7), 72103:1-72103:13 (2019). https:\/\/doi.org\/10.1007\/s11432-017-9467-7","journal-title":"Sci. China Inf. Sci."}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66064-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T10:03:19Z","timestamp":1721988199000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66064-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031660634","9783031660641"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66064-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"27 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ames, IA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/homepage.cs.uiowa.edu\/~ajreynol\/VSTTE2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}