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