加速傅里叶 SAT (AFSAT)：完全实现基于 GPU 的对称伪布尔 SAT 求解器

arXiv:2606.06641v1 公告类型：新 摘要：我们提出了 Accelerated Fourier SAT (AFSAT)，这是一种基于连续局部搜索 (CLS) 的伪布尔可满足性 GPU 加速求解器。 AFSAT 将概念验证方法 FastFourierSAT 实现为一个完全设计的求解器，支持单个问题实例中对称约束类型和长度的任何异构混合。使用 JAX 编译器，AFSAT 利用纯函数组合、自动向量化、自动微分和即时 (JIT) 编译来跨批次候选作业执行大规模并行 CLS。我们证明了与概念验证相比，数值稳定性、运行时性能和内存效率得到了显着提高。我们通过识别和解决内存延迟和浮点表示产生的各种限制以及利用自动并行化和紧凑表示来实现这一目标。浮点固有的表示性和稳定性限制可以通过定制的离散傅里叶变换实现部分解决。通过 JAX 数组分片扩展到多个加速器时，我们实现了近线性吞吐量。