arXivに2026年6月4日付で投稿された論文「Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver」は、Cody J. Christopher氏らによる研究成果である。本論文は、以前に提案された概念実証であるFastFourierSATを、完全にエンジニアリングされた求解器AFSATへと昇華させるもので、擬似ブール充足可能性問題をGPUの並列計算能力によって解くことを目的としている。論文の主題は人工知能（cs.AI）と論理計算機科学（cs.LO）にまたがる。
AFSATの基本的なアプローチは、連続局所探索（CLS）に基づいて擬似ブールSAT問題を解くことにある。初期のプロトタイプとの決定的な違いは、単一または同質の制約形式に限定されず、同一の問題インスタンス内で任意の異種対称制約タイプと制約長の混合を扱える点である。これにより、求解器は現実の応用に近い複雑な制約の組み合わせを、同質な部分問題に分割することなく直接処理できる。
実装面では、AFSATはJAXコンパイラを活用し、純粋関数合成、自動ベクトル化、自動微分、ジャストインタイム（JIT）コンパイルといった機能を最大限に引き出している。これらの機能により、AFSATは多数の候補割り当てバッチに対して大規模並列の連続局所探索を実行できる。自動ベクトル化は同一の計算ロジックを多数の候補解に同時適用することを可能にし、自動微分は勾配に基づく局所探索を支援し、JITコンパイルは実行時のオーバーヘッドを削減する。
論文によれば、AFSATは数値安定性、実行時性能、メモリ効率のいずれにおいてもプロトタイプを大幅に上回る。研究チームは、メモリアクセス遅延と浮動小数点表現に起因する一連の制限を特定し、対処した。例えば、大規模並列計算では浮動小数点演算が数値的不安定性を招きやすいが、AFSATはカスタマイズされた離散フーリエ変換の実装を採用することで、浮動小数点表現と安定性に関する固有の制限を部分的に緩和している。さらに、自動並列化とコンパクトなデータ表現の活用により、リソース利用効率を一層高めている。
複数アクセラレータへの拡張では、AFSATはJAXの配列シャーディング機構を利用して、複数のアクセラレータにスケールする際にほぼ線形のスループット向上を実現している。これは、求解器が水平スケーリング能力を備え、より大規模な問題インスタンスや高いスループット要求に対応できることを示している。総じて、AFSATはフーリエ変換に基づく連続局所探索手法を概念実証から実用の可能性を備えたGPU加速擬似ブールSATソルバーへと押し進めた研究である。