GpuShareSat：一种利用GPU进行子句共享的SAT求解器
人工智能
2020-12-08 v1
摘要
我们描述了一种同时使用GPU(CUDA)与CPU并采用新子句交换策略的SAT求解器。CPU运行经典的 multithreaded CDCL SAT求解器。每个CPU线程将其学到的所有子句导出至GPU。GPU大量使用按位运算。它注意到某个子句本会被某CPU线程使用，并通知该线程，此时该线程导入该子句。这依赖于GPU针对数百个赋值反复测试数百万条子句。所有子句彼此独立测试（这使得GPU的大规模并行方法成为可能），但使用按位运算一次性针对所有赋值进行测试。这使得CPU线程仅导入对它们有用的子句。我们的求解器基于glucose-syrup。实验表明，这带来了显著的性能提升，在SAT 2020竞赛中比glucose-syrup多求解了22个实例。
引用
@article{arxiv.2012.03119,
title = {GpuShareSat: a SAT solver using the GPU for clause sharing},
author = {Nicolas Prevot},
journal= {arXiv preprint arXiv:2012.03119},
year = {2020}
}
备注
13 pages, 4 figures