来自 arXiv 的新论文《Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver》于 2026 年 6 月 4 日提交，作者为 Cody J. Christopher 等。该研究将此前提出的概念验证方法 FastFourierSAT 推进为一个完整的工程化求解器 AFSAT，用于求解伪布尔可满足性问题，并充分利用 GPU 的并行计算能力。论文属于人工智能（cs.AI）与逻辑计算机科学（cs.LO）交叉领域。
AFSAT 的核心思路是基于连续局部搜索（CLS）来求解伪布尔 SAT 问题。与早期原型相比，AFSAT 的关键提升在于它不再局限于单一或同质的约束形式，而是能够在同一个问题实例中支持任意异构的对称约束类型和约束长度的混合。这意味着求解器可以处理更贴近实际应用的复杂约束组合，而无需将问题拆分成多个同构子问题分别求解。
在工程实现上，AFSAT 使用 JAX 编译器，充分发挥纯函数组合、自动向量化、自动微分和即时编译（JIT）等特性。这些特性使得 AFSAT 能够对多批候选赋值执行大规模并行的连续局部搜索。自动向量化让相同的计算逻辑可以同时作用于大量候选解，自动微分则为基于梯度的局部搜索提供便利，而 JIT 编译则减少了运行时的额外开销。
论文指出，AFSAT 在数值稳定性、运行时性能和内存效率方面均显著优于原型系统。研究团队识别并解决了由内存访问延迟和浮点数表示引起的一系列限制。例如，浮点运算在大规模并行计算中容易产生数值不稳定，为此 AFSAT 采用了一种定制的离散傅里叶变换实现，以部分缓解浮点表示和稳定性方面的固有限制。此外，通过利用自动并行化和紧凑的数据表示，求解器进一步提升了资源利用效率。
在多加速器扩展方面，AFSAT 借助 JAX 的数组分片（array sharding）机制，在扩展到多个加速器时实现了接近线性的吞吐量增长。这表明该求解器具备良好的横向扩展能力，能够适应更大规模的问题实例和更高吞吐量的求解需求。总体而言，AFSAT 将基于傅里叶变换的连续局部搜索方法从概念验证推进到了具备实用潜力的 GPU 加速伪布尔 SAT 求解器。