Towards Massively Parallel GPU Assisted SAT
Filippos Pantekis, Phillip James · 2022
Parallelisation of SAT is an area that faces many challenges, with current techniques often relying on the sharing of information between threads. In this work, we consider massively parallelising partial SAT checking using new GPGPU architec-tures in a manner that is both loosely coupled and fully scalable. Our work provides valuable lessons in implementing SAT style problems on such computing platforms and we demonstrate results that favour the use of GPGPU technology in heterogeneous CPU/GPU based SAT solvers. We do not propose our approach as a fully fledged SAT solver, as it currently uses a naïve search strategy, but we demonstrate techniques and results that favour the use of GPGPU technology for SAT based applications (e.g. through hybrid model checkers). In particular, we give details of our implementation along with an analysis of where performance has been gained via particular design choices.