AFSAT: High-Performance GPU-Accelerated Pseudo-Boolean SAT Solver

•AFSAT 是一款功能完備的求解器，將概念驗證方法 FastFourierSAT 轉化為一個支援單一問題實例中任意異質對稱約束類型和長度組合的完整工程化求解器。
•該求解器基於連續局部搜尋 (CLS)，透過 Walsh-Fourier 變換將布林變數鬆弛為實值變數，將 SAT 問題重新表述為一個適用於梯度最佳化方法的有界連續最佳化問題。
•AFSAT 相較於其概念驗證模型，在數值穩定性、執行時間效能和記憶體效率方面展現出顯著提升。
•未來的開發方向將包括自適應約束加權、透過分解框架與系統求解器整合，以及利用新興的高精度加速器算術。
•AFSAT 識別了精度驅動的約束長度限制和快取驅動的吞吐量特性，為實際部署提供了可操作的指導。

AFSAT 基於連續局部搜尋 (CLS)，透過 Walsh-Fourier 展開將布林問題變數鬆弛為實值變數，將 SAT 問題重新表述為一個適用於梯度最佳化方法的有界連續最佳化問題。
求解器採用投影梯度下降 (PGD) 作為基準搜尋演算法，並透過 JAX 在 GPU warp 中實現對候選賦值批次的向量映射，每個候選賦值都有專用記憶體和串流處理器，演算法同步執行。
JAX 編譯器被用於純函數組合、自動向量化、自動微分和即時 (JIT) 編譯，以實現大規模平行 CLS。
為了緩解浮點數表示和穩定性的固有局限性，AFSAT 實作了客製化的離散傅立葉變換。
透過 JAX 陣列分片技術（例如使用 jax.shard_map 和 PartitionSpec），AFSAT 在多個加速器上實現了近乎線性的吞吐量擴展，這對於跨裝置網格分佈計算至關重要。
透過識別和解決記憶體延遲和浮點數表示的各種限制，並利用自動平行化和緊湊表示，AFSAT 提高了記憶體效率。

AFSAT 可能會顯著加速加速器豐富環境中的組合最佳化。

其可擴展的多 GPU 執行和超越基準的改進效能，為此類環境中實用的 GPU 加速 SAT 求解奠定了基礎。

AFSAT 的方法論可能會啟發新的混合求解器設計。

透過將連續局部搜尋與 JAX 的平行化能力相結合，它提供了一種新穎的方法，可以與傳統的系統求解器整合或互補。

AFSAT 在處理異質約束方面的進步將擴大偽布林求解器的適用性。

在單一問題實例中支援任意混合的約束類型，可以更自然地建模複雜的現實世界問題。

2005

偽布林約束轉換為 SAT 及現代偽布林 SAT 求解器 Pueblo 的早期研究發表。

2010

關於在圖形處理器上實現布林可滿足性 (SAT) 的早期工作發表，展示了 GPU 加速 SAT 的潛力。

2020-11

一篇關於使用 GPU 加速連續時間類比 SAT 求解器的論文發表，展示了顯著的效能提升。

2021-12

ParaFROST 推出，這是第一個支援 GPU 加速內部處理的 SAT 求解器。

2025

AFSAT 的前身 FastFourierSAT 被提及實現了大規模平行 GPU 計算。

2026-06-04

AFSAT 論文《Accelerated Fourier SAT: Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver》在 arXiv 上發表。

AFSAT：高效能 GPU 加速偽布林 SAT 求解器