Although state-of-the-art (SOTA) SAT solvers based on conflict-driven clause learning (CDCL) have achieved remarkable engineering success, their sequential nature limits the parallelism that may be extracted for acceleration on platforms such as the graphics processing unit (GPU). In this work, we propose FastFourierSAT, a highly parallel hybrid SAT solver based on gradient-driven continuous local search (CLS). This is realized by a novel parallel algorithm inspired by the Fast Fourier Transform (FFT)-based convolution for computing the elementary symmetric polynomials (ESPs), which is the major computational task in previous CLS methods. The complexity of our algorithm matches the best previous result. Furthermore, the substantial parallelism inherent in our algorithm can leverage the GPU for acceleration, demonstrating significant improvement over the previous CLS approaches. We also propose to incorporate the restart heuristics in CLS to improve search efficiency. We compare our approach with the SOTA parallel SAT solvers on several benchmarks. Our results show that FastFourierSAT computes the gradient 100+ times faster than previous prototypes implemented on CPU. Moreover, FastFourierSAT solves most instances and demonstrates promising performance on larger-size instances.

翻译：尽管基于冲突驱动子句学习（CDCL）的最先进SAT求解器已取得显著的工程成就，但其串行特性限制了在图形处理器（GPU）等平台上可并行加速的空间。本研究提出FastFourierSAT——一种基于梯度驱动连续局部搜索（CLS）的高度并行混合SAT求解器。该求解器通过受快速傅里叶变换（FFT）卷积启发的新型并行算法实现，用于计算先前CLS方法中的核心计算任务——初等对称多项式（ESP）。所提算法的复杂度匹配已有最优结果，且其内在的显著并行性可借助GPU实现加速，展现出对先前CLS方法的重大改进。我们还提出在CLS中融入重启启发式策略以提升搜索效率。在多个基准测试上对比最先进并行SAT求解器，结果表明FastFourierSAT的梯度计算速度比先前基于CPU的原型系统快100倍以上。此外，FastFourierSAT可求解大部分实例，并在大规模实例上展现出有前景的性能表现。