Study of Fine-grained Nested Parallelism in CDCL SAT Solvers

Autor:	James L. Edwards, Uzi Vishkin
Rok vydání:	2021
Předmět:	Speedup Nested parallelism Computer science Open problem Parallel algorithm Parallel computing Computer Science Applications Variety (cybernetics) Computational Theory and Mathematics Hardware and Architecture Modeling and Simulation Parallelism (grammar) Boolean satisfiability problem Software
Zdroj:	ACM Transactions on Parallel Computing. 8:1-18
ISSN:	2329-4957 2329-4949
Popis:	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× 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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::78c7c84e896dfeef9fdddb7fb60b4018 https://doi.org/10.1145/3470639 Zobrazit plný text záznamu