{"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":1792254188502,"version":"4.4.0"},"reference-count":69,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T00:00:00Z","timestamp":1690934400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T00:00:00Z","timestamp":1690934400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003958","name":"Stichting voor de Technische Wetenschappen","doi-asserted-by":"crossref","award":["TOP2.16.044"],"award-info":[{"award-number":["TOP2.16.044"]}],"id":[{"id":"10.13039\/501100003958","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Since 2013, the leading SAT solvers in SAT competitions all use inprocessing, which, unlike preprocessing, interleaves search with simplifications. However, inprocessing is typically a performance bottleneck, in particular for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As one of the main challenges in GPU programming is memory locality, we present new compact data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improve memory locality. Our new parallel variable elimination algorithm is roughly twice as fast as previous work. Moreover, we augment the variable elimination with the first parallel algorithm for functional dependency extraction in an attempt to find more logical gates to eliminate that cannot be found with syntactic approaches. We present a novel algorithm to generate clausal proofs in parallel to validate all simplifications running on the GPU besides the CDCL search, giving high credibility to our solver and its use in critical applications such as model checkers. In experiments, our new solver <jats:sc>ParaFROST<\/jats:sc> solves numerous benchmarks faster on the GPU than its sequential counterparts. With functional dependency extraction, inprocessing in <jats:sc>ParaFROST<\/jats:sc> was more effective in reducing the solving time. Last but not least, all proofs generated by <jats:sc>ParaFROST<\/jats:sc> were successfully verified.<\/jats:p>","DOI":"10.1007\/s10703-023-00432-z","type":"journal-article","created":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T17:01:43Z","timestamp":1690995703000},"page":"79-118","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Certified SAT solving with GPU accelerated inprocessing"],"prefix":"10.1007","volume":"62","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":[[2023,8,2]]},"reference":[{"key":"432_CR1","doi-asserted-by":"publisher","unstructured":"Abhinav, Nasre R (2016) FastCollect: offloading generational garbage collection to integrated GPUs. In: CASES, Pittsburgh, Pennsylvania, USA, October 1\u20137, 2016. Proceedings. ACM, pp 21:1\u201321:10. https:\/\/doi.org\/10.1145\/2968455.2968520","DOI":"10.1145\/2968455.2968520"},{"key":"432_CR2","doi-asserted-by":"publisher","unstructured":"Audemard G, Simon L (2009) Predicting learnt clauses quality in modern SAT solvers. In: IJCAI, Pasadena, California, USA, July 11\u201317, 2009, pp 399\u2013404. https:\/\/doi.org\/10.5555\/1661445.1661509","DOI":"10.5555\/1661445.1661509"},{"issue":"5","key":"432_CR3","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/MC.2016.127","volume":"49","author":"HE Bal","year":"2016","unstructured":"Bal HE, Epema DHJ, de Laat C et al (2016) A medium-scale distributed system for computer science research: infrastructure for the long term. Computer 49(5):54\u201363. https:\/\/doi.org\/10.1109\/MC.2016.127","journal-title":"Computer"},{"issue":"3","key":"432_CR4","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/s10462-016-9530-6","volume":"49","author":"FS Bao","year":"2018","unstructured":"Bao FS, Gutierrez CE, Jn-Charles J et al (2018) Accelerating Boolean satisfiability (SAT) solving by common subclause elimination. Artif Intell Rev 49(3):439\u2013453. https:\/\/doi.org\/10.1007\/s10462-016-9530-6","journal-title":"Artif Intell Rev"},{"key":"432_CR5","unstructured":"Biere A (2013) Lingeling, plingeling and treengeling entering the SAT competition 2013. In: Proceedings of SAT competition 2013\u2014solver and benchmark descriptions, Department of Computer Science report series B, vol B-2013-1. University of Helsinki, p\u00a01"},{"key":"432_CR6","doi-asserted-by":"publisher","unstructured":"Biere A, Cimatti A, Clarke EM et al (1999) Symbolic model checking without BDDs. In: TACAS, Amsterdam, The Netherlands, March 22\u201328, 1999. Proceedings, LNCS, vol 1579. Springer, pp 193\u2013207. https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"432_CR7","unstructured":"Biere A, Fleury M (2021) Mining definitions in Kissat with kittens. In: Workshop on the pragmatics of SAT 2021. http:\/\/www.pragmaticsofsat.org\/2021\/"},{"key":"432_CR8","unstructured":"Biere A, Fleury M, Heisinger M (2021) CADICAL, KISSAT, PARACOST. In: Proceedings of SAT competition 2021\u2014solver and benchmark descriptions, Department of Computer Science report series B, vol B-2021-1. University of Helsinki, pp 10\u201313"},{"key":"432_CR9","doi-asserted-by":"crossref","unstructured":"Biere A, J\u00e4rvisalo M, Kiesl B (2020) Preprocessing in SAT solving. In: Handbook of satisfiability, 2nd edn. Frontiers in Artificial Intelligence and Applications, IOS Press","DOI":"10.3233\/FAIA200992"},{"key":"432_CR10","doi-asserted-by":"publisher","unstructured":"Biere A, J\u00e4rvisalo M, Le Berre D et al (2020). The SAT practitioner\u2019s manifesto. https:\/\/doi.org\/10.5281\/zenodo.4500928","DOI":"10.5281\/zenodo.4500928"},{"key":"432_CR11","doi-asserted-by":"publisher","unstructured":"Billeter M, Olsson O, Assarsson U (2009) Efficient stream compaction on wide SIMD many-core architectures. In: HPG, New Orleans, Louisiana, USA, August 1\u20133, 2009. Proceedings. Eurographics Association, pp 159\u2013166. https:\/\/doi.org\/10.2312\/EGGH\/HPG09\/159-166","DOI":"10.2312\/EGGH\/HPG09\/159-166"},{"key":"432_CR12","doi-asserted-by":"publisher","unstructured":"Bo\u0161na\u010dki D, Edelkamp S, Sulewski D et\u00a0al (2010) GPU-PRISM: an extension of PRISM for general purpose graphics processing units. In: PDMC-HiBi, pp 17\u201319. https:\/\/doi.org\/10.1109\/PDMC-HiBi.2010.11","DOI":"10.1109\/PDMC-HiBi.2010.11"},{"key":"432_CR13","doi-asserted-by":"publisher","unstructured":"Bradley AR (2011) SAT-based model checking without unrolling. In: VMCAI, Austin, TX, USA, January 23\u201325, 2011. Proceedings, LNCS, vol 6538. Springer, pp 70\u201387. https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"issue":"1","key":"432_CR14","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10817-013-9283-8","volume":"51","author":"CE Brown","year":"2013","unstructured":"Brown CE (2013) Reducing higher-order theorem proving to a sequence of SAT problems. J Autom Reason 51(1):57\u201377. https:\/\/doi.org\/10.1007\/s10817-013-9283-8","journal-title":"J Autom Reason"},{"issue":"1","key":"432_CR15","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s10703-017-0272-0","volume":"50","author":"G Cabodi","year":"2017","unstructured":"Cabodi G, Camurati P, Mishchenko A et al (2017) SAT solver management strategies in IC3: an experimental approach. Formal Methods Syst Des 50(1):39\u201374. https:\/\/doi.org\/10.1007\/s10703-017-0272-0","journal-title":"Formal Methods Syst Des"},{"issue":"1","key":"432_CR16","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke EM, Biere A, Raimi R et al (2001) Bounded model checking using satisfiability solving. Formal Methods Syst Des 19(1):7\u201334. https:\/\/doi.org\/10.1023\/A:1011276507260","journal-title":"Formal Methods Syst Des"},{"issue":"7","key":"432_CR17","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 DW (1962) A machine program for theorem-proving. Commun ACM 5(7):394\u2013397. https:\/\/doi.org\/10.1145\/368273.368557","journal-title":"Commun ACM"},{"key":"432_CR18","doi-asserted-by":"publisher","unstructured":"E\u00e9n N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: SAT, St. Andrews, UK, June 19\u201323, 2005. Proceedings, LNCS, vol 3569. Springer, pp 61\u201375. https:\/\/doi.org\/10.1007\/11499107_5","DOI":"10.1007\/11499107_5"},{"key":"432_CR19","doi-asserted-by":"publisher","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) An extensible SAT-solver. In: SAT, Italy, May 5\u20138, 2003, selected revised papers, LNCS, vol 2919. Springer, pp 502\u2013518. https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"432_CR20","unstructured":"Fleury M, Biere A (2022) Mining definitions in Kissat with kittens. Extended version of our unpublished POS\u201921 paper [6], pp 1\u201322. Submitted to a special issue of a journal"},{"key":"432_CR21","doi-asserted-by":"publisher","unstructured":"Gebhardt K, Manthey N (2013) Parallel variable elimination on CNF formulas. In: KI, Koblenz, Germany, September 16\u201320, 2013. Proceedings, LNCS, vol 8077. Springer, pp 61\u201373. https:\/\/doi.org\/10.1007\/978-3-642-40942-4_6","DOI":"10.1007\/978-3-642-40942-4_6"},{"key":"432_CR22","doi-asserted-by":"publisher","unstructured":"Han H, Somenzi F (2007) Alembic: an efficient algorithm for CNF preprocessing. In: DAC, San Diego, CA, USA, June 4\u20138, 2007. IEEE, pp 582\u2013587. https:\/\/doi.org\/10.1145\/1278480.1278628","DOI":"10.1145\/1278480.1278628"},{"key":"432_CR23","doi-asserted-by":"publisher","unstructured":"Heule Jr MWAH, Wetzler N (2013) Trimming while checking clausal proofs. In: FMCAD, Portland, OR, USA, October 20\u201323, 2013. IEEE, pp 181\u2013188. https:\/\/doi.org\/10.1109\/FMCAD.2013.6679408","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"432_CR24","doi-asserted-by":"publisher","unstructured":"Heule Jr MWAH, Wetzler N (2013) Verifying refutations with extended resolution. In: CADE-24, Lake Placid, NY, USA, June 9\u201314, 2013. Proceedings, LNCS, vol 7898. Springer, pp 345\u2013359. https:\/\/doi.org\/10.1007\/978-3-642-38574-2_24","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"432_CR25","doi-asserted-by":"publisher","unstructured":"Heule M, J\u00e4rvisalo M, Biere A (2010) Clause elimination procedures for CNF formulas. In: LPAR, Yogyakarta, Indonesia, October 10\u201315, 2010. Proceedings, LNCS, vol 6397. Springer, pp 357\u2013371. https:\/\/doi.org\/10.1007\/978-3-642-16242-8_26","DOI":"10.1007\/978-3-642-16242-8_26"},{"issue":"4","key":"432_CR26","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/s10817-011-9239-9","volume":"49","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo M, Biere A, Heule M (2012) Simulating circuit-level simplifications on CNF. J Autom Reason 49(4):583\u2013619. https:\/\/doi.org\/10.1007\/s10817-011-9239-9","journal-title":"J Autom Reason"},{"key":"432_CR27","doi-asserted-by":"publisher","unstructured":"J\u00e4rvisalo M, Heule M, Biere A (2012b) Inprocessing rules. In: IJCAR 2012, Manchester, UK, June 26\u201329, 2012. Proceedings, LNCS, vol 7364. Springer, pp 355\u2013370. https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"432_CR28","doi-asserted-by":"publisher","unstructured":"Johnson DS, Trick MA (1996) Cliques, coloring, and satisfiability. In: DIMACS workshop, New Brunswick, New Jersey, USA, October 11\u201313, 1993. Proceedings, DIMACS series in discrete mathematics and theoretical computer science, vol\u00a026. DIMACS\/AMS. https:\/\/doi.org\/10.1090\/dimacs\/026","DOI":"10.1090\/dimacs\/026"},{"issue":"2","key":"432_CR29","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s00224-015-9653-1","volume":"59","author":"G Kov\u00e1sznai","year":"2016","unstructured":"Kov\u00e1sznai G, Fr\u00f6hlich A, Biere A (2016) Complexity of fixed-size bit-vector logics. Theory Comput Syst 59(2):323\u2013376. https:\/\/doi.org\/10.1007\/s00224-015-9653-1","journal-title":"Theory Comput Syst"},{"key":"432_CR30","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann O (1999) On a generalization of extended resolution. Discrete Appl Math 96\u201397:149\u2013176. https:\/\/doi.org\/10.1016\/S0166-218X(99)00037-2","journal-title":"Discrete Appl Math"},{"issue":"1","key":"432_CR31","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/s10703-020-00356-y","volume":"58","author":"M Kwiatkowska","year":"2021","unstructured":"Kwiatkowska M, Norman G, Parker D et al (2021) Automatic verification of concurrent stochastic systems. Formal Methods Syst Des 58(1):188\u2013250. https:\/\/doi.org\/10.1007\/s10703-020-00356-y","journal-title":"Formal Methods Syst Des"},{"key":"432_CR32","unstructured":"Li CM (2000) Integrating equivalency reasoning into Davis\u2013Putnam procedure. AAAI, IAAI, July 30\u2013August 3, 2000. USA. AAAI Press\/The MIT Press, Austin, pp 291\u2013296"},{"issue":"3","key":"432_CR33","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/s10703-016-0247-6","volume":"48","author":"T Liang","year":"2016","unstructured":"Liang T, Reynolds A, Tsiskaridze N et al (2016) An efficient SMT solver for string constraints. Formal Methods Syst Des 48(3):206\u2013234. https:\/\/doi.org\/10.1007\/s10703-016-0247-6","journal-title":"Formal Methods Syst Des"},{"issue":"1","key":"432_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton MH, Sakallah KA (2008) Algorithms for computing minimal unsatisfiable subsets of constraints. J Autom Reason 40(1):1\u201333. https:\/\/doi.org\/10.1007\/s10817-007-9084-z","journal-title":"J Autom Reason"},{"key":"432_CR35","doi-asserted-by":"publisher","unstructured":"Lynce I, Silva JPM (2003) Probing-based preprocessing techniques for propositional satisfiability. In: ICTAI, 3\u20135 November 2003, Sacramento, California, USA. IEEE Computer Society, p 105. https:\/\/doi.org\/10.1109\/TAI.2003.1250177","DOI":"10.1109\/TAI.2003.1250177"},{"key":"432_CR36","doi-asserted-by":"publisher","unstructured":"Maas M, Reames P, Morlan J et al (2012) GPUs as an opportunity for offloading garbage collection. In: ISMM, Beijing, China, June 15\u201316, 2012. Proceedings. ACM, pp 25\u201336. https:\/\/doi.org\/10.1145\/2258996.2259002","DOI":"10.1145\/2258996.2259002"},{"issue":"2","key":"432_CR37","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1109\/TII.2017.2723960","volume":"14","author":"M Moness","year":"2018","unstructured":"Moness M, Mahmoud MO, Moustafa AM (2018) A real-time heterogeneous emulator of a high-fidelity utility-scale variable-speed variable-pitch wind turbine. IEEE Trans Ind Inform 14(2):437\u2013447. https:\/\/doi.org\/10.1109\/TII.2017.2723960","journal-title":"IEEE Trans Ind Inform"},{"key":"432_CR38","doi-asserted-by":"publisher","unstructured":"Munshi A (2009) The OpenCL specification. In: 2009 IEEE hot chips 21 symposium (HCS), Stanford, CA, USA, August 23\u201325, 2009. IEEE, pp 1\u2013314. https:\/\/doi.org\/10.1109\/HOTCHIPS.2009.7478342","DOI":"10.1109\/HOTCHIPS.2009.7478342"},{"key":"432_CR39","unstructured":"NVIDIA (2022) CUDA C programming guide. https:\/\/docs.nvidia.com\/cuda\/cuda-c-programming-guide"},{"key":"432_CR40","doi-asserted-by":"publisher","unstructured":"Osama M (2021) Large SAT benchmark suite for certified SAT solving with GPU accelerated inprocessing. https:\/\/doi.org\/10.5281\/zenodo.5138008","DOI":"10.5281\/zenodo.5138008"},{"key":"432_CR41","doi-asserted-by":"publisher","unstructured":"Osama M (2021) PARAFROST proofs for certified SAT solving with GPU accelerated inprocessing. https:\/\/doi.org\/10.5281\/zenodo.5137887","DOI":"10.5281\/zenodo.5137887"},{"key":"432_CR42","unstructured":"Osama M (2022) GPU enabled automated reasoning. Ph.D. thesis, Eindhoven University of Technology. ISBN: 978-90-386-5445-4"},{"issue":"5","key":"432_CR43","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/s10836-018-5747-4","volume":"34","author":"M Osama","year":"2018","unstructured":"Osama M, Gaber L, Hussein AI et al (2018) An efficient SAT-based test generation algorithm with GPU accelerator. J Electron Test 34(5):511\u2013527. https:\/\/doi.org\/10.1007\/s10836-018-5747-4","journal-title":"J Electron Test"},{"key":"432_CR44","doi-asserted-by":"publisher","unstructured":"Osama M, Wijs A (2019) Parallel SAT simplification on GPU architectures. In: TACAS, Prague, Czech Republic, April 6\u201311, 2019. Proceedings, Part I, LNCS, vol 11427. Springer, pp 21\u201340. https:\/\/doi.org\/10.1007\/978-3-030-17462-0_2","DOI":"10.1007\/978-3-030-17462-0_2"},{"key":"432_CR45","doi-asserted-by":"publisher","unstructured":"Osama M, Wijs A (2019) SIGMA: GPU accelerated simplification of SAT formulas. In: IFM, Bergen, Norway, December 2\u20136, 2019. Proceedings, LNCS, vol 11918. Springer, pp 514\u2013522. https:\/\/doi.org\/10.1007\/978-3-030-34968-4_29","DOI":"10.1007\/978-3-030-34968-4_29"},{"key":"432_CR46","doi-asserted-by":"publisher","unstructured":"Osama M, Wijs A (2020) Multiple decision making in conflict-driven clause learning. In: ICTAI, Baltimore, MD, USA, November 9\u201311, 2020. IEEE, pp 161\u2013169. https:\/\/doi.org\/10.1109\/ICTAI50040.2020.00035","DOI":"10.1109\/ICTAI50040.2020.00035"},{"key":"432_CR47","doi-asserted-by":"publisher","unstructured":"Osama M, Wijs A (2021) GPU acceleration of bounded model checking with ParaFROST. In: CAV, Los Angeles, July 18\u201324, 2021. Proceedings, Part II. Springer, LNCS, pp 447\u2013460. https:\/\/doi.org\/10.1007\/978-3-030-81688-9_21","DOI":"10.1007\/978-3-030-81688-9_21"},{"key":"432_CR48","doi-asserted-by":"publisher","unstructured":"Osama M, Wijs A, Biere A (2021) SAT solving with GPU accelerated inprocessing. In: TACAS, Luxembourg, March 27\u2013April 1, 2021. Proceedings, Part I, LNCS, vol 12651. Springer, pp 133\u2013151. https:\/\/doi.org\/10.1007\/978-3-030-72016-2_8","DOI":"10.1007\/978-3-030-72016-2_8"},{"key":"432_CR49","doi-asserted-by":"publisher","unstructured":"Ostrowski R, Gr\u00e9goire \u00c9, Mazure B et al (2002) Recovering and exploiting structural knowledge from CNF formulas. In: CP, Ithaca, NY, USA, September 9\u201313, 2002. Proceedings, LNCS, vol 2470. Springer, pp 185\u2013199. https:\/\/doi.org\/10.1007\/3-540-46135-3_13","DOI":"10.1007\/3-540-46135-3_13"},{"issue":"3","key":"432_CR50","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1080\/0952813X.2014.954274","volume":"27","author":"AD Pal\u00f9","year":"2015","unstructured":"Pal\u00f9 AD, Dovier A, Formisano A et al (2015) CUD@SAT: SAT solving on GPUs. J Exp Theor Artif Intell 27(3):293\u2013316. https:\/\/doi.org\/10.1080\/0952813X.2014.954274","journal-title":"J Exp Theor Artif Intell"},{"key":"432_CR51","doi-asserted-by":"publisher","unstructured":"Piette C, Hamadi Y, Sais L (2008) Vivifying propositional clausal formulae. In: ECAI, Patras, Greece, July 21\u201325, 2008. Proceedings, Frontiers in Artificial Intelligence and Applications, vol 178. IOS Press, pp 525\u2013529. https:\/\/doi.org\/10.3233\/978-1-58603-891-5-525","DOI":"10.3233\/978-1-58603-891-5-525"},{"key":"432_CR52","doi-asserted-by":"publisher","unstructured":"Prevot N, Soos M, Meel KS (2021) Leveraging GPUs for effective clause sharing in parallel SAT solving. In: SAT, Barcelona, Spain, July 5\u20139, 2021. Proceedings, LNCS, vol 12831. Springer, pp 471\u2013487. https:\/\/doi.org\/10.1007\/978-3-030-80223-3_32","DOI":"10.1007\/978-3-030-80223-3_32"},{"key":"432_CR53","doi-asserted-by":"publisher","unstructured":"Silva JPM, Glass T (1999) Combinational equivalence checking using satisfiability and recursive learning. In: DATE, 9\u201312 March 1999, Munich, Germany. IEEE Computer Society\/ACM, pp 145\u2013149. https:\/\/doi.org\/10.1109\/DATE.1999.761110","DOI":"10.1109\/DATE.1999.761110"},{"issue":"5","key":"432_CR54","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JPM Silva","year":"1999","unstructured":"Silva JPM, Sakallah KA (1999) GRASP: a search algorithm for propositional satisfiability. IEEE Trans Comput 48(5):506\u2013521. https:\/\/doi.org\/10.1109\/12.769433","journal-title":"IEEE Trans Comput"},{"key":"432_CR55","doi-asserted-by":"publisher","unstructured":"Soos M, Kulkarni R, Meel KS (2019) CrystalBall: gazing in the black box of SAT solving. In: SAT, Lisbon, Portugal, July 9\u201312, 2019. Proceedings, LNCS, vol 11628. Springer, pp 371\u2013387. https:\/\/doi.org\/10.1007\/978-3-030-24258-9_26","DOI":"10.1007\/978-3-030-24258-9_26"},{"key":"432_CR56","doi-asserted-by":"publisher","unstructured":"Springer M, Masuhara H (2019) Massively parallel GPU memory compaction. In: ISMM, Phoenix, AZ, USA, June 23, 2019. Proceedings. ACM, pp 14\u201326. https:\/\/doi.org\/10.1145\/3315573.3329979","DOI":"10.1145\/3315573.3329979"},{"issue":"9","key":"432_CR57","doi-asserted-by":"publisher","first-page":"1167","DOI":"10.1109\/43.536723","volume":"15","author":"PR Stephan","year":"1996","unstructured":"Stephan PR, Brayton RK, Sangiovanni-Vincentelli AL (1996) Combinational test generation using satisfiability. IEEE Trans Comput Aided Des Integr Circuits Syst 15(9):1167\u20131176. https:\/\/doi.org\/10.1109\/43.536723","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"432_CR58","doi-asserted-by":"publisher","unstructured":"Subbarayan S, Pradhan DK (2004) NiVER: non increasing variable elimination resolution for preprocessing SAT instances. In: SAT, 10\u201313 May 2004, Vancouver, BC, Canada, Online Proceedings. https:\/\/doi.org\/10.1007\/11527695_22","DOI":"10.1007\/11527695_22"},{"key":"432_CR59","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"On the complexity of derivation in propositional calculus","author":"GS Tseitin","year":"1983","unstructured":"Tseitin GS (1983) On the complexity of derivation in propositional calculus. Springer, Berlin, pp 466\u2013483. https:\/\/doi.org\/10.1007\/978-3-642-81955-1_28"},{"issue":"3","key":"432_CR60","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/s10703-017-0284-9","volume":"51","author":"VX Tung","year":"2017","unstructured":"Tung VX, Khanh TV, Ogawa M (2017) raSAT: an SMT solver for polynomial constraints. Formal Methods Syst Des 51(3):462\u2013499. https:\/\/doi.org\/10.1007\/s10703-017-0284-9","journal-title":"Formal Methods Syst Des"},{"key":"432_CR61","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2022.102910","volume":"225","author":"J van Eerd","year":"2023","unstructured":"van Eerd J, Groote JF, Hijma P et al (2023) Innermost many-sorted term rewriting on GPUs. Sci Comput Program 225:102910. https:\/\/doi.org\/10.1016\/j.scico.2022.102910","journal-title":"Sci Comput Program"},{"key":"432_CR62","doi-asserted-by":"crossref","unstructured":"van Eerd J, Groote JF, Hijma P et al (2020) Term rewriting on GPUs. CoRR arXiv:2009.07174","DOI":"10.1007\/978-3-030-89247-0_12"},{"key":"432_CR63","doi-asserted-by":"publisher","unstructured":"Wetzler N, Heule Jr MWAH (2014) DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: SAT, Vienna, Austria, July 14\u201317, 2014. Proceedings, LNCS, vol 8561. Springer, pp 422\u2013429. https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"432_CR64","doi-asserted-by":"publisher","unstructured":"Wijs A (2015) GPU accelerated strong and branching bisimilarity checking. In: TACAS, London, UK, April 11\u201318, 2015. Proceedings, LNCS, vol 9035. Springer, pp 368\u2013383. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_29","DOI":"10.1007\/978-3-662-46681-0_29"},{"key":"432_CR65","doi-asserted-by":"publisher","unstructured":"Wijs A, Bosnacki D (2014) GPUexplore: many-core on-the-fly state space exploration using GPUs. In: TACAS, Grenoble, France, April 5\u201313, 2014. Proceedings, LNCS, vol 8413. Springer, pp 233\u2013247. https:\/\/doi.org\/10.1007\/978-3-642-54862-8_16","DOI":"10.1007\/978-3-642-54862-8_16"},{"key":"432_CR66","doi-asserted-by":"crossref","unstructured":"Wijs A, Osama M (2023) A GPU tree database for many-core explicit state space exploration. In: TACAS. Springer, to appear, LNCS","DOI":"10.1007\/978-3-031-30823-9_35"},{"key":"432_CR67","doi-asserted-by":"crossref","unstructured":"Wijs A, Osama M (2023b) GPUexplore 3.0: GPU accelerated state space exploration for concurrent systems with data. In: SPIN. Springer, to appear, LNCS","DOI":"10.1007\/978-3-031-32157-3_11"},{"key":"432_CR68","doi-asserted-by":"publisher","unstructured":"Youness HA, Ibraheim A, Moness M et al (2015) An efficient implementation of ant colony optimization on GPU for the satisfiability problem. In: PDP, Turku, Finland, March 4\u20136, 2015. IEEE Computer Society, pp 230\u2013235. https:\/\/doi.org\/10.1109\/PDP.2015.59","DOI":"10.1109\/PDP.2015.59"},{"key":"432_CR69","doi-asserted-by":"publisher","first-page":"102920","DOI":"10.1109\/ACCESS.2020.2999382","volume":"8","author":"H Youness","year":"2020","unstructured":"Youness H, Osama M, Hussein A et al (2020) An effective SAT solver utilizing ACO based on heterogenous systems. IEEE Access 8:102920\u2013102934. https:\/\/doi.org\/10.1109\/ACCESS.2020.2999382","journal-title":"IEEE Access"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00432-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00432-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00432-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,3]],"date-time":"2024-06-03T16:11:35Z","timestamp":1717431095000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00432-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,2]]},"references-count":69,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["432"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00432-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,2]]},"assertion":[{"value":"23 December 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 June 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 August 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}