GaloisSAT：有限体代数による微分可能なブール充足可能性（SAT）解法

arXiv cs.AI / 2026/4/1

💬 オピニオンIdeas & Deep AnalysisTools & Practical UsageModels & Research

共有:

要点

本論文は、GPU上で動作する微分可能なSAT解法エンジンと、CPU上で実行される従来のCDCLベースの解法段階を組み合わせた、ハイブリッドGPU-CPU SATソルバGaloisSATを提示する。
それは、機械学習のための最新のインフラストラクチャを用いてSAT解法プロセスを微分可能にし、その上でアプローチの一部として有限体（ガロア体）代数を活用する。
SAT Competition 2024のベンチマークスイートにおいて、主要ソルバであるKissatおよびCaDiCaLと比較してベンチマークを行い、5,000秒のタイムアウト制限下で公式のPAR-2指標を改善した。
報告された向上として、最強のベースラインに対して充足可能（satisfiable）インスタンスで8.41×の高速化、不充足（unsatisfiable）インスタンスで1.29×の高速化が挙げられる。
著者らは、本研究を、SATソルバの性能向上が歴史的に遅かったこと—競技の初期の勝者と比べて複数十年にわたり改善が限定的であったこと—への対処として位置づけている。

要旨: ブール充足可能性（SAT）問題は、最初にNP困難であることが証明された問題であり、計算複雑性における基本的な課題となっています。最適化や検証をはじめ、多くの領域に幅広い応用があるためです。過去20年にわたって大きなアルゴリズム上の進展があったにもかかわらず、SATソルバの性能は限られたペースでしか改善してきません。特に、2025年の競技の勝者は、ほぼ20年に及ぶ努力の後のSAT Competitionの成績において、2006年の勝者に対して約2倍（2X）の改善にとどまっています。この論文では、GaloisSATという新しいハイブリッドGPU-CPU SATソルバを紹介します。GaloisSATは、GPU上の最新の機械学習インフラストラクチャによって駆動される差分可能なSAT解法エンジンを統合し、その後にCPU上で従来のCDCLベースのSAT解法段階を実行します。GaloisSATは、SAT Competition 2024のベンチマークスイートを用いて、最新の最先端ソルバであるKissatおよびCaDiCaLの最新版とベンチマーク比較を行います。その結果、公式のSAT Competition指標であるPAR-2（5,000秒のタイムアウトとペナルティ係数2を伴うペナルized平均実行時間）において、顕著な改善が示されます。具体的には、GaloisSATは、最も強力なベースラインと比べて、充足可能（satisfiable）カテゴリで8.41倍の高速化を達成し、充足不能（unsatisfiable）カテゴリでは1.29倍の高速化を達成します。