{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T16:23:08Z","timestamp":1792254188479,"version":"4.4.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720155","type":"print"},{"value":"9783030720162","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Since 2013, the leading SAT solvers in the SAT competition all use inprocessing, which unlike preprocessing, interleaves search with simplifications. However, applying inprocessing frequently can still be a bottle neck, i.e., for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As memory is a scarce resource in GPUs, we present new space-efficient data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improves memory access locality. Our new parallel variable elimination algorithm is twice as fast as previous work. In experiments our new solver <jats:sc>ParaFROST<\/jats:sc> solves many benchmarks faster on the GPU than its sequential counterparts.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_8","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"133-151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["SAT Solving with GPU Accelerated Inprocessing"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5023-5348","authenticated-orcid":false,"given":"Muhammad","family":"Osama","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2071-9624","authenticated-orcid":false,"given":"Anton","family":"Wijs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Abhinav, Nasre, R.: FastCollect: Offloading Generational Garbage Collection to integrated GPUs. In: 2016 International Conference on Compliers, Architectures, and Sythesis of Embedded Systems (CASES). pp. 1\u201310 (2016)","DOI":"10.1145\/2968455.2968520"},{"key":"8_CR2","unstructured":"Audemard, G., Simon, L.: Predicting Learnt Clauses Quality in Modern SAT Solvers. In: IJCAI 2009. pp. 399\u2013404. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (2009)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Bao, F.S., Gutierrez, C., Charles-Blount, J.J., Yan, Y., Zhang, Y.: Accelerating Boolean Satisfiability (SAT) solving by common subclause elimination. Artificial Intelligence Review 49(3), 439\u2013453 (2018)","DOI":"10.1007\/s10462-016-9530-6"},{"key":"8_CR4","unstructured":"Biere, A.: P$$\\{$$re, i$$\\}$$coSAT@SC\u201909. In: SAT 2009 competitive events booklet. pp. 41\u201343 (2009)"},{"key":"8_CR5","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT race 2010. FMV Report\u00a01, Johannes Kepler University (2010)"},{"key":"8_CR6","unstructured":"Biere, A.: CaDiCaL at the SAT Race 2019. In: Proc. SAT Race 2019: Solver and Benchmark Descriptions. Department of Computer Science Report Series - University of Helsinki, vol. B-2019-1, pp.\u00a08\u20139 (2019)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS 1999. pp. 193\u2013207. Springer (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Biere, A., J\u00e4rvisalo, M., Kiesl, B.: Preprocessing in SAT solving. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, IOS Press, 2nd edn. (2020), to be published","DOI":"10.3233\/FAIA336"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Biere, A., J\u00e4rvisalo, M., Le\u00a0Berre, D., Meel, K.S., Mengel, S.: The SAT Practitioner\u2019s Manifesto (Sep 2020). https:\/\/doi.org\/10.5281\/zenodo.4500928","DOI":"10.5281\/zenodo.4500928"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Billeter, M., Olsson, O., Assarsson, U.: Efficient Stream Compaction on Wide SIMD Many-Core Architectures. In: Proceedings of the Conference on High Performance Graphics 2009. pp. 159\u2013166. HPG \u201909, Association for Computing Machinery, New York, NY, USA (2009)","DOI":"10.1145\/1572769.1572795"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Bo\u0161na\u010dki, D., Edelkamp, S., Sulewski, D., Wijs, A.: GPU-PRISM: An Extension of PRISM for General Purpose Graphics Processing Units. In: PDMC-HiBi. pp. 17\u201319. IEEE Computer Society (2010)","DOI":"10.1109\/PDMC-HiBi.2010.11"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Bo\u0161na\u010dki, D., Odenbrett, M., Wijs, A., Ligtenberg, W., Hilbers, P.: Efficient reconstruction of biological networks via transitive reduction on general purpose graphics processors. BMC Bioinformatics 13(281) (2012)","DOI":"10.1186\/1471-2105-13-281"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: VMCAI 2011. pp. 70\u201387. Springer (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Brown, C.E.: Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. Journal of Automated Reasoning 51(1), 57\u201377 (Jun 2013)","DOI":"10.1007\/s10817-013-9283-8"},{"key":"8_CR15","unstructured":"Dal Pal\u00f9, A., Dovier, A., Formisano, A., Pontelli, E.: CUD@SAT: SAT solving on GPUs. Journal of Exper. & Theoret. Artificial Intelligence 27(3), 293\u2013316 (2015)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., Biere, A.: Effective Preprocessing in SAT Through Variable and Clause Elimination. In: SAT. LNCS, vol. 3569, pp. 61\u201375. Springer (2005)","DOI":"10.1007\/11499107_5"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: SAT. LNCS, vol. 2919, pp. 502\u2013518. Springer (2004)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"8_CR18","unstructured":"Eerd, J. van, Groote, J.F., Hijma, P., Martens, J., Wijs, A.J.: Term Rewriting on GPUs. In: FSEN. LNCS, Springer, to appear (2021)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Gebhardt, K., Manthey, N.: Parallel Variable Elimination on CNF Formulas. In: Timm, I.J., Thimm, M. (eds.) KI 2013: Advances in Artificial Intelligence. pp. 61\u201373. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-40942-4_6"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Han, H., Somenzi, F.: Alembic: An efficient algorithm for CNF preprocessing. In: Proc. 44th ACM\/IEEE Design Automation Conference. pp. 582\u2013587. IEEE (2007)","DOI":"10.1109\/DAC.2007.375231"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Clause Elimination Procedures for CNF Formulas. In: LPAR. LNCS, vol. 6397, pp. 357\u2013371. Springer (2010)","DOI":"10.1007\/978-3-642-16242-8_26"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.: Simulating circuit-level simplifications on CNF. Journal of Automated Reasoning 49(4), 583\u2013619 (2012)","DOI":"10.1007\/s10817-011-9239-9"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Heule, M.J., Biere, A.: Inprocessing Rules. In: IJCAR. LNCS, vol. 7364, pp. 355\u2013370. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Jin, H., Somenzi, F.: An incremental algorithm to check satisfiability for bounded model checking. ENTCS 119(2), 51\u201365 (2005)","DOI":"10.1016\/j.entcs.2004.06.062"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics 97, 149\u2013176 (1999)","DOI":"10.1016\/S0166-218X(99)00037-2"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Maas, M., Reames, P., Morlan, J., Asanovi\u0107, K., Joseph, A.D., Kubiatowicz, J.: GPUs as an Opportunity for Offloading Garbage Collection. SIGPLAN Not. 47(11), 25\u201336 (Jun 2012)","DOI":"10.1145\/2426642.2259002"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Glass, T.: Combinational equivalence checking using satisfiability and recursive learning. In: Design, Automation and Test in Europe Conference and Exhibition, 1999. Proceedings (Cat. No. PR00078). pp. 145\u2013149 (March 1999)","DOI":"10.1145\/307418.307477"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48(5), 506\u2013521 (1999)","DOI":"10.1109\/12.769433"},{"key":"8_CR29","unstructured":"Merrill, D.: CUB: A Parallel Primitives Library. NVLabs (2020), https:\/\/nvlabs.github.io\/cub\/"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Moness, M., Mahmoud, M.O., Moustafa, A.M.: A Real-Time Heterogeneous Emulator of a High-Fidelity Utility-Scale Variable-Speed Variable-Pitch Wind Turbine. IEEE Transactions on Industrial Informatics 14(2), 437\u2013447 (2018)","DOI":"10.1109\/TII.2017.2723960"},{"key":"8_CR31","unstructured":"NVIDIA: CUDA C Programming Guide (2020), https:\/\/docs.nvidia.com\/cuda\/cuda-c-programming-guide\/index.html"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Osama, M., Wijs, A.: Multiple Decision Making in Conflict-Driven Clause Learning. In: 2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI). pp. 161\u2013169 (2020)","DOI":"10.1109\/ICTAI50040.2020.00035"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Osama, M., Gaber, L., Hussein, A.I., Mahmoud, H.: An Efficient SAT-Based Test Generation Algorithm with GPU Accelerator. Journal of Electronic Testing 34(5), 511\u2013527 (Oct 2018)","DOI":"10.1007\/s10836-018-5747-4"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Osama, M., Wijs, A.: Parallel SAT Simplification on GPU Architectures. In: TACAS. LNCS, vol. 11427, pp. 21\u201340. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-17462-0_2"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Osama, M., Wijs, A.: SIGmA: GPU Accelerated Simplification of SAT Formulas. In: iFM. LNCS, vol. 11918, pp. 514\u2013522. Springer (2019)","DOI":"10.1007\/978-3-030-34968-4_29"},{"key":"8_CR36","unstructured":"Osama, M., Wijs, A.: ParaFROST, ParaFROST CBT, ParaFROST HRE, ParaFROST ALL at the SAT Race 2020. SAT Competition 2020 p.\u00a042 (2020)"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Ostrowski, R., Gr\u00e9goire, E., Mazure, B., Sais, L.: Recovering and Exploiting Structural Knowledge from CNF Formulas. In: Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming. pp. 185\u2013199. CP \u201902, Springer-Verlag, London, UK, UK (2002)","DOI":"10.1007\/3-540-46135-3_13"},{"key":"8_CR38","doi-asserted-by":"publisher","unstructured":"Soos, M., Kulkarni, R., Meel, K.S.: Crystalball: Gazing in the black box of SAT solving. In: Janota, M., Lynce, I. (eds.) Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9\u201312, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11628, pp. 371\u2013387. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_26","DOI":"10.1007\/978-3-030-24258-9_26"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"Springer, M., Masuhara, H.: Massively Parallel GPU Memory Compaction. In: ISMM. pp. 14\u201326. ACM (2019)","DOI":"10.1145\/3315573.3329979"},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"Stephan, P., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Combinational test generation using satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 15(9), 1167\u20131176 (1996)","DOI":"10.1109\/43.536723"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Subbarayan, S., Pradhan, D.K.: NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In: SAT. LNCS, vol. 3542, pp. 276\u2013291. Springer (2004)","DOI":"10.1007\/11527695_22"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Wijs, A.: GPU accelerated strong and branching bisimilarity checking. In: TACAS, LNCS, vol. 9035, pp. 368\u2013383. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_29"},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"Wijs, A., Neele, T., Bo\u0161na\u010dki, D.: GPUexplore 2.0: Unleashing GPU Explicit-state Model Checking. In: FM. LNCS, vol. 9995, pp. 694\u2013701. Springer (2016)","DOI":"10.1007\/978-3-319-48989-6_42"},{"key":"8_CR44","doi-asserted-by":"crossref","unstructured":"Youness, H., Ibraheim, A., Moness, M., Osama, M.: An Efficient Implementation of Ant Colony Optimization on GPU for the Satisfiability Problem. In: 2015 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing. pp. 230\u2013235 (March 2015)","DOI":"10.1109\/PDP.2015.59"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T00:06:24Z","timestamp":1616371584000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}