{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T18:13:16Z","timestamp":1757614396612,"version":"3.44.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031982071"},{"type":"electronic","value":"9783031982088"}],"license":[{"start":{"date-parts":[[2025,7,9]],"date-time":"2025-07-09T00:00:00Z","timestamp":1752019200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,7,9]],"date-time":"2025-07-09T00:00:00Z","timestamp":1752019200000},"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":[[2026]]},"DOI":"10.1007\/978-3-031-98208-8_9","type":"book-chapter","created":{"date-parts":[[2025,7,13]],"date-time":"2025-07-13T17:56:53Z","timestamp":1752429413000},"page":"143-160","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Adaptive Clause Management in\u00a0SMT Solvers: A Dynamic Weighting Framework for\u00a0Formal Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-7181-4902","authenticated-orcid":false,"given":"Wenda","family":"Leng","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0001-4910-253X","authenticated-orcid":false,"given":"Meihua","family":"Liu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4218-8297","authenticated-orcid":false,"given":"Yufeng","family":"Jin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,9]]},"reference":[{"key":"9_CR1","unstructured":"Audemard, G., Simon, L.: Glucose: a solver that predicts learnt clauses quality. SAT Compet. 7\u20138 (2009)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Audemard, G., Simon, L.: Refining restarts strategies for SAT and UNSAT. In: Principles and Practice of Constraint Programming: 18th International Conference, CP 2012, Qu\u00e9bec City, QC, Canada, 8\u201312 October 2012, pp. 118\u2013126. Springer (2012)","DOI":"10.1007\/978-3-642-33558-7_11"},{"key":"9_CR3","unstructured":"Audemard, G., Simon, L.: Glucose in the SAT 2014 competition. In: Proceedings of SAT Competition, vol. 2014, p. 31 (2014)"},{"issue":"01","key":"9_CR4","doi-asserted-by":"publisher","first-page":"1840001","DOI":"10.1142\/S0218213018400018","volume":"27","author":"G Audemard","year":"2018","unstructured":"Audemard, G., Simon, L.: On the glucose sat solver. Int. J. Artif. Intell. Tools 27(01), 1840001 (2018)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"9_CR5","unstructured":"Barrett, C.: From sat to SMT: successes and challenges. In: ACL2 Workshop, Northeastern University, 11\u201312 May 2009, pp. 1\u201371 (2009)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 1267\u20131329. IOS Press (2021)","DOI":"10.3233\/FAIA201017"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Chowdhury, M.S., M\u00fcller, M., You, J.H.: Exploiting glue clauses to design effective CDCL branching heuristics. In: Principles and Practice of Constraint Programming: 25th International Conference, CP 2019, Stamford, CT, USA, 30 September\u20134 October 2019, Proceedings 25, pp. 126\u2013143. Springer (2019)","DOI":"10.1007\/978-3-030-30048-7_8"},{"issue":"7","key":"9_CR8","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.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: International Conference on Computer Aided Verification, pp. 737\u2013744. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 502\u2013518. Springer (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"issue":"12","key":"9_CR12","doi-asserted-by":"publisher","first-page":"1549","DOI":"10.1016\/j.dam.2006.10.007","volume":"155","author":"E Goldberg","year":"2007","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a fast and robust sat-solver. Discret. Appl. Math. 155(12), 1549\u20131561 (2007)","journal-title":"Discret. Appl. Math."},{"key":"9_CR13","unstructured":"Gomes, C.P., Selman, B., Kautz, H., et al.: Boosting combinatorial search through randomization. In: AAAI\/IAAI, vol. 98, no. 1998, pp. 431\u2013437 (1998)"},{"issue":"08","key":"9_CR14","doi-asserted-by":"publisher","first-page":"1850033","DOI":"10.1142\/S0218213018500331","volume":"27","author":"S Jabbour","year":"2018","unstructured":"Jabbour, S., Lonlac, J., Sais, L., Salhi, Y.: Revisiting the learned clauses database reduction strategies. Int. J. Artif. Intell. Tools 27(08), 1850033 (2018)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"9_CR15","unstructured":"Kautz, H., Horvitz, E., Ruan, Y., Gomes, C., Selman, B.: Dynamic restart policies. In: AAAI\/IAAI, vol. 97, pp. 674\u2013681 (2002)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Liang, J.H., Ganesh, V., Zulkoski, E., Zaman, A., Czarnecki, K.: Understanding VSIDS branching heuristics in conflict-driven clause-learning SAT solvers. In: Hardware and Software: verification and Testing: 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, 17\u201319 November 2015, Proceedings 11, pp. 225\u2013241. Springer (2015)","DOI":"10.1007\/978-3-319-26287-1_14"},{"issue":"01","key":"9_CR17","doi-asserted-by":"publisher","first-page":"2350003","DOI":"10.1142\/S0218213023500033","volume":"32","author":"J Lonlac","year":"2023","unstructured":"Lonlac, J., Nguifo, E.M.: Top-k learned clauses for modern sat solvers. Int. J. Artif. Intell. Tools 32(01), 2350003 (2023)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Mahajan, Y.S., Fu, Z., Malik, S.: Zchaff2004: an efficient sat solver. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 360\u2013375. Springer (2004)","DOI":"10.1007\/11527695_27"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: Proceedings of the 38th annual Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Oh, C.: Between SAT and UNSAT: the fundamental difference in CDCL SAT. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 307\u2013323. Springer (2015)","DOI":"10.1007\/978-3-319-24318-4_23"},{"key":"9_CR21","first-page":"1","volume":"2017","author":"C Oh","year":"2017","unstructured":"Oh, C.: Cominisatps pulsar and ghackcomsps. SAT Compet. 2017, 1 (2017)","journal-title":"SAT Compet."},{"issue":"3\u20134","key":"9_CR22","doi-asserted-by":"publisher","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisfiabil. Boolean Model. Comput. 3(3\u20134), 141\u2013224 (2007)","journal-title":"J. Satisfiabil. Boolean Model. Comput."},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Shim, C., Bae, J., Kim, B.: 30.3 VIP-Sat: a Boolean satisfiability solver featuring 5$$\\times $$ 12 variable in-memory processing elements with 98% solvability for 50-variables 218-clauses 3-sat problems. In: 2024 IEEE International Solid-State Circuits Conference (ISSCC), vol.\u00a067, pp. 486\u2013488. IEEE (2024)","DOI":"10.1109\/ISSCC49657.2024.10454397"},{"key":"9_CR24","unstructured":"Silva, J.M., Sakallah, K.A.: GRASP-a new search algorithm for satisfiability. In: Proceedings of International Conference on Computer Aided Design, pp. 220\u2013227. IEEE (1996)"},{"key":"9_CR25","unstructured":"Wolf, C.: Yosys manual. Retrieved January 16, 2021 (2021)"},{"key":"9_CR26","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: IEEE\/ACM International Conference on Computer Aided Design, ICCAD 2001. IEEE\/ACM Digest of Technical Papers (Cat. No. 01CH37281), pp. 279\u2013285. IEEE (2001)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98208-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,5]],"date-time":"2025-09-05T07:38:21Z","timestamp":1757057901000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98208-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,9]]},"ISBN":["9783031982071","9783031982088"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98208-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,7,9]]},"assertion":[{"value":"9 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Theoretical Aspects of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","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":"14 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tase2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cyprusconferences.org\/tase2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}