GpuShareSat: a SAT solver using the GPU for clause sharing
We describe a SAT solver using both the GPU (CUDA) and the CPU with a new clause exchange strategy. The CPU runs a classic multithreaded CDCL SAT solver. EachCPU thread exports all the clauses it learns to the GPU. The GPU makes a heavy usage of bitwise operations. It notices when a clause would have been used by a CPU thread and notifies that thread, in which case it imports that clause. This relies on the GPU repeatedly testing millions of clauses against hundreds of assignments. All the clauses are tested independantly from each other (which allows the GPU massively parallel approach), but against all the assignments at once, using bitwise operations. This allows CPU threads to only import clauses which would have been useful for them. Our solver is based upon glucose-syrup. Experiments show that this leads to a strong performance improvement, with 22 more instances solved on the SAT 2020 competition than glucose-syrup.
Code (0)
등록된 구현이 없습니다.
Tasks
AllCPUGPUSimilar Papers 제목 키워드 기반
An Experimental Study of Permanently Stored Learned Clauses
Modern CDCL SAT solvers learn clauses rapidly, and an important heuristic is the clause deletion scheme. Most current solvers have two (or more) stores of clauses. One has ``valuable'' clauses which are never deleted. Mo…
Component Sharing in English and Chinese Clause Complex
NT Clause Complex Framework defines a clause complex as a combination of NT clauses through component sharing and logic-semantic relationship. This paper clarifies the existence of component sharing mechanism in both Eng…
Machine TranslationTranslationToo much information: why CDCL solvers need to forget learned clauses
Conflict-driven clause learning (CDCL) is a remarkably successful paradigm for solving the satisfiability problem of propositional logic. Instead of a simple depth-first backtracking approach, this kind of solver learns …
Clause Vivification by Unit Propagation in CDCL SAT Solvers
Original and learnt clauses in Conflict-Driven Clause Learning (CDCL) SAT solvers often contain redundant literals. This may have a negative impact on performance because redundant literals may deteriorate both the effec…
Local Consistency and SAT-Solvers
Local consistency techniques such as k-consistency are a key component of specialised solvers for constraint satisfaction problems. In this paper we show that the power of using k-consistency techniques on a constraint s…