用GPU加速布尔可满足性求解，支持多种约束混合问题
Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver
- 基于连续局部搜索，在GPU上实现并行求解
- 相比原型系统，速度更快、内存更省、数值更稳定
- 适合需要高效处理复杂布尔约束的科研与工业场景
我们提出Accelerated Fourier SAT (AFSAT)，一种基于连续局部搜索（CLS）的GPU加速伪布尔可满足性求解器。AFSAT将快速傅里叶SAT（FastFourierSAT）的原型方案转化为可工程化部署的求解器，支持单一实例中任意混合的对称约束类型与长度。通过JAX编译器，AFSAT利用纯函数组合、自动向量化、自动微分和即时编译，在候选赋值批量上实现大规模并行CLS。我们显著提升了数值稳定性、运行效率与内存使用效率，主要通过识别并解决内存延迟、浮点表示等带来的瓶颈，并利用自动并行化与紧凑表示。针对浮点数固有的表示与稳定性限制，采用定制化的离散傅里叶变换实现予以缓解。在多加速器扩展时，借助JAX数组分片实现近线性吞吐量。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。