论文标题
GPUSHARESAT：使用GPU进行子句共享的SAT求解器
GpuShareSat: a SAT solver using the GPU for clause sharing
论文作者
论文摘要
我们使用GPU（CUDA）和CPU使用新的子句交换策略来描述SAT求解器。 CPU运行经典的多线CDCL SAT求解器。每个CPU线程导出了其学习到GPU的所有条款。 GPU大量使用了位操作。它注意到CPU线程将使用子句何时通知该线程，在这种情况下，它会导入该子句。这取决于GPU反复测试数百万项作业的数百万条款。所有条款均可彼此独立测试（这允许GPU大规模并行方法），但使用位操作立即与所有分配进行了测试。这允许CPU线程仅导入对其有用的子句。我们的求解器基于葡萄糖响应。实验表明，这导致了强大的性能提高，而在2020年SAT竞赛中，与葡萄糖相结合的实例要多22个实例。
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.
