加速傅里叶SAT（AFSAT）：完全实现基于GPU的对称伪布尔SAT求解器
本文介绍加速傅里叶SAT（AFSAT），一种基于连续局部搜索（CLS）的GPU加速伪布尔可满足性求解器。AFSAT将概念验证方法FastFourierSAT发展为完全工程化的求解器，支持任意异构对称约束类型和长度的混合。利用JAX编译器，通过纯函数组合、自动向量化、自动微分和即时编译实现大规模并行CLS。与概念验证相比，AFSAT在数值稳定性、运行时性能和内存效率上显著提升，通过解决内存延迟和浮点表示限制，以及利用自动并行化和紧凑表示实现。定制的离散傅里叶变换部分解决了浮点限制，通过JAX数组分片实现多加速器近线性扩展。
加速傅里叶SAT（AFSAT）是一篇发表于arXiv的新论文，提出了一种基于GPU的加速求解器，专门用于伪布尔可满足性问题。这一求解器采用连续局部搜索方法，将之前的概念验证系统FastFourierSAT转化为一个完整的工程化实现。其核心创新在于利用了JAX编译器——一个用于高性能数值计算的框架——通过纯函数组合、自动向量化、自动微分以及即时编译技术，在大规模候选赋值批次上实现了高度并行的局部搜索。
AFSAT在多个方面超越了其前身。首先，它支持同一问题实例中任意异构对称约束类型和长度的混合，这极大地扩展了应用范围。其次，通过识别并解决内存延迟和浮点表示带来的限制，AFSAT在数值稳定性、运行时性能和内存效率上取得了显著改进。例如，论文中采用了一种定制的离散傅里叶变换实现，部分克服了浮点数在表示和稳定性上的固有限制。此外，借助JAX的自动并行化和紧凑表示能力，AFSAT能够高效地利用现代GPU的计算资源。
在扩展性方面，AFSAT通过JAX数组分片技术实现了接近线性的吞吐量增长，这意味着当使用多个加速器时，性能几乎可以线性提升。整体来看，AFSAT为伪布尔可满足性求解提供了一个强大的新工具，尤其适用于需要处理复杂约束和大规模问题的场景。