加速フーリエSAT（AFSAT）：GPUベースの対称疑似ブールSATソルバーの完全実現
本論文では、連続局所探索（CLS）に基づくGPU加速疑似ブール充足可能性ソルバーAccelerated Fourier SAT (AFSAT)を紹介する。AFSATは概念実証アプローチFastFourierSATを完全にエンジニアリングされたソルバーへと発展させ、単一の問題インスタンス内で任意の異種対称制約タイプと長さの混合をサポートする。JAXコンパイラを利用し、純関数合成、自動ベクトル化、自動微分、ジャストインタイム（JIT）コンパイルにより、候補割り当てのバッチにわたって大規模並列CLSを実行する。概念実証と比較して、数値安定性、実行時性能、メモリ効率が大幅に向上したことを示す。これは、メモリレイテンシと浮動小数点表現から生じる様々な制限を特定し対処するとともに、自動並列化とコンパクト表現を活用することで達成される。浮動小数点の本質的な表現と安定性の制限は、カスタマイズされた離散フーリエ変換実装によって部分的に対処される。JAX配列シャーディングにより、複数のアクセラレータへのスケーリングでほぼ線形のスループットを達成する。
新しい論文「Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver」がarXivで公開されました。本論文は、連続局所探索（CLS）に基づくGPU加速疑似ブール充足可能性ソルバーであるAFSATを提案しています。AFSATは、以前の概念実証システムFastFourierSATを完全にエンジニアリングされたソルバーへと進化させ、単一の問題インスタンス内で任意の異種対称制約タイプと長さを混合して扱うことを可能にしました。
AFSATの核心はJAXコンパイラの活用にあります。JAXは純関数合成、自動ベクトル化、自動微分、そしてジャストインタイム（JIT）コンパイルを提供し、これにより候補割り当てのバッチに対して大規模かつ効率的な並列CLSを実行できます。このアプローチにより、AFSATは概念実証と比較して数値安定性、実行時性能、メモリ効率において顕著な改善を達成しました。改善は主に、メモリレイテンシと浮動小数点表現に起因する制限を特定し対処したこと、および自動並列化とコンパクト表現を活用したことに起因します。
特に、浮動小数点の表現と安定性の本質的な制限は、カスタマイズされた離散フーリエ変換実装を導入することで部分的に克服されました。さらに、AFSATはJAXの配列シャーディング機能を利用して、複数のアクセラレータにわたってほぼ線形のスループットスケーリングを実現しています。AFSATは、複雑な制約と大規模問題を扱うための強力なツールを提供します。