{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T15:12:15Z","timestamp":1778080335287,"version":"3.51.4"},"publisher-location":"Singapore","reference-count":43,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819586165","type":"print"},{"value":"9789819586172","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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-981-95-8617-2_1","type":"book-chapter","created":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T14:25:30Z","timestamp":1778077530000},"page":"3-32","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["More Paradigms of\u00a0SAT Solvers: Circuit-SAT, FPGA-Based SAT, LLM-Based SAT"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1730-6922","authenticated-orcid":false,"given":"Shaowei","family":"Cai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,1]]},"reference":[{"key":"1_CR1","unstructured":"Achiam, J., et\u00a0al.: GPT-4 technical report. arXiv preprint arXiv:2303.08774 (2023)"},{"key":"1_CR2","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: The 21st International Joint Conference on Artificial Intelligence, vol.\u00a09, pp. 399\u2013404 (2009)"},{"key":"1_CR3","unstructured":"Audemard, G., Simon, L.: Glucose 2.1: aggressive, but reactive, clause database management, dynamic restarts (system description). In: Pragmatics of SAT 2012 (2012)"},{"issue":"01","key":"1_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). https:\/\/doi.org\/10.1142\/S0218213018400018","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1016\/j.artint.2015.01.002","volume":"223","author":"A Balint","year":"2015","unstructured":"Balint, A., Belov, A., J\u00e4rvisalo, M., Sinz, C.: Overview and analysis of the sat challenge 2012 solver competition. Artif. Intell. 223, 120\u2013155 (2015)","journal-title":"Artif. Intell."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Balint, A., Fr\u00f6hlich, A.: Improving stochastic local search for SAT with a new probability distribution. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 10\u201315. Springer, Cham (2010)","DOI":"10.1007\/978-3-642-14186-7_3"},{"key":"1_CR7","unstructured":"Balyo, T., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.): Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science, University of Helsinki (2023)"},{"key":"1_CR8","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT competition 2024. SAT Competition 2024 (2024)"},{"key":"1_CR9","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep.\u00a011\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Biere, A., J\u00e4rvisalo, M., Kiesl, B.: Preprocessing in SAT solving. In: Biere, A., Heule, M., Van\u00a0Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a06, 2nd edn. IOS Press (2021)","DOI":"10.3233\/FAIA336"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"B\u00f6ttcher, S., Doerr, B., Neumann, F.: Optimal fixed and adaptive mutation rates for the leadingones problem. In: International Conference on Parallel Problem Solving from Nature, pp. 1\u201310. Springer, Cham (2010)","DOI":"10.1007\/978-3-642-15844-5_1"},{"key":"1_CR12","unstructured":"Brown, T., et\u00a0al.: Language models are few-shot learners. In: NIPS 2020: Proceedings of the 34th International Conference on Neural Information Processing System, pp. 1877\u20131901 (2020)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Cai, S., Luo, C., Su, K.: CCAnr: a configuration checking based local search solver for non-random satisfiability. In: Theory and Applications of Satisfiability Testing, pp.\u00a01\u20138. Springer, Cham (2015)","DOI":"10.1007\/978-3-319-24318-4_1"},{"issue":"1","key":"1_CR14","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Cogent: accurate theorem proving for program verification. In: Etessami, K., Rajamani, S.K. (eds.) Proceedings of 17th International Conference of Computer Aided Verification, CAV 2005. LNCS, vol.\u00a03576, pp. 296\u2013300. Springer, Cham (2005)","DOI":"10.1007\/11513988_30"},{"issue":"7","key":"1_CR16","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(7), 394\u2013397 (1962). https:\/\/doi.org\/10.1145\/368273.368557","journal-title":"Commun. ACM"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Doerr, C., Ye, F., van Rijn, S., Wang, H., B\u00e4ck, T.: Towards a theory-guided benchmarking suite for discrete black-box optimization heuristics: profiling (1+$$\\lambda $$) EA variants on onemax and leadingones. In: Proceedings of the Genetic and Evolutionary Computation Conference, pp. 951\u2013958 (2018)","DOI":"10.1145\/3205455.3205621"},{"key":"1_CR18","unstructured":"Een, N.: MINISAT: a SAT solver with conflict-clause minimization. In: Proceedings of SAT 2005 (2005)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Een, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Proceedings of SAT 2003, pp. 502\u2013518 (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"1_CR20","unstructured":"Fleury, A., Heisinger, M.: Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020. In: Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, vol.\u00a02020, pp. 51\u201353. Department of Computer Science, University of Helsinki (2020)"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Proceedings of SAT 2016, pp. 228\u2013245 (2016)","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"1_CR22","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: Proceedings of ECAI 1992, pp. 359\u2013363 (1992)"},{"issue":"54","key":"1_CR23","first-page":"1","volume":"23","author":"M Lindauer","year":"2022","unstructured":"Lindauer, M., et al.: SMAC3: a versatile Bayesian optimization package for hyperparameter optimization. J. Mach. Learn. Res. 23(54), 1\u20139 (2022)","journal-title":"J. Mach. Learn. Res."},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Lo, M., Chang, M.C.F., Cong, J.: SAT-Accel: a modern SAT solver on a FPGA. In: FPGA 2025: Proceedings of the 2025 ACM\/SIGDA International Symposium on Field Programmable Gate Arrays, pp. 234\u2013246. Association for Computing Machinery, New York, NY, USA (2025). https:\/\/doi.org\/10.1145\/3706628.3708869","DOI":"10.1145\/3706628.3708869"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Mencer, O., Plazner, M.: Dynamic circuit generation for Boolean satisfiability in an object-oriented design environment. In: Proceedings of the 32nd Annual Hawaii International Conference on Systems Sciences, HICSS-32. Abstracts and CD-ROM of Full Papers. IEEE Computer Society, Maui, HI, USA (1999). https:\/\/doi.org\/10.1109\/HICSS.1999.772883","DOI":"10.1109\/HICSS.1999.772883"},{"key":"1_CR26","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 Design Automation Conference, DAC 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"1_CR27","unstructured":"Naveed, H., et al.: A comprehensive overview of large language models. arXiv preprint arXiv:2307.06435 (2023)"},{"issue":"1","key":"1_CR28","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/3107548","volume":"61","author":"N Newman","year":"2018","unstructured":"Newman, N., Fr\u00e9chette, A., Leyton-Brown, K.: Deep optimization for spectrum repacking. Commun. ACM 61(1), 97\u2013104 (2018). https:\/\/doi.org\/10.1145\/3107548","journal-title":"Commun. ACM"},{"key":"1_CR29","unstructured":"OpenAI: OpenAI API documentation (2023). https:\/\/platform.openai.com\/docs"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Qian, Y., Chen, Z., Zhang, X., Cai, S.: X-SAT: an efficient circuit-based SAT solver. In: 62nd ACM\/IEEE Design Automation Conference, DAC 2025, San Francisco, CA, USA, 22\u201325 June 2025, pp.\u00a01\u20137. IEEE (2025)","DOI":"10.1109\/DAC63849.2025.11132604"},{"key":"1_CR31","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP \u2013 a new search algorithm for satisfiability. In: Proceedings of ICCAD 1996, pp. 220\u2013227 (1996)"},{"issue":"11","key":"1_CR32","doi-asserted-by":"publisher","first-page":"1449","DOI":"10.1109\/TC.2004.102","volume":"53","author":"I Skliarova","year":"2004","unstructured":"Skliarova, I., De Brito Ferrari, A.: Reconfigurable hardware SAT solvers: a survey of systems. IEEE Trans. Comput. 53(11), 1449\u20131461 (2004). https:\/\/doi.org\/10.1109\/TC.2004.102","journal-title":"IEEE Trans. Comput."},{"key":"1_CR33","unstructured":"S\u00f6rensson, N.: MINISAT 2.2 and MINISAT++ 1.1. Citeseer (2010)"},{"key":"1_CR34","unstructured":"Sun, Y., Ye, F., Chen, Z., Wei, K., Cai, S.: Automatically discovering heuristics in a complex SAT solver with large language models. CoRR abs\/2507.22876 (2025)"},{"key":"1_CR35","unstructured":"Sun, Y., et al.: AutoSAT: automatically optimize SAT solvers via large language models. CoRR abs\/2402.10705 (2024)"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Suyama, T., Yokoo, M., Sawada, H., Nagoya, A.: Solving satisfiability problems using reconfigurable computing. IEEE Trans. Very Large Scale Integration (VLSI) Syst. 9(1), 109\u2013116 (2001). https:\/\/doi.org\/10.1109\/92.920826","DOI":"10.1109\/92.920826"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Tao, Y., Cai, S.: VeriSAT: the hardware design of modern SAT solver. In: Proceedings of ICCAD 2025 (2025)","DOI":"10.1109\/ICCAD66269.2025.11240752"},{"key":"1_CR38","doi-asserted-by":"publisher","unstructured":"Ustaoglu, B., Huhn, S., Sill\u00a0Torres, F., Gro\u00dfe, D., Drechsler, R.: SAT-hard: a learning-based hardware SAT-solver. In: 22nd Euromicro Conference on Digital System Design (DSD), pp. 74\u201381 (2019). https:\/\/doi.org\/10.1109\/DSD.2019.00021","DOI":"10.1109\/DSD.2019.00021"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Ye, F., Wang, H., Doerr, C., B\u00e4ck, T.: Benchmarking a genetic algorithm with configurable crossover probability. In: Proceedings of the International Conference on Parallel Problem Solving from Nature, pp. 699\u2013713. Springer, Cham (2020)","DOI":"10.1007\/978-3-030-58115-2_49"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Zhang, H.T., Jiang, J.H.R., Mishchenko, A.: A circuit-based SAT solver for logic synthesis. In: Proceedings of the IEEE\/ACM International Conference on Computer Aided Design (ICCAD), pp.\u00a01\u20136. IEEE (2021)","DOI":"10.1109\/ICCAD51958.2021.9643505"},{"key":"1_CR41","unstructured":"Zhihan\u00a0Chen, X.Z.: EasySAT: a simple CDCL SAT solver (2022). https:\/\/github.com\/shaowei-cai-group\/EasySAT"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Zhong, P., Martonosi, M., Ashar, P., Malik, S.: Accelerating Boolean satisfiability with configurable hardware. In: Proceedings of the IEEE Symposium on FPGAs for Custom Computing Machines, pp. 186\u2013195 (1998). https:\/\/doi.org\/10.1109\/FPGA.1998.707896","DOI":"10.1109\/FPGA.1998.707896"},{"key":"1_CR43","doi-asserted-by":"publisher","unstructured":"Zhou, N.F., Kjellerstrand, H., Fruhman, J.: Constraint Solving and Planning with Picat, Springer Briefs in Intelligent Systems, vol.\u00a011. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25883-6","DOI":"10.1007\/978-3-319-25883-6"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-8617-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T14:25:55Z","timestamp":1778077555000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-8617-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9789819586165","9789819586172"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-8617-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"1 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Summer School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Beijing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"17 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tis.ios.ac.cn\/SETSS2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}