TY - GEN
T1 - SAT Solving with GPU Accelerated Inprocessing
AU - Osama, Muhammad
AU - Wijs, Anton J.
AU - Biere, Armin
PY - 2021
Y1 - 2021
N2 - Since 2013, the leading SAT solvers in the SAT competition all use inprocessing, which unlike preprocessing, interleaves search with simplifications. However, applying inprocessing frequently can still be a bottle neck, i.e., for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As memory is a scarce resource in GPUs, we present new space-efficient data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improves memory access locality. Our new parallel variable elimination algorithm is twice as fast as previous work. In experiments our new solver PARAFROST solves many benchmarks faster on the GPU than its sequential counterparts.
AB - Since 2013, the leading SAT solvers in the SAT competition all use inprocessing, which unlike preprocessing, interleaves search with simplifications. However, applying inprocessing frequently can still be a bottle neck, i.e., for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As memory is a scarce resource in GPUs, we present new space-efficient data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improves memory access locality. Our new parallel variable elimination algorithm is twice as fast as previous work. In experiments our new solver PARAFROST solves many benchmarks faster on the GPU than its sequential counterparts.
KW - Eager Redundancy Elimination
KW - GPU
KW - Parallel Garbage Collection
KW - Parallel SAT Inprocessing
KW - Satisfiability
KW - Variable Elimination
UR - http://www.scopus.com/inward/record.url?scp=85150185146&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-72016-2_8
DO - 10.1007/978-3-030-72016-2_8
M3 - Conference contribution
SN - 9783030720155
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 133
EP - 151
BT - Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021
A2 - Groote, Jan Friso
A2 - Larsen, Kim Guldstrand
PB - Springer
ER -