基于 GPU 的用于混合 SAT 求解的大规模并行连续局部搜索
人工智能
2023-08-30 v1 分布式、并行与集群计算
信息论
机器学习
计算机科学中的逻辑
math.IT
摘要
尽管基于冲突驱动子句学习（CDCL）的最先进（SOTA）SAT 求解器取得了显著的工程成功，但其顺序性质限制了可在图形处理单元（GPU）等平台上提取用于加速的并行性。在这项工作中，我们提出 FastFourierSAT，一种基于梯度驱动的连续局部搜索（CLS）的高度并行混合 SAT 求解器。这是通过一种受基于快速傅里叶变换（FFT）的卷积启发的新型并行算法实现的，用于计算初等对称多项式（ESP），这是先前 CLS 方法中的主要计算任务。我们算法的复杂度与先前最佳结果相匹配。此外，我们算法固有的大量并行性可利用 GPU 进行加速，相比先前的 CLS 方法表现出显著改进。我们还提出将重启启发式纳入 CLS 以提高搜索效率。我们在多个基准上将我们的方法与 SOTA 并行 SAT 求解器进行比较。我们的结果表明，FastFourierSAT 计算梯度的速度比先前在 CPU 上实现的原型快 100 倍以上。此外，FastFourierSAT 解决了大多数实例，并在更大规模实例上展现出有前景的性能。
引用
@article{arxiv.2308.15020,
title = {Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs},
author = {Yunuo Cen and Zhiwei Zhang and Xuanyao Fong},
journal= {arXiv preprint arXiv:2308.15020},
year = {2023}
}