TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System
Steve Dai, Cunxi Yu, Kalyan Krishnamani, Brucek Khailany
虽然加速计算已经改变了许多计算领域,但它对逻辑推理的影响,特别是布尔的可满足性(SAT),仍然有限。 最先进的SAT求解器在很大程度上依赖于固有的顺序冲突驱动的搜索算法,这些算法提供了强大的启发式,但限制了并行性的数量,否则可以实现更具可扩展性的SAT解决。 受神经网络训练的启发,我们将SAT问题制定为双线性矩阵乘法层,可以使用可微分的客观函数进行优化。 通过这种编码,我们结合了并行可微分优化和顺序搜索的优势,以加速混合GPU-CPU系统的SAT。 在这个系统中,GPU利用并行可微解来快速评估SAT子句,并使用梯度来随机探索解决方案空间并优化变量分配。 GPU 生成的有希望的部分赋值是在许多 CPU 线程上进行后处理的,这些线程利用冲突驱动的顺序搜索来进一步遍历解决方案子空间并识别完整的分配。 在 NVIDIA DGX GB200 节点上对混合求解器进行原型,与 SAT 竞赛中基于公共可满足基准问题的最先进的基于 CPU 的求解器相比,我们的求解器实现了高达 200 倍的运行时速度。
While accelerated computing has transformed many domains of computing, its impact on logical reasoning, specifically Boolean satisfiability (SAT), remains limited. State-of-the-art SAT solvers rely heavily on inherently sequential conflict-driven search algorithms that offer powerful heuristics but limit the amount of parallelism that could otherwise enable significantly more scalable SAT solving. Inspired by neural network training, we formulate the SAT problem as a binarized matrix-matrix mult...
