加速傅里葉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為偽布爾可滿足性求解提供了一個強大的新工具，尤其適用於需要處理複雜約束和大規模問題的場景。