{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,27]],"date-time":"2026-10-27T14:56:09Z","timestamp":1793112969510,"version":"4.5.0"},"publisher-location":"Cham","reference-count":116,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656262","type":"print"},{"value":"9783031656279","type":"electronic"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The SAT solver CaDiCaL provides a rich feature set with a clean library interface. It has been adopted by many users, is well documented and easy to extend due to its effective testing and debugging infrastructure. In this tool paper we give a high-level introduction into the solver architecture and then go briefly over implemented techniques. We describe basic features and novel advanced usage scenarios. Experiments confirm that CaDiCaL despite this flexibility has state-of-the-art performance both in a stand-alone as well as incremental setting.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_7","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"133-152","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":66,"title":["CaDiCaL 2.0"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0864-077X","authenticated-orcid":false,"given":"Tobias","family":"Faller","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0497-3059","authenticated-orcid":false,"given":"Katalin","family":"Fazekas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1705-3083","authenticated-orcid":false,"given":"Mathias","family":"Fleury","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3925-3438","authenticated-orcid":false,"given":"Nils","family":"Froleyks","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-4337-6919","authenticated-orcid":false,"given":"Florian","family":"Pollitt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Andersson, G., Bjesse, P., Cook, B., Hanna, Z.: A proof engine approach to solving combinational design automation problems. In: Proceedings of the 39th Design Automation Conference, DAC 2002, New Orleans, LA, USA, 10\u201314 June 2002, pp. 725\u2013730. ACM (2002). https:\/\/doi.org\/10.1145\/513918.514101","DOI":"10.1145\/513918.514101"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38916-0_3","volume-title":"Tests and Proofs","author":"C Artho","year":"2013","unstructured":"Artho, C., Biere, A., Seidl, M.: Model-based testing for verification back-ends. In: Veanes, M., Vigan\u00f2, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 39\u201355. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38916-0_3"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-39071-5_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"G Audemard","year":"2013","unstructured":"Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309\u2013317. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_23"},{"key":"7_CR4","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, 11\u201317 July 2009, pp. 399\u2013404. Morgan Kaufmann Publishers Inc., San Francisco (2009). http:\/\/ijcai.org\/Proceedings\/09\/Papers\/074.pdf"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Audemard, G., Simon, L.: On the glucose SAT solver. Int. J. Artif. Intell. Tools 27(1), 1840001:1\u20131840001:25 (2018). https:\/\/doi.org\/10.1142\/S0218213018400018","DOI":"10.1142\/S0218213018400018"},{"key":"7_CR6","unstructured":"Bacchus, F.: MaxHS in the 2022 MaxSat evaluation. In: Bacchus, F., Berg, J., J\u00e4rvisalo, M., Martins, R. (eds.) Proceedings\u00a0of MaxSAT Evaluation 2020 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2022-2, p.\u00a017. University of Helsinki (2022)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-030-72016-2_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Baek","year":"2021","unstructured":"Baek, S., Carneiro, M., Heule, M.J.H.: A flexible proof format for SAT solver-elaborator communication. In: TACAS 2021. LNCS, vol. 12651, pp. 59\u201375. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_4"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.artint.2016.08.007","volume":"241","author":"T Balyo","year":"2016","unstructured":"Balyo, T., Biere, A., Iser, M., Sinz, C.: SAT race 2015. Artif. Intell. 241, 45\u201365 (2016)","journal-title":"Artif. Intell."},{"key":"7_CR9","unstructured":"Balyo, T., Heule, M.J.H., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.): Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Series of Publications B, Department of Computer Science, University of Helsinki, Finland (2023)"},{"key":"7_CR10","unstructured":"Balyo, T., Heule, M.J.H. (eds.): Proceedings of SAT Competition 2016 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2016-1. University of Helsinki (2016)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-030-51074-9_3","volume-title":"Automated Reasoning","author":"LA Barnett","year":"2020","unstructured":"Barnett, L.A., Cerna, D., Biere, A.: Covered clauses are not propagation redundant. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 32\u201347. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_3"},{"key":"7_CR13","unstructured":"Belov, A., Marques-Silva, J.: Accelerating MUS extraction with recursive model rotation. In: Bjesse, P., Slobodov\u00e1, A. (eds.) International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911, Austin, TX, USA, 30 October\u201302 November 2011, pp. 37\u201340. FMCAD Inc. (2011)"},{"key":"7_CR14","unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT competition 2017. In: Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M. (eds.) Proceedings\u00a0of SAT Competition 2017 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2017-1, pp. 14\u201315. University of Helsinki (2017)"},{"key":"7_CR15","unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT competition 2018. In: Heule, M.J.H., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2018 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2018-1, pp. 13\u201314. University of Helsinki (2018)"},{"key":"7_CR16","unstructured":"Biere, A.: CaDiCaL at the SAT race 2019. In: Heule, M.J.H., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings\u00a0of SAT Race 2019 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2019-1, pp.\u00a08\u20139. University of Helsinki (2019)"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Biere, A., Chowdhury, M.S., Heule, M.J.H., Kiesl, B., Whalen, M.W.: Migrating solver state. In: SAT. LIPIcs, vol.\u00a0236, pp. 27:1\u201327:24. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2022.27","DOI":"10.4230\/LIPICS.SAT.2022.27"},{"key":"7_CR18","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In: Balyo, T., Froleyks, N., Heule, M.J.H., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings\u00a0of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020)"},{"key":"7_CR19","unstructured":"Biere, A., Fleury, M.: Gimsatul, IsaSAT and Kissat entering the SAT competition 2022. In: Balyo, T., Heule, M.J.H., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc.\u00a0of SAT Competition 2022 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2022-1, pp. 10\u201311. University of Helsinki (2022)"},{"key":"7_CR20","unstructured":"Biere, A., Fleury, M., Froleyks, N., Heule, M.J.: The SAT museum. In: J\u00e4rvisalo, M., Le\u00a0Berre, D. (eds.) Proceedings of the 14th International Workshop on Pragmatics of SAT Co-located with the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), Alghero, Italy, 4 July 2023. CEUR Workshop Proceedings, vol.\u00a03545, pp. 72\u201387. CEUR-WS.org (2023). http:\/\/ceur-ws.org\/Vol-3545\/paper6.pdf"},{"key":"7_CR21","unstructured":"Biere, A., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba entering the SAT competition 2021. In: Balyo, T., Froleyks, N., Heule, M.J.H., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings\u00a0of SAT Competition 2021 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2021-1, pp. 10\u201313. University of Helsinki (2021)"},{"key":"7_CR22","unstructured":"Biere, A., Fleury, M., Pollitt, F.: CaDiCaL_vivinst, IsaSAT, Gimsatul, Kissat, and Tabulara SAT entering the SAT competition 2023. In: Balyo, T., Froleyks, N., Heule, M.J.H., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings\u00a0of SAT Competition 2023 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2023-1, pp. 14\u201315. University of Helsinki (2023)"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Biere, A., Froleyks, N., Wang, W.: CadiBack: extracting backbones with CaDiCaL. In: Mahajan, M., Slivovsky, F. (eds.) 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, Alghero, Italy, 4\u20138 July 2023. LIPIcs, vol.\u00a0271, pp. 3:1\u20133:12. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2023.3","DOI":"10.4230\/LIPICS.SAT.2023.3"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Biere, A., J\u00e4rvisalo, M., Kiesl, B.: Preprocessing in SAT solving. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, 2nd edn., vol.\u00a0336, pp. 391\u2013435. IOS Press (2021)","DOI":"10.3233\/FAIA336"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition 2017. In: 2017 Formal Methods in Computer Aided Design (FMCAD), pp.\u00a09\u20139. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102233"},{"key":"7_CR26","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-031-24950-1_5","volume-title":"VMCAI","author":"NS Bj\u00f8rner","year":"2023","unstructured":"Bj\u00f8rner, N.S., Eisenhofer, C., Kov\u00e1cs, L.: Satisfiability modulo custom theories in Z3. In: Dragoi, C., Emmi, M., Wang, J. (eds.) VMCAI. LNCS, vol. 13881, pp. 91\u2013105. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_5"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-96142-2_6","volume-title":"Computer Aided Verification","author":"D Blotsky","year":"2018","unstructured":"Blotsky, D., Mora, F., Berzish, M., Zheng, Y., Kabir, I., Ganesh, V.: StringFuzz: a fuzzer for string solvers. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 45\u201351. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_6"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Bogaerts, B., Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Certified symmetry and dominance breaking for combinatorial optimisation. J. Artif. Intell. Res. 77, 1539\u20131589 (2023)","DOI":"10.1613\/jair.1.14296"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Bringolf, M., Winterer, D., Su, Z.: Finding and understanding incompleteness bugs in SMT solvers. In: ASE, pp. 43:1\u201343:10. ACM (2022)","DOI":"10.1145\/3551349.3560435"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-14186-7_6","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"R Brummayer","year":"2010","unstructured":"Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44\u201357. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_6"},{"key":"7_CR32","doi-asserted-by":"publisher","first-page":"1515","DOI":"10.1613\/jair.1.13666","volume":"74","author":"S Cai","year":"2022","unstructured":"Cai, S., Zhang, X., Fleury, M., Biere, A.: Better decision heuristics in CDCL through local search and target phases. J. Artif. Intell. Res. 74, 1515\u20131563 (2022). https:\/\/doi.org\/10.1613\/jair.1.13666","journal-title":"J. Artif. Intell. Res."},{"key":"7_CR33","unstructured":"Chen, J.: optsat, abcdsat and solvers based on simplified data structure and hybrid solving strategies. In: Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, p.\u00a025 (2020)"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-319-63046-5_14","volume-title":"Automated Deduction \u2013 CADE 26","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 220\u2013236. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_14"},{"key":"7_CR35","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":"7_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11499107_5"},{"key":"7_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"7_CR38","doi-asserted-by":"publisher","unstructured":"Faller, T., Deligiannis, N.I., Schw\u00f6rer, M., Reorda, M.S., Becker, B.: Constraint-based automatic SBST generation for RISC-V processor families. In: IEEE European Test Symposium, ETS 2023, Venezia, Italy, 22\u201326 May 2023, pp.\u00a01\u20136. IEEE (2023).https:\/\/doi.org\/10.1109\/ETS56758.2023.10174156","DOI":"10.1109\/ETS56758.2023.10174156"},{"key":"7_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-030-24258-9_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"K Fazekas","year":"2019","unstructured":"Fazekas, K., Biere, A., Scholl, C.: Incremental inprocessing in SAT solving. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 136\u2013154. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_9"},{"key":"7_CR40","doi-asserted-by":"publisher","unstructured":"Fazekas, K., Niemetz, A., Preiner, M., Kirchweger, M., Szeider, S., Biere, A.: IPASIR-UP: user propagators for CDCL. In: Mahajan, M., Slivovsky, F. (eds.) 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, Alghero, Italy. LIPIcs, vol.\u00a0271, pp. 8:1\u20138:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2023.8","DOI":"10.4230\/LIPICS.SAT.2023.8"},{"key":"7_CR41","unstructured":"Fazekas, K., Pollitt, F., Fleury, M., Biere, A.: Certifying incremental sat solving. In: Bjorner, N., Heule, M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 25th International Conference, LPAR-25, Balaclava, Mauritius, 26\u201331 May 2024. Proceedings (2024)"},{"key":"7_CR42","unstructured":"Fazekas, K., Pollitt, F., Fleury, M., Biere, A.: Incremental proofs for bounded model checking. In: Kunz, W., Gro\u00dfe, D. (eds.) Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems, MBMV 2024, Kaiserslautern, Germany, 14\u201315 February 2023. ITG Fachberichte, VDE Verlag (2024)"},{"key":"7_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-030-51825-7_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2020","author":"N Feng","year":"2020","unstructured":"Feng, N., Bacchus, F.: Clause size reduction with all-UIP learning. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 28\u201345. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_3"},{"key":"7_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-030-80223-3_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2021","author":"M Fleury","year":"2021","unstructured":"Fleury, M., Biere, A.: Efficient All-UIP learned clause minimization. In: Li, C.-M., Many\u00e0, F. (eds.) SAT 2021. LNCS, vol. 12831, pp. 171\u2013187. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_12"},{"key":"7_CR45","doi-asserted-by":"publisher","unstructured":"Fleury, M., Lammich, P.: A more pragmatic CDCL for isasat and targetting LLVM (short paper). In: Pientka, B., Tinelli, C. (eds.) Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, 1\u20134 July 2023, Proceedings. Lecture Notes in Computer Science, vol. 14132, pp. 207\u2013219. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_12","DOI":"10.1007\/978-3-031-38499-8_12"},{"key":"7_CR46","doi-asserted-by":"publisher","unstructured":"Froleyks, N., Biere, A.: Single clause assumption without activation literals to speed-up IC3. In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, 19\u201322 October 2021, pp. 72\u201376. IEEE (2021). https:\/\/doi.org\/10.34727\/2021\/ISBN.978-3-85448-046-4_15","DOI":"10.34727\/2021\/ISBN.978-3-85448-046-4_15"},{"key":"7_CR47","doi-asserted-by":"publisher","DOI":"10.1016\/J.ARTINT.2021.103572","volume":"301","author":"N Froleyks","year":"2021","unstructured":"Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M.: SAT competition 2020. Artif. Intell. 301, 103572 (2021). https:\/\/doi.org\/10.1016\/J.ARTINT.2021.103572","journal-title":"Artif. Intell."},{"key":"7_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-31612-8_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"V Ganesh","year":"2012","unstructured":"Ganesh, V., O\u2019Donnell, C.W., Soos, M., Devadas, S., Rinard, M.C., Solar-Lezama, A.: Lynx: a programmatic SAT solver for the RNA-folding problem. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 143\u2013156. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_12"},{"key":"7_CR49","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., Wanko, P.: Theory solving made easy with clingo 5. In: ICLP (Technical Communications). OASIcs, vol.\u00a052, pp. 2:1\u20132:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"key":"7_CR50","unstructured":"Gocht, S.: Certifying Correctness for Combinatorial Algorithms by Using Pseudo-Boolean Reasoning. Ph.D. thesis, Lund University, Lund, Sweden (2022). https:\/\/portal.research.lu.se\/en\/publications\/certifying-correctness-for-combinatorial-algorithms-by-using-pseu"},{"key":"7_CR51","doi-asserted-by":"crossref","unstructured":"Gocht, S., Nordstr\u00f6m, J.: Certifying parity reasoning efficiently using pseudo-Boolean proofs. In: Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI\u00a0\u201921), pp. 3768\u20133777 (2021)","DOI":"10.1609\/aaai.v35i5.16494"},{"key":"7_CR52","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for cnf formulas. In: 2003 Design, Automation and Test in Europe Conference and Exhibition, pp. 886\u2013891 (2003). https:\/\/api.semanticscholar.org\/CorpusID:10504432"},{"key":"7_CR53","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Vizel, Y.: DRUPing for interpolates. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21\u201324 October 2014, pp. 99\u2013106. IEEE (2014). https:\/\/doi.org\/10.1109\/FMCAD.2014.6987601","DOI":"10.1109\/FMCAD.2014.6987601"},{"key":"7_CR54","unstructured":"Haberlandt, A., Green, H.: SBVA-CADICAL and SBVA-KISSAT: structured bounded variable addition. In: Balyo, T., Froleyks, N., Heule, M.J.H., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc.\u00a0of SAT Competition 2023 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2023-1, p.\u00a018. University of Helsinki (2023)"},{"key":"7_CR55","doi-asserted-by":"publisher","unstructured":"Haberlandt, A., Green, H., Heule, M.J.H.: Effective auxiliary variables via structured reencoding. In: Mahajan, M., Slivovsky, F. (eds.) 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, Alghero, Italy. LIPIcs, 4\u20138 July 2023, vol.\u00a0271, pp. 11:1\u201311:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2023.11","DOI":"10.4230\/LIPICS.SAT.2023.11"},{"key":"7_CR56","doi-asserted-by":"publisher","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Learning for dynamic subsumption. In: ICTAI 2009, 21st IEEE International Conference on Tools with Artificial Intelligence, Newark, New Jersey, USA, 2\u20134 November 2009, pp. 328\u2013335. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/ICTAI.2009.22","DOI":"10.1109\/ICTAI.2009.22"},{"key":"7_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-02777-2_21","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"H Han","year":"2009","unstructured":"Han, H., Somenzi, F.: On-the-fly clause improvement. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 209\u2013222. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_21"},{"key":"7_CR58","doi-asserted-by":"crossref","unstructured":"Heule, M., Jr., W.A.H., Wetzler, N.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013, pp. 181\u2013188. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"7_CR59","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H.: Proofs of unsatisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 635\u2013668. IOS Press (2021).https:\/\/doi.org\/10.3233\/FAIA200998","DOI":"10.3233\/FAIA200998"},{"key":"7_CR60","unstructured":"Heule, M.J.H., Biere, A.: Proofs for satisfiability problems. In: All about Proofs, Proofs for All (APPA), Mathmatical, Logic and Foundations, vol.\u00a055. College Publication (2015)"},{"key":"7_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-16242-8_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Heule","year":"2010","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Clause elimination procedures for CNF formulas. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 357\u2013371. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_26"},{"key":"7_CR62","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Covered clause elimination. In: Voronkov, A., Sutcliffe, G., Baaz, M., Ferm\u00fcller, C.G. (eds.) Short papers for 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning, LPAR-17-short, Yogyakarta, Indonesia, 10\u201315 October 2010. EPiC Series in Computing, vol.\u00a013, pp. 41\u201346. EasyChair (2010). https:\/\/doi.org\/10.29007\/CL8S","DOI":"10.29007\/CL8S"},{"key":"7_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-38171-3_6","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"MJH Heule","year":"2013","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Revisiting hyper binary resolution. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 77\u201393. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38171-3_6"},{"key":"7_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-030-51825-7_4","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2020","author":"R Hickey","year":"2020","unstructured":"Hickey, R., Bacchus, F.: Trail saving on backtrack. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 46\u201361. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_4"},{"key":"7_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-319-94144-8_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"A Ignatiev","year":"2018","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a python toolkit for prototyping with SAT oracles. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 428\u2013437. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_26"},{"issue":"2","key":"7_CR66","doi-asserted-by":"publisher","first-page":"161","DOI":"10.3233\/AIC-140640","volume":"28","author":"M Janota","year":"2015","unstructured":"Janota, M., Lynce, I., Marques-Silva, J.: Algorithms for computing backbones of propositional formulae. AI Commun. 28(2), 161\u2013177 (2015). https:\/\/doi.org\/10.3233\/AIC-140640","journal-title":"AI Commun."},{"key":"7_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-642-14186-7_30","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"M J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A.: Reconstructing solutions after blocked clause elimination. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 340\u2013345. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_30"},{"key":"7_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-12002-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129\u2013144. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_10"},{"key":"7_CR69","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28"},{"key":"7_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-030-31784-3_3","volume-title":"Automated Technology for Verification and Analysis","author":"B Kiesl","year":"2019","unstructured":"Kiesl, B., Heule, M.J.H., Biere, A.: Truth assignments as conditional autarkies. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 48\u201364. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_3"},{"key":"7_CR71","doi-asserted-by":"publisher","unstructured":"Kiesl-Reiter, B., Whalen, M.W.: Proofs for incremental SAT with inprocessing. In: Nadel, A., Rozier, K.Y. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, 24\u201327 October 2023, pp. 132\u2013140. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_21","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_21"},{"key":"7_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-030-80223-3_20","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2021","author":"S Kochemazov","year":"2021","unstructured":"Kochemazov, S., Ignatiev, A., Marques-Silva, J.: Assessing progress in SAT solvers through the lens of incremental SAT. In: Li, C.-M., Many\u00e0, F. (eds.) SAT 2021. LNCS, vol. 12831, pp. 280\u2013298. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_20"},{"key":"7_CR73","unstructured":"Kupferschmid, S.: \u00dcber Craigsche Interpolation und deren Anwendung in der formalen Modellpr\u00fcfung. Ph.D. thesis, University of Freiburg (2013)"},{"issue":"2","key":"7_CR74","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/S10703-011-0122-4","volume":"39","author":"S Kupferschmid","year":"2011","unstructured":"Kupferschmid, S., Lewis, M., Schubert, T., Becker, B.: Incremental preprocessing methods for use in BMC. Formal Methods Syst. Des. 39(2), 185\u2013204 (2011). https:\/\/doi.org\/10.1007\/S10703-011-0122-4","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"7_CR75","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s10817-019-09525-z","volume":"64","author":"P Lammich","year":"2020","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reason. 64(3), 513\u2013532 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09525-z","journal-title":"J. Autom. Reason."},{"key":"7_CR76","unstructured":"Le\u00a0Berre, D., Roussel, O., Simon, L.: SAT competition 2009: Benchmark submission guidelines. https:\/\/web.archive.org\/web\/20190325181937\/https:\/\/www.satcompetition.org\/2009\/format-benchmarks2009.html. Accessed 15 Jan 2024"},{"key":"7_CR77","unstructured":"Li, C.M.: Integrating equivalency reasoning into Davis-Putnam procedure. In: Kautz, H.A., Porter, B.W. (eds.) Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on on Innovative Applications of Artificial Intelligence, Austin, Texas, USA, 30 July\u20133 August 2000, pp. 291\u2013296. AAAI Press\/The MIT Press (2000), http:\/\/www.aaai.org\/Library\/AAAI\/2000\/aaai00-045.php"},{"key":"7_CR78","doi-asserted-by":"publisher","unstructured":"Lohn, E., Lambert, C., Heule, M.J.H.: Compact symmetry breaking for tournaments. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, 17\u201321 October 2022, pp. 179\u2013188. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_24","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_24"},{"key":"7_CR79","doi-asserted-by":"publisher","unstructured":"Luo, M., Li, C., Xiao, F., Many\u00e0, F., L\u00fc, Z.: An effective learnt clause minimization approach for CDCL SAT solvers. In: Sierra, C. (ed.) Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, 19\u201325 August 2017, pp. 703\u2013711. ijcai.org (2017). https:\/\/doi.org\/10.24963\/IJCAI.2017\/98","DOI":"10.24963\/IJCAI.2017\/98"},{"key":"7_CR80","doi-asserted-by":"crossref","unstructured":"Mansur, M.N., Christakis, M., W\u00fcstholz, V., Zhang, F.: Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. In: ESEC\/SIGSOFT FSE, pp. 701\u2013712. ACM (2020)","DOI":"10.1145\/3368089.3409763"},{"key":"7_CR81","unstructured":"Manthey, N.: Riss 7 in proceedings of SAT competition 2020. In: Proceedings of SAT Competition 2020: Solver and benchmark descriptions (2020)"},{"key":"7_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-39611-3_14","volume-title":"Hardware and Software: Verification and Testing","author":"N Manthey","year":"2013","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of Boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 102\u2013117. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_14"},{"key":"7_CR83","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 133\u2013182. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA200987","DOI":"10.3233\/FAIA200987"},{"key":"7_CR84","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-030-24258-9_18","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"S M\u00f6hle","year":"2019","unstructured":"M\u00f6hle, S., Biere, A.: Backing backtracking. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 250\u2013266. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_18"},{"key":"7_CR85","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":"7_CR86","doi-asserted-by":"publisher","unstructured":"Nadel, A.: Introducing Intel(R) SAT Solver. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0236, pp. 8:1\u20138:23. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2022.8. https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2022\/16682","DOI":"10.4230\/LIPIcs.SAT.2022.8"},{"key":"7_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-31612-8_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 242\u2013255. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_19"},{"key":"7_CR88","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":"7_CR89","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-31612-8_20","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Preprocessing in incremental SAT. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 256\u2013269. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_20"},{"key":"7_CR90","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-319-09284-3_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"A Nadel","year":"2014","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Ultimately incremental SAT. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 206\u2013218. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_16"},{"issue":"5","key":"7_CR91","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/S00373-022-02560-5","volume":"38","author":"D Neiman","year":"2022","unstructured":"Neiman, D., Mackey, J., Heule, M.J.H.: Tighter bounds on directed ramsey number R(7). Graphs Comb. 38(5), 156 (2022). https:\/\/doi.org\/10.1007\/S00373-022-02560-5","journal-title":"Graphs Comb."},{"key":"7_CR92","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17\u201322 July 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 3\u201317. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_1","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"7_CR93","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Barrett, C.W.: Murxla: a modular and highly extensible API fuzzer for SMT solvers. In: Shoham, S., Vizel, Y. (eds.) CAV (2). Lecture Notes in Computer Science, vol. 13372, pp. 92\u2013106. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_5","DOI":"10.1007\/978-3-031-13188-2_5"},{"key":"7_CR94","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Model-based API testing for SMT solvers. In: SMT. CEUR Workshop Proceedings, vol.\u00a01889, pp. 3\u201314. CEUR-WS.org (2017)"},{"key":"7_CR95","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector at the SMT competition 2019. In: Hendrix, J., Sharygina, N. (eds.) Proceedings of the 17th International Workshop on Satisfiability Modulo Theories (SMT 2019), affiliated with the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 2019), Lisbon, Portugal, 7\u20138 July 2019, p. 2 (2019)"},{"key":"7_CR96","doi-asserted-by":"crossref","unstructured":"Park, J., Winterer, D., Zhang, C., Su, Z.: Generative type-aware mutation for testing SMT solvers. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201319 (2021)","DOI":"10.1145\/3485529"},{"key":"7_CR97","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-319-94144-8_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"T Paxian","year":"2018","unstructured":"Paxian, T., Reimer, S., Becker, B.: Dynamic polynomial watchdog encoding for solving weighted MaxSAT. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 37\u201353. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_3"},{"key":"7_CR98","doi-asserted-by":"publisher","unstructured":"Piette, C., Hamadi, Y., Sais, L.: Vivifying propositional clausal formulae. In: Ghallab, M., Spyropoulos, C.D., Fakotakis, N., Avouris, N.M. (eds.) ECAI 2008 - 18th European Conference on Artificial Intelligence, Patras, Greece, 21\u201325 July 2008, Proceedings. Frontiers in Artificial Intelligence and Applications, vol.\u00a0178, pp. 525\u2013529. IOS Press (2008). https:\/\/doi.org\/10.3233\/978-1-58603-891-5-525","DOI":"10.3233\/978-1-58603-891-5-525"},{"key":"7_CR99","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-72788-0_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"K Pipatsrisawat","year":"2007","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294\u2013299. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72788-0_28"},{"key":"7_CR100","doi-asserted-by":"publisher","unstructured":"Pollitt, F., Fleury, M., Biere, A.: Faster LRAT checking than solving with CaDiCaL. In: Mahajan, M., Slivovsky, F. (eds.) 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0271, pp. 21:1\u201321:12. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2023). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2023.21","DOI":"10.4230\/LIPIcs.SAT.2023.21"},{"key":"7_CR101","doi-asserted-by":"publisher","unstructured":"Sanders, P., Schreiber, D.: Mallob: scalable SAT solving on demand with decentralized job scheduling. J. Open Source Softw. 7(77), 4591 (2022). https:\/\/doi.org\/10.21105\/JOSS.04591","DOI":"10.21105\/JOSS.04591"},{"key":"7_CR102","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-030-90870-6_6","volume-title":"Formal Methods","author":"J Scott","year":"2021","unstructured":"Scott, J., Sudula, T., Rehman, H., Mora, F., Ganesh, V.: BanditFuzz: fuzzing SMT solvers with multi-agent reinforcement learning. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 103\u2013121. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_6"},{"key":"7_CR103","doi-asserted-by":"publisher","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Rutenbar, R.A., Otten, R.H.J.M. (eds.) Proceedings of the 1996 IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 1996, San Jose, CA, USA, 10\u201314 November 1996, pp. 220\u2013227. IEEE Computer Society\/ACM (1996). https:\/\/doi.org\/10.1109\/ICCAD.1996.569607","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"7_CR104","unstructured":"Soos, M., Devriendt, J., Gocht, S., Shaw, A., Meel, K.S.: CryptoMiniSat with ccanr at the SAT competition 2020. In: Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions 2020, vol. 27 (2020)"},{"key":"7_CR105","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-030-53288-8_22","volume-title":"Computer Aided Verification","author":"M Soos","year":"2020","unstructured":"Soos, M., Gocht, S., Meel, K.S.: Tinted, Detached, and Lazy CNF-XOR solving and its applications to counting and sampling. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 463\u2013484. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_22"},{"key":"7_CR106","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244\u2013257. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_24"},{"key":"7_CR107","unstructured":"Soos, M., Selman, B., Kautz, H., Devriendt, J., Gocht, S.: CryptoMiniSat with WalkSAT at the SAT competition 2020. In: Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, p.\u00a029 (2020)"},{"key":"7_CR108","doi-asserted-by":"publisher","unstructured":"Subercaseaux, B., Heule, M.J.H.: The packing chromatic number of the infinite square grid is 15. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, 22\u201327 April 2023, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13993, pp. 389\u2013406. Springer, Heidelberg (2023).https:\/\/doi.org\/10.1007\/978-3-031-30823-9_20","DOI":"10.1007\/978-3-031-30823-9_20"},{"key":"7_CR109","doi-asserted-by":"publisher","unstructured":"van der Tak, P., Ramos, A., Heule, M.J.H.: Reusing the assignment trail in CDCL solvers. J. Satisf. Boolean Model. Comput. 7(4), 133\u2013138 (2011). https:\/\/doi.org\/10.3233\/SAT190082","DOI":"10.3233\/SAT190082"},{"key":"7_CR110","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-030-72013-1_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"YK Tan","year":"2021","unstructured":"Tan, Y.K., Heule, M.J.H., Myreen, M.O.: cake_lpr: verified propagation redundancy checking in CakeML. In: TACAS 2021. LNCS, vol. 12652, pp. 223\u2013241. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_12"},{"key":"7_CR111","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"},{"key":"7_CR112","doi-asserted-by":"publisher","unstructured":"Whittemore, J., Kim, J., Sakallah, K.A.: SATIRE: a new incremental satisfiability engine. In: Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, 18\u201322 June 2001, pp. 542\u2013545. ACM (2001).https:\/\/doi.org\/10.1145\/378239.379019","DOI":"10.1145\/378239.379019"},{"key":"7_CR113","doi-asserted-by":"publisher","unstructured":"Wieringa, S., Niemenmaa, M., Heljanko, K.: Tarmo: A framework for parallelized bounded model checking. In: Brim, L., van\u00a0de Pol, J. (eds.) Proceedings 8th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2009, Eindhoven, The Netherlands, 4 November 2009. EPTCS, vol.\u00a014, pp. 62\u201376 (2009). https:\/\/doi.org\/10.4204\/EPTCS.14.5","DOI":"10.4204\/EPTCS.14.5"},{"issue":"2","key":"7_CR114","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/S10817-022-09658-8","volume":"67","author":"E Yolcu","year":"2023","unstructured":"Yolcu, E., Aaronson, S., Heule, M.J.H.: An automated approach to the collatz conjecture. J. Autom. Reason. 67(2), 15 (2023). https:\/\/doi.org\/10.1007\/S10817-022-09658-8","journal-title":"J. Autom. Reason."},{"key":"7_CR115","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/11499107_42","volume-title":"Theory and Applications of Satisfiability Testing","author":"L Zhang","year":"2005","unstructured":"Zhang, L.: On subsumption removal and on-the-fly CNF simplification. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 482\u2013489. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11499107_42"},{"key":"7_CR116","doi-asserted-by":"publisher","unstructured":"Zhang, T., Szeider, S.: Searching for smallest universal graphs and tournaments with SAT. In: Yap, R.H.C. (ed.) 29th International Conference on Principles and Practice of Constraint Programming, CP 2023, Toronto, Canada, 27\u201331 August 2023. LIPIcs, vol.\u00a0280, pp. 39:1\u201339:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.CP.2023.39","DOI":"10.4230\/LIPICS.CP.2023.39"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65627-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:02:28Z","timestamp":1721934148000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":116,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}