{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T07:21:45Z","timestamp":1777965705415,"version":"3.51.4"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2021,9,20]],"date-time":"2021-09-20T00:00:00Z","timestamp":1632096000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Parallel Comput."],"published-print":{"date-parts":[[2021,9,30]]},"abstract":"<jats:p>Boolean satisfiability (SAT) is an important performance-hungry problem with applications in many problem domains. However, most work on parallelizing SAT solvers has focused on coarse-grained, mostly embarrassing, parallelism. Here, we study fine-grained parallelism that can speed up existing sequential SAT solvers, which all happen to be of the so-called Conflict-Directed Clause Learning variety. We show the potential for speedups of up to 382\u00d7 across a variety of problem instances. We hope that these results will stimulate future research, particularly with respect to a computer architecture open problem we present.<\/jats:p>","DOI":"10.1145\/3470639","type":"journal-article","created":{"date-parts":[[2021,9,20]],"date-time":"2021-09-20T18:27:58Z","timestamp":1632162478000},"page":"1-18","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Study of Fine-grained Nested Parallelism in CDCL SAT Solvers"],"prefix":"10.1145","volume":"8","author":[{"given":"James","family":"Edwards","sequence":"first","affiliation":[{"name":"University of Maryland, Maryland, USA"}]},{"given":"Uzi","family":"Vishkin","sequence":"additional","affiliation":[{"name":"University of Maryland, Maryland, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,9,20]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1661445.1661509"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_15"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1892875.1892920"},{"key":"e_1_2_1_4_1","volume-title":"PicoSAT and PrecoSAT at SAT Race","author":"Biere Armin","year":"2010","unstructured":"Armin Biere . 2010. Lingeling, Plingeling , PicoSAT and PrecoSAT at SAT Race 2010 . Technical Report. Johannes Kepler University , Linz, Austria. Armin Biere. 2010. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report. Johannes Kepler University, Linz, Austria."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions. 33\u201334","author":"Biere Armin","year":"2012","unstructured":"Armin Biere . 2012 . Lingeling and friends entering the SAT challenge 2012 . In Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions. 33\u201334 . Armin Biere. 2012. Lingeling and friends entering the SAT challenge 2012. In Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions. 33\u201334."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, Tom\u00e1\u0161 Balyo, Marijn Heule, and Matti J\u00e4rvisalo (Eds.)","author":"Biere Armin","year":"2017","unstructured":"Armin Biere . 2017 . CaDiCaL, lingeling, plingeling, treengeling and yalsat entering the SAT competition 2017 . In Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, Tom\u00e1\u0161 Balyo, Marijn Heule, and Matti J\u00e4rvisalo (Eds.) . University of Helsinki, 14\u201315. http:\/\/hdl.handle.net\/10138\/224324. Armin Biere. 2017. CaDiCaL, lingeling, plingeling, treengeling and yalsat entering the SAT competition 2017. In Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, Tom\u00e1\u0161 Balyo, Marijn Heule, and Matti J\u00e4rvisalo (Eds.). University of Helsinki, 14\u201315. http:\/\/hdl.handle.net\/10138\/224324."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, Tom\u00e1\u0161 Balyo, Nils Froleyks, Marijn J.H. Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.)","author":"Biere Armin","year":"2020","unstructured":"Armin Biere , Katalin Fazekas , Mathias Fleury , and Maximilian Heisinger . 2020 . CaDiCaL, kissat, paracooba, plingeling and treengeling entering the SAT competition 2020 . In Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, Tom\u00e1\u0161 Balyo, Nils Froleyks, Marijn J.H. Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.) . University of Helsinki, 50\u201353. http:\/\/hdl.handle.net\/10138\/3 18450. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximilian Heisinger. 2020. CaDiCaL, kissat, paracooba, plingeling and treengeling entering the SAT competition 2020. In Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, Tom\u00e1\u0161 Balyo, Nils Froleyks, Marijn J.H. Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.). University of Helsinki, 50\u201353. http:\/\/hdl.handle.net\/10138\/318450."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.42122"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/209937.209958"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 2nd Workshop on Hot Topics in Parallelism (HotPar\u201910)","author":"Caragea George C.","year":"2010","unstructured":"George C. Caragea , Fuat Keceli , Alexandros Tzannes , and Uzi Vishkin . 2010 . General-purpose vs. GPU: Comparison of many-cores on irregular workloads . In Proceedings of the 2nd Workshop on Hot Topics in Parallelism (HotPar\u201910) . USENIX. George C. Caragea, Fuat Keceli, Alexandros Tzannes, and Uzi Vishkin. 2010. General-purpose vs. GPU: Comparison of many-cores on irregular workloads. In Proceedings of the 2nd Workshop on Hot Topics in Parallelism (HotPar\u201910). USENIX."},{"key":"e_1_2_1_12_1","volume-title":"Parallelization of SAT Algorithms on GPU. Master\u2019s thesis. Instituto Superior T\u00e9cnico","author":"Costa Carlos Filipe","unstructured":"Carlos Filipe Costa . 2014. Parallelization of SAT Algorithms on GPU. Master\u2019s thesis. Instituto Superior T\u00e9cnico , University of Lisbon. Carlos Filipe Costa. 2014. Parallelization of SAT Algorithms on GPU. Master\u2019s thesis. Instituto Superior T\u00e9cnico, University of Lisbon."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/173284.155333"},{"key":"e_1_2_1_14_1","first-page":"3","article-title":"CUD@SAT: SAT solving on GPUs","volume":"27","author":"Pal\u00f9 Alessandro Dal","year":"2015","unstructured":"Alessandro Dal Pal\u00f9 , Agostino Dovier , Andrea Formisano , and Enrico Pontelli . 2015 . CUD@SAT: SAT solving on GPUs . J. Exp. Theor. Artif. Intell. 27 , 3 (May 2015), 293\u2013316. https:\/\/doi.org\/10.1080\/0952813X.2014.954274 10.1080\/0952813X.2014.954274 Alessandro Dal Pal\u00f9, Agostino Dovier, Andrea Formisano, and Enrico Pontelli. 2015. CUD@SAT: SAT solving on GPUs. J. Exp. Theor. Artif. Intell. 27, 3 (May 2015), 293\u2013316. https:\/\/doi.org\/10.1080\/0952813X.2014.954274","journal-title":"J. Exp. Theor. Artif. Intell."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(90)90046-3"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/861888"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1789826.1789828"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT\u201903)","author":"E\u00e9n Niklas","year":"2003","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson . 2003 . An extensible SAT-solver . In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT\u201903) , Enrico Giunchiglia and Armando Tacchella (Eds.). Springer, Berlin, 502\u2013518. https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37 10.1007\/978-3-540-24605-3_37 Niklas E\u00e9n and Niklas S\u00f6rensson. 2003. An extensible SAT-solver. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT\u201903), Enrico Giunchiglia and Armando Tacchella (Eds.). Springer, Berlin, 502\u2013518. https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"e_1_2_1_20_1","volume-title":"Oancea","author":"Elsman Martin","year":"2018","unstructured":"Martin Elsman , Troels Henriksen , and Cosmin E . Oancea . 2018 . Parallel programming in Futhark. Retrieved from https:\/\/futhark-book.readthedocs.io\/en\/latest\/. Martin Elsman, Troels Henriksen, and Cosmin E. Oancea. 2018. Parallel programming in Futhark. Retrieved from https:\/\/futhark-book.readthedocs.io\/en\/latest\/."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_25"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA\u201912)","author":"Fujii Hironori","year":"2012","unstructured":"Hironori Fujii and Noriyuki Fujimoto . 2012 . GPU acceleration of BCP procedure for SAT algorithms . In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA\u201912) . Hironori Fujii and Noriyuki Fujimoto. 2012. GPU acceleration of BCP procedure for SAT algorithms. In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA\u201912)."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2017.2754376"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1991.185438"},{"key":"e_1_2_1_25_1","unstructured":"Seth Copen Goldstein. 1997. Lazy Threads: Compiler and Runtime Stuctures for Fine-Grained Programming. Ph.D. Dissertation. University of California\u2013Berkeley Berkeley CA.  Seth Copen Goldstein. 1997. Lazy Threads: Compiler and Runtime Stuctures for Fine-Grained Programming. Ph.D. Dissertation. University of California\u2013Berkeley Berkeley CA."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1996.0104"},{"key":"e_1_2_1_27_1","first-page":"89","article-title":"Satisfiability solvers. In Handbook of Knowledge Representation, F. van Harmelen, V. Lifschitz, and B. Porter (Eds.). Vol. 3","volume":"2","author":"Gomes Carla P.","year":"2008","unstructured":"Carla P. Gomes , Henry Kautz , Ashish Sabharwal , and Bart Selman . 2008 . Satisfiability solvers. In Handbook of Knowledge Representation, F. van Harmelen, V. Lifschitz, and B. Porter (Eds.). Vol. 3 . Chapter 2 , 89 \u2013 134 . https:\/\/doi.org\/10.1016\/S1574-6526(07)03002-7 10.1016\/S1574-6526(07)03002-7 Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. 2008. Satisfiability solvers. In Handbook of Knowledge Representation, F. van Harmelen, V. Lifschitz, and B. Porter (Eds.). Vol. 3. Chapter 2, 89\u2013134. https:\/\/doi.org\/10.1016\/S1574-6526(07)03002-7","journal-title":"Chapter"},{"key":"e_1_2_1_28_1","volume-title":"AIP Conference Proceedings","volume":"1836","author":"Gong Weiwei","year":"2017","unstructured":"Weiwei Gong and Xu Zhou . 2017 . A survey of SAT solver . In AIP Conference Proceedings , Vol. 1836 . https:\/\/doi.org\/10.1063\/1.4981999 10.1063\/1.4981999 Weiwei Gong and Xu Zhou. 2017. A survey of SAT solver. In AIP Conference Proceedings, Vol. 1836. https:\/\/doi.org\/10.1063\/1.4981999"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11757283_5"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of SAT Competition 2018\u2014Solver and Benchmark Descriptions.","volume":"1","author":"Heule Marijn","year":"2018","unstructured":"Marijn Heule , Matti J\u00e4rvisalo , and Martin Suda ( Eds .). 2018 . Proceedings of SAT Competition 2018\u2014Solver and Benchmark Descriptions. Vol. B-2018- 1 . Department of Computer Science, University of Helsinki. Marijn Heule, Matti J\u00e4rvisalo, and Martin Suda (Eds.). 2018. Proceedings of SAT Competition 2018\u2014Solver and Benchmark Descriptions. Vol. B-2018-1. Department of Computer Science, University of Helsinki."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/3171837.3171974"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/133889"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/557756"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1391237"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/146628.139702"},{"key":"e_1_2_1_38_1","volume-title":"MapleSAT: Combining Machine Learning and Deduction in SAT solvers. Retrieved Junary 8","author":"\u00a0al Jia Hui","year":"2021","unstructured":"Jia Hui Liang et \u00a0al . 2018. MapleSAT: Combining Machine Learning and Deduction in SAT solvers. Retrieved Junary 8 , 2021 from https:\/\/sites.google.com\/a\/gsd.uwaterloo.ca\/maplesat\/. Jia Hui Liang et\u00a0al. 2018. MapleSAT: Combining Machine Learning and Deduction in SAT solvers. Retrieved Junary 8, 2021 from https:\/\/sites.google.com\/a\/gsd.uwaterloo.ca\/maplesat\/."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26287-1_14"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9084-z"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1101\/gr.234435.118"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/HiPC.2019.00053"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2008.4605925"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCS.2010.5547116"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_13"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91631"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2013.142"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94144-8_4"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_53"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_38"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2020.2972385"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629643"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866739.1866757"},{"key":"e_1_2_1_56_1","volume-title":"Handbook on Parallel Computing: Models, Algorithms, and Applications","author":"Vishkin Uzi","unstructured":"Uzi Vishkin , George C. Caragea , and Bryant Lee . 2008. Models for advancing PRAM and other algorithms into parallel programs for a PRAM-on-Chip platform . In Handbook on Parallel Computing: Models, Algorithms, and Applications , S. Rajasekaran and J. Reif (Eds.). Chapman and Hall\/CRC Press , Chapter 5. Uzi Vishkin, George C. Caragea, and Bryant Lee. 2008. Models for advancing PRAM and other algorithms into parallel programs for a PRAM-on-Chip platform. In Handbook on Parallel Computing: Models, Algorithms, and Applications, S. Rajasekaran and J. Reif (Eds.). Chapman and Hall\/CRC Press, Chapter 5."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/277651.277680"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.007"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1366230.1366240"},{"key":"e_1_2_1_61_1","volume-title":"Patent 8,209,690 B2","author":"Wen Xingzhi","year":"2012","unstructured":"Xingzhi Wen and Uzi Yehoshua Vishkin . U. S. Patent 8,209,690 B2 , 2012 . System and Method for Thread Handling in Multithreaded Parallel Computing of Nested Threads. (U.S. Patent 8,209,690 B2, 2012). Xingzhi Wen and Uzi Yehoshua Vishkin. U.S. Patent 8,209,690 B2, 2012. System and Method for Thread Handling in Multithreaded Parallel Computing of Nested Threads. (U.S. Patent 8,209,690 B2, 2012)."}],"container-title":["ACM Transactions on Parallel Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3470639","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3470639","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:55Z","timestamp":1750191535000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3470639"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,20]]},"references-count":59,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,9,30]]}},"alternative-id":["10.1145\/3470639"],"URL":"https:\/\/doi.org\/10.1145\/3470639","relation":{},"ISSN":["2329-4949","2329-4957"],"issn-type":[{"value":"2329-4949","type":"print"},{"value":"2329-4957","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,9,20]]},"assertion":[{"value":"2020-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-09-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}