Muhammad Osama, Anton Wijs, Armin Biere,
"SAT Solving with GPU Accelerated Inprocessing"
: Proc. 14th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Serie Lecture Notes in Computer Science (LNCS), Vol. vol. 12651, Springer, Seite(n) 131-151, 2021
SAT Solving with GPU Accelerated Inprocessing
Sprache des Titels:
Proc. 14th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Since 2013, the leading SAT solvers in the SAT competition all use in-processing, which unlike preprocessing, interleaves search with simplifications.However, applying inprocessing frequently can still be a bottle neck, i.e., for hardor large formulas. In this work, we introduce the first attempt to parallelize in-processing on GPU architectures. As memory is a scarce resource in GPUs, wepresent new space-efficient data structures and devise a data-parallel garbage col-lector. It runs in parallel on the GPU to reduce memory consumption and im-proves memory access locality. Our new parallel variable elimination algorithmis twice as fast as previous work. In experiments our new solver PARAFROSTsolves many benchmarks faster on the GPU than its sequential counterparts.