We present Accelerated Fourier SAT (AFSAT), a GPU-accelerated solver for pseudo-Boolean satisfiability based on continuous local search (CLS). AFSAT realises the proof-of-concept approach, FastFourierSAT, into a fully-engineered solver supporting any heterogeneous mixture of symmetric constraint types and lengths within a single problem instance. Using the JAX compiler, AFSAT leverages pure function composition, automatic vectorisation, automatic differentiation, and just-in-time (JIT) compilation to perform massively parallel CLS across batches of candidate assignments. We demonstrate substantially improved numerical stability, runtime performance, and memory efficiency over the proof-of-concept. We achieve this by way of identifying and addressing various limitations that arise from memory latency and floating-point representation, as well as leveraging automatic parallelisation and compact representations. The inherent representational and stability limitations of floating point are partially addressed by a tailored discrete Fourier transform implementation. We achieve near-linear throughput when scaling to multiple accelerators via JAX array sharding.

翻译：我们提出加速傅里叶SAT（AFSAT），一种基于连续局部搜索（CLS）的GPU加速伪布尔可满足性求解器。AFSAT将概念验证方法FastFourierSAT实现为完全工程化的求解器，支持同一问题实例中任意异构混合的对称约束类型与长度。利用JAX编译器，AFSAT通过纯函数组合、自动向量化、自动微分及即时编译（JIT）技术，跨候选赋值批次执行大规模并行CLS。相较于概念验证方法，我们展示了显著的数值稳定性、运行时性能及内存效率提升。这通过识别并解决内存延迟与浮点表示所引发的各类局限性，同时利用自动并行化与紧凑表示机制来实现。浮点数固有关表示与稳定性限制通过定制离散傅里叶变换实现得到部分缓解。借助JAX数组分片技术，我们在扩展至多加速器时实现了近线性吞吐量。