{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:21:18Z","timestamp":1779074478761,"version":"3.51.4"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986673","type":"print"},{"value":"9783031986680","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    The IC3 algorithm, also known as PDR, is a SAT-based model checking algorithm that has significantly influenced the field in recent years due to its efficiency, scalability, and completeness. It utilizes SAT solvers to solve a series of SAT queries associated with relative induction. In this paper, we introduce several optimizations for the SAT solver in IC3 based on our observations of the unique characteristics of these SAT queries. By observing that SAT queries do not necessarily require decisions on all variables, we compute a subset of variables that need to be decided before each solving process while ensuring that the result remains unaffected. Additionally, noting that the overhead of binary heap operations in VSIDS is non-negligible, we replace the binary heap with buckets to achieve constant-time operations. Furthermore, we support temporary clauses without the need to allocate a new activation variable for each solving process, thereby eliminating the need to reset solvers. We developed a novel lightweight CDCL SAT solver, GipSAT, which integrates these optimizations. A comprehensive evaluation highlights the performance improvements achieved by GipSAT. Specifically, the GipSAT-based IC3 demonstrates an average speedup of\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$3.61$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mn>3.61<\/mml:mn>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    times in solving time compared to the IC3 implementation based on MiniSat.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-98668-0_12","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T20:45:46Z","timestamp":1753130746000},"page":"237-257","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Deeply Optimizing the\u00a0SAT Solver for\u00a0the\u00a0IC3 Algorithm"],"prefix":"10.1007","author":[{"given":"Yuheng","family":"Su","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiusong","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yiwei","family":"Ci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yingcheng","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tianjun","family":"Bu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ziyu","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"12_CR1","unstructured":"Abc. https:\/\/github.com\/berkeley-abc\/abc"},{"key":"12_CR2","unstructured":"Aiger. https:\/\/fmv.jku.at\/aiger"},{"key":"12_CR3","unstructured":"Artifact. https:\/\/github.com\/gipsyh\/GipSAT-CAV25"},{"key":"12_CR4","unstructured":"Cadical. https:\/\/github.com\/arminbiere\/cadical"},{"key":"12_CR5","unstructured":"Cryptominisat. https:\/\/github.com\/msoos\/cryptominisat"},{"key":"12_CR6","unstructured":"IC3ref. https:\/\/github.com\/arbrad\/IC3ref"},{"key":"12_CR7","unstructured":"MiniSat. http:\/\/minisat.se"},{"key":"12_CR8","unstructured":"nuXmv. https:\/\/nuxmv.fbk.eu"},{"key":"12_CR9","unstructured":"RIC3. https:\/\/github.com\/gipsyh\/rIC3, branch: satif"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"12_CR11","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., 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":"12_CR12","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":"12_CR13","doi-asserted-by":"publisher","unstructured":"Buss, S., Nordstr\u00f6m, J.: Proof complexity and SAT solving. 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. 233\u2013350. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA200990","DOI":"10.3233\/FAIA200990"},{"issue":"1","key":"12_CR14","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s10703-017-0272-0","volume":"50","author":"G Cabodi","year":"2017","unstructured":"Cabodi, G., Camurati, P.E., Mishchenko, A., Palena, M., Pasini, P.: SAT solver management strategies in IC3: an experimental approach. Formal Methods Syst. Des. 50(1), 39\u201374 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0272-0","journal-title":"Formal Methods Syst. Des."},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"12_CR16","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model Checking, 2nd edn. MIT Press (2018). https:\/\/mitpress.mit.edu\/books\/model-checking-second-edition"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking, 1st edn. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Dureja, R., Gurfinkel, A., Ivrii, A., Vizel, Y.: IC3 with internal signals. In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, 19\u201322 October 2021, pp. 63\u201371. IEEE (2021). https:\/\/doi.org\/10.34727\/2021\/ISBN.978-3-85448-046-4_14","DOI":"10.34727\/2021\/ISBN.978-3-85448-046-4_14"},{"key":"12_CR19","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Bjesse, P., Slobodov\u00e1, A. (eds.) International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011, Austin, TX, USA, 30 October\u201302 November 2011, pp. 125\u2013134. FMCAD Inc. (2011). http:\/\/dl.acm.org\/citation.cfm?id=2157675"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. In: Strichman, O., Biere, A. (eds.) First International Workshop on Bounded Model Checking, BMC@CAV 2003, Boulder, Colorado, USA, 13 July 2003. Electronic Notes in Theoretical Computer Science, vol.\u00a089, pp. 543\u2013560. Elsevier (2003). https:\/\/doi.org\/10.1016\/S1571-0661(05)82542-3","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Forsythe, G.E.: Algorithms. Commun. ACM 7(6), 347\u2013349 (1964). https:\/\/doi.org\/10.1145\/512274.512284","DOI":"10.1145\/512274.512284"},{"key":"12_CR22","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":"12_CR23","doi-asserted-by":"publisher","unstructured":"Goel, A., Sakallah, K.A.: Empirical evaluation of IC3-based model checking techniques on Verilog RTL designs. In: Teich, J., Fummi, F. (eds.) Design, Automation & Test in Europe Conference & Exhibition, DATE 2019, Florence, Italy, 25\u201329 March 2019, pp. 618\u2013621. IEEE (2019). https:\/\/doi.org\/10.23919\/DATE.2019.8715289","DOI":"10.23919\/DATE.2019.8715289"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-030-45190-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Goel","year":"2020","unstructured":"Goel, A., Sakallah, K.: AVR: abstractly verifying reachability. In: TACAS 2020. LNCS, vol. 12078, pp. 413\u2013422. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_23"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Ivrii, A.: Pushing to the top. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, 27\u201330 September 2015, pp. 65\u201372. IEEE (2015). https:\/\/doi.org\/10.1109\/FMCAD.2015.7542254","DOI":"10.1109\/FMCAD.2015.7542254"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Ivrii, A.: K-induction without unrolling. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2\u20136 October 2017, pp. 148\u2013155. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102253","DOI":"10.23919\/FMCAD.2017.8102253"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Hassan, Z., Bradley, A.R., Somenzi, F.: Better generalization in IC3. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013, pp. 157\u2013164. IEEE (2013). https:\/\/ieeexplore.ieee.org\/document\/6679405\/","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"12_CR28","doi-asserted-by":"publisher","unstructured":"Kuehlmann, A., Krohm, F.: Equivalence checking using cuts and heaps. In: Yoffa, E.J., Micheli, G.D., Rabaey, J.M. (eds.) Proceedings of the 34st Conference on Design Automation, Anaheim, California, USA, Anaheim Convention Center, 9\u201313 June 1997, pp. 263\u2013268. ACM Press (1997). https:\/\/doi.org\/10.1145\/266021.266090","DOI":"10.1145\/266021.266090"},{"issue":"3","key":"12_CR29","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1093\/COMJNL\/36.3.209","volume":"36","author":"J van Leeuwen","year":"1993","unstructured":"van Leeuwen, J., Wood, D.: Interval heaps. Comput. J. 36(3), 209\u2013216 (1993). https:\/\/doi.org\/10.1093\/COMJNL\/36.3.209","journal-title":"Comput. J."},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-030-81688-9_22","volume-title":"Computer Aided Verification","author":"M Mann","year":"2021","unstructured":"Mann, M., et al.: Pono: a flexible and extensible SMT-based model checker. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12760, pp. 461\u2013474. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22"},{"key":"12_CR31","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":"12_CR32","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":"12_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-030-94583-1_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Seufert","year":"2022","unstructured":"Seufert, T., Scholl, C., Chandrasekharan, A., Reimer, S., Welp, T.: Making PROGRESS in property directed reachability. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 355\u2013377. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_18"},{"key":"12_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127\u2013144. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8"},{"key":"12_CR35","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":"12_CR36","doi-asserted-by":"publisher","unstructured":"Su, Y., Yang, Q., Ci, Y.: Predicting lemmas in generalization of IC3. In: De, V. (ed.) Proceedings of the 61st ACM\/IEEE Design Automation Conference, DAC 2024, San Francisco, CA, USA, 23\u201327 June 2024, pp. 208:1\u2013208:6. ACM (2024). https:\/\/doi.org\/10.1145\/3649329.3655970","DOI":"10.1145\/3649329.3655970"},{"key":"12_CR37","doi-asserted-by":"publisher","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970, pp. 466\u2013483. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_28","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"12_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-319-08867-9_17","volume-title":"Computer Aided Verification","author":"Y Vizel","year":"2014","unstructured":"Vizel, Y., Gurfinkel, A.: Interpolating property directed reachability. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 260\u2013276. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_17"},{"key":"12_CR39","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Weissenbacher, G., Malik, S.: Boolean satisfiability solvers and their applications in model checking. Proc. IEEE 103(11), 2021\u20132035 (2015). https:\/\/doi.org\/10.1109\/JPROC.2015.2455034","DOI":"10.1109\/JPROC.2015.2455034"},{"key":"12_CR40","doi-asserted-by":"publisher","unstructured":"Xia, Y., Becchi, A., Cimatti, A., Griggio, A., Li, J., Pu, G.: Searching for I-good lemmas to accelerate safety model checking. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17\u201322 July 2023, Proceedings, Part II. LNCS, vol. 13965, pp. 288\u2013308. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_14","DOI":"10.1007\/978-3-031-37703-7_14"}],"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-98668-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T15:09:18Z","timestamp":1777302558000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98668-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986673","9783031986680"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98668-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}