{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T02:49:47Z","timestamp":1781837387254,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":83,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T00:00:00Z","timestamp":1740614400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100006374","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,2,27]]},"DOI":"10.1145\/3706628.3708869","type":"proceedings-article","created":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T12:22:11Z","timestamp":1740572531000},"page":"234-246","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["SAT-Accel: A Modern SAT Solver on a FPGA"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8004-2942","authenticated-orcid":false,"given":"Michael","family":"Lo","sequence":"first","affiliation":[{"name":"University of California, Los Angeles, Los Angeles, California, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2934-9359","authenticated-orcid":false,"given":"Mau-Chung Frank","family":"Chang","sequence":"additional","affiliation":[{"name":"University of California, Los Angeles, Los Angeles, California, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2887-6963","authenticated-orcid":false,"given":"Jason","family":"Cong","sequence":"additional","affiliation":[{"name":"University of California, Los Angeles, Los Angeles, California, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,2,27]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n. d.] (). http:\/\/www.satcompetition.org\/."},{"key":"e_1_3_2_1_2_1","unstructured":"[n. d.] (). https:\/\/satcompetition.github.io\/2022\/results.html."},{"key":"e_1_3_2_1_3_1","unstructured":"[n. d.] (). https:\/\/www.cs.ubc.ca\/~hoos\/SATLIB\/benchm.html."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.310028"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2567709.2627674"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04244-7_13"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA52012.2021.00054"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45620-1_17"},{"key":"e_1_3_2_1_9_1","unstructured":"Gilles Audemard and Laurent Simon. 2009. Glucose: a solver that predicts learnt clauses quality. SAT Competition 7--8."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2008.4681565"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3570928"},{"key":"e_1_3_2_1_12_1","volume-title":"Plingeling and Treengeling entering the SAT Competition","author":"Biere Armin","year":"2020","unstructured":"Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. 2020. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Proc. of SAT Competition 2020 -- Solver and Benchmark Descriptions (Department of Computer Science Report Series B). Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda, (Eds.) Vol. B-2020--1. University of Helsinki, 51--53."},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of Pragmatics of SAT 2015 and 2018 (EPiC Series in Computing). Daniel Le Berre and Matti Jarvisalo, (Eds.)","volume":"59","author":"Biere Armin","year":"2019","unstructured":"Armin Biere and Andreas Frohlich. 2019. Evaluating CDCL restart schemes. In Proceedings of Pragmatics of SAT 2015 and 2018 (EPiC Series in Computing). Daniel Le Berre and Matti Jarvisalo, (Eds.) Vol. 59. EasyChair, 1--17. doi: 10.29 007\/89dw."},{"key":"e_1_3_2_1_14_1","first-page":"111","article-title":"The effect of scrambling CNFs","volume":"59","author":"Biere Armin","year":"2019","unstructured":"Armin Biere and Marijn Heule. 2019. The effect of scrambling CNFs. Proceedings of Pragmatics of SAT, 59, 111--126.","journal-title":"Proceedings of Pragmatics of SAT"},{"key":"e_1_3_2_1_15_1","volume-title":"2016 IEEE 24th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM), 32--39","author":"Frank Chang Mau-Chung","year":"2016","unstructured":"Mau-Chung Frank Chang, Yu-Ting Chen, Jason Cong, Po-Tsang Huang, Chun- Liang Kuo, and Cody Hao Yu. 2016. The SMEM seeding acceleration for DNA sequence alignment. In 2016 IEEE 24th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM), 32--39. doi: 10.1109 \/FCCM.2016.21."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3524108"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3294054"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3530775"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/33616"},{"key":"e_1_3_2_1_21_1","volume-title":"Loveland","author":"Davis Martin","year":"1962","unstructured":"Martin Davis, George Logemann, and Donald W. Loveland. 1962. A machine program for theorem-proving. In Communications of the ACM 5."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Martin Davis and Hilary Putnam. 1960. A computing procedure for quantification theory. In Journal of the ACM 7.","DOI":"10.1145\/321033.321034"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSSC.1974.1050511"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/FPL.2014.6927471"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3466752.3480117"},{"key":"e_1_3_2_1_26_1","volume-title":"Theory and Applications of Satisfiability Testing","author":"E\u00e9n Niklas","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson. 2004. An extensible SAT-solver. In Theory and Applications of Satisfiability Testing. Enrico Giunchiglia and Armando Tacchella, (Eds.) Springer Berlin Heidelberg, Berlin, Heidelberg, 502--518. isbn: 978--3--540--24605--3."},{"key":"e_1_3_2_1_27_1","volume-title":"Principles and Practice of Constraint Programming","author":"Fichte Johannes K.","unstructured":"Johannes K. Fichte, Markus Hecher, and Stefan Szeider. 2020. A time leap challenge for SAT-solving. In Principles and Practice of Constraint Programming. Helmut Simonis, (Ed.) Springer International Publishing, Cham, 267--285. isbn: 978--3-030--58475--7."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2018.00012"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2847263.2847342"},{"key":"e_1_3_2_1_30_1","volume-title":"2019 29th International Conference on Field Programmable Logic and Applications (FPL), 314--320","author":"Nicholas","year":"2019","unstructured":"Nicholas V. Giamblanco and Jason H. Anderson. 2019. A dynamic memory allocation library for high-level synthesis. In 2019 29th International Conference on Field Programmable Logic and Applications (FPL), 314--320. doi: 10.1109 \/FPL.2019.00057."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2020.2981080"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2017.7858394"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3431920.3439289"},{"key":"e_1_3_2_1_34_1","unstructured":"Leopold Haller and Satnam Singh. 2010. Relieving capacity limits on FPGAbased SAT-solvers. In Formal Methods in Computer Aided Design 217--220."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2016.30"},{"key":"e_1_3_2_1_36_1","volume-title":"Proceedings of the 2017 ACM\/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA '17)","author":"Song","year":"2007","unstructured":"Song Han et al. 2017. ESE: efficient speech recognition engine with sparse LSTM on FPGA. In Proceedings of the 2017 ACM\/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA '17). Association for Computing Machinery, Monterey, California, USA, 75--84. isbn: 9781450343541. doi: 10.11 45\/3020078.3021745."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA51647.2021.00017"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.09.006"},{"key":"e_1_3_2_1_39_1","volume-title":"Marques-Silva","author":"Katebi Hadi","year":"2011","unstructured":"Hadi Katebi, Karem A. Sakallah, and Joao P. Marques-Silva. 2011. Empirical study of the anatomy of modern SAT solvers. In Theory and Applications of Satisfiability Testing - SAT 2011. Karem A. Sakallah and Laurent Simon, (Eds.) Springer Berlin Heidelberg, Berlin, Heidelberg, 343--356. isbn: 978--3--642--21581- 0."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3556938"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.108614"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380340"},{"key":"e_1_3_2_1_43_1","volume-title":"Atulan Zaman, and Krzysztof Czarnecki.","author":"Liang Jia Hui","year":"2015","unstructured":"Jia Hui Liang, Vijay Ganesh, Ed Zulkoski, Atulan Zaman, and Krzysztof Czarnecki. 2015. Understanding VSIDS branching heuristics in conflict-driven clause-learning SAT solvers. (2015). arXiv: 1506.08905 [cs.LO]."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC56929.2023.10247760"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/JETCAS.2022.3202870"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM48280.2020.00029"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA200987"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/337292.337611"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006326723002"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/369691.369777"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2002.1004311"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/296399.296450"},{"key":"e_1_3_2_1_55_1","volume-title":"2021 26th Asia and South Pacific Design Automation Conference (ASP-DAC), 29--34","author":"Park Soowang","unstructured":"Soowang Park, Jae-Won Nam, and Sandeep K. Gupta. 2021. Hw-bcp: a custom hardware accelerator for sat suitable for single chip implementation for large benchmarks. In 2021 26th Asia and South Pacific Design Automation Conference (ASP-DAC), 29--34."},{"key":"e_1_3_2_1_56_1","volume-title":"Proceedings 10","author":"Pipatsrisawat Knot","year":"2007","unstructured":"Knot Pipatsrisawat and Adnan Darwiche. 2007. A lightweight component caching scheme for satisfiability solvers. In Theory and Applications of Satisfiability Testing--SAT 2007: 10th International Conference, Lisbon, Portugal, May 28--31, 2007. Proceedings 10. Springer, 294--299."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3599691.3603404"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM.2018.00015"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","unstructured":"Mona Safar M.Watheq El-Kharashi Mohamed Shalan and Ashraf Salem. 2011. A reconfigurable pipelined conflict directed jumping search SAT solver. In 2011 Design Automation & Test in Europe 1--6. doi: 10.1109\/DATE.2011.5763199.","DOI":"10.1109\/DATE.2011.5763199"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA45697.2020.00033"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/1641503.1641511"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358302"},{"key":"e_1_3_2_1_63_1","first-page":"8","article-title":"FPGA based opencl acceleration of genome sequencing software","volume":"128","author":"Sirasao Ashish","year":"2015","unstructured":"Ashish Sirasao, Elliott Delaye, Ravi Sunkavalli, and Stephen Neuendorffer. 2015. FPGA based opencl acceleration of genome sequencing software. System, 128, 8.7, 11.","journal-title":"System"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.852031"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_23"},{"key":"e_1_3_2_1_66_1","unstructured":"Saurabh Srivastava. 2010. Satisfiability-based program reasoning and program synthesis. Ph.D. Dissertation."},{"key":"e_1_3_2_1_67_1","volume-title":"2017 50th Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO), 15-- 26","author":"Sukhwani Bharat","year":"2017","unstructured":"Bharat Sukhwani, Thomas Roewer, Charles L. Haymes, Kyu-Hyoun Kim, Adam J. McPadden, Daniel M. Dreps, Dean Sanner, Jan Van Lunteren, and Sameh Asaad. 2017. Contutto -- a novel FPGA-based prototyping platform enabling innovation in the memory subsystem of a server class processor. In 2017 50th Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO), 15-- 26."},{"key":"e_1_3_2_1_68_1","volume-title":"Design Automation of Quantum Computers","author":"Tan Bochen","unstructured":"Bochen Tan and Jason Cong. 2022. Layout synthesis for near-term quantum computing: gap analysis and optimal solution. In Design Automation of Quantum Computers. Springer, 25--40."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3400302.3415620"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2020.3009140"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2013.6691124"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3194554.3194643"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2019.00021"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240856"},{"key":"e_1_3_2_1_75_1","volume-title":"Proceedings of the 1997 ACM fifth international symposium on Field-programmable gate arrays, 119--125","author":"GlennWood R","year":"1997","unstructured":"R GlennWood and Rob A Rutenbar. 1997. FPGA routing and routability estimation via boolean satisfiability. In Proceedings of the 1997 ACM fifth international symposium on Field-programmable gate arrays, 119--125."},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2019.00044"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPSW.2012.57"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934583.2934644"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2019.8702071"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2001.968634"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277098"},{"key":"e_1_3_2_1_82_1","volume-title":"Dally","author":"Zhu Chenzhuo","year":"2023","unstructured":"Chenzhuo Zhu, Alexander C. Rucker, Yawen Wang, and William J. Dally. 2023. Satin: hardware for boolean satisfiability inference. (2023). https:\/\/arxiv.org\/ab s\/2303.02588 arXiv: 2303.02588 [cs.AR]."},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA56546.2023.10071133"}],"event":{"name":"FPGA '25: The 2025 ACM\/SIGDA International Symposium on Field Programmable Gate Arrays","location":"Monterey CA USA","acronym":"FPGA '25","sponsor":["SIGDA ACM Special Interest Group on Design Automation"]},"container-title":["Proceedings of the 2025 ACM\/SIGDA International Symposium on Field Programmable Gate Arrays"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3706628.3708869","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3706628.3708869","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T21:54:18Z","timestamp":1755899658000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3706628.3708869"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,27]]},"references-count":83,"alternative-id":["10.1145\/3706628.3708869","10.1145\/3706628"],"URL":"https:\/\/doi.org\/10.1145\/3706628.3708869","relation":{},"subject":[],"published":{"date-parts":[[2025,2,27]]},"assertion":[{"value":"2025-02-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}