ブール充足可能性問題（SAT問題）は、チップ検証からサイバーセキュリティ、形式証明チェックに至るまで、幅広いコンピューティングタスクの基盤となっている。この問題を解くアルゴリズムは数十年にわたり人間の専門家によって改良され、変数選択、節削減、再起動タイミングに関する巧妙なヒューリスティックを通じて性能を段階的に向上させてきた。
7月17日に『ネイチャー・コミュニケーションズ』に掲載された研究によると、大規模言語モデル（LLM）は現在、人間が設計したものを上回るSATソルバーのヒューリスティックを生成できることが示された。ベースラインソルバーと比較して実行時間が40％改善され、11のベンチマークデータセットのうち8つで、最先端システムの最適なパラメータ調整版を上回った。
研究の内容
復旦大学のKe Wei氏と中国科学院のShaowei Cai氏が率いる研究チームは、AutoModSATと呼ばれるフレームワークを構築した。重要な洞察は、SATソルバーのコードベースが膨大で複雑であることだった。人気のKissatソルバーは25万トークンに達する。LLMにそのようなコードベースを直接修正するよう求めるのは不可能だ。代わりに研究者らは、CDCL（Conflict-Driven Clause Learning）ソルバーをモジュール化し、再起動タイミング、節削減、変数アクティビティバンピングなど、正確に7つのヒューリスティック関数をクリーンな探索空間として公開した。
ソルバーがモジュール化されると、システムは3つのLLMエージェントを循環させる。Coderが新しいC++ヒューリスティックコードを生成し、Evaluatorが既存のヒューリスティックと意味的に同一のコードをフィルタリングし、Repairerがコンパイルエラーを修正する。最も性能の高いヒューリスティックは進化的ループで保持される。プロセス全体では問題領域あたり50回のLLM呼び出しを使用し、低コストで競争力のある性能が評価されてDeepSeek-V3が採用されている。
研究結果
SATコンペティション問題、EDA（電子設計自動化）検証、組合せパズルにわたる11のベンチマークデータセットにおいて、AutoModSATは最適化されたヒューリスティックを生成し、ベースラインモジュラーソルバーと比較してPAR-2スコア（未解決インスタンスにペナルティを課す標準的な評価指標）で平均40％の改善を達成した。
最先端ソルバーであるKissatとCaDiCaLのパラメータ調整版と比較して、AutoModSATは11のデータセットのうち8つで勝利し、約20％の平均高速化を達成した。レジスタ割り当て問題では、LLMが発見したヒューリスティックが20インスタンス中18を解決したのに対し、ベースラインは6未満だった。ハッシュテーブル安全性検証問題では、1170万変数と5360万節を持つ問題で、AutoModSATがPAR-2スコア3,302を記録し、最良の競合の7,322を上回った。
また、LLMはこれまで文献で説明されていなかったヒューリスティックも発明した。再起動戦略については、節の品質スコアの移動平均を用いた動的手法を生成し、既存のどのソルバーにもない新しいアプローチを実現した。
重要性
これは既存のパラメータを調整する自動ハイパーパラメータチューニングとは質的に異なる。AutoModSATは新しいアルゴリズムコード、つまり人間の専門家が考えつかなかったヒューリスティックを生成する。最適化実行あたりの総コストはAPI料金で数ドルであり、実際の産業展開に実用的である。
モジュール化アプローチ自体がこの論文の最も強い主張である。ソルバーコードをLLMフレンドリーにすることはオプションではなく、基礎的な条件だ。このアプローチは、混合整数計画法、制約充足問題、定理証明など、他の複雑なソルバーにも拡張できる可能性がある。
注意点
ベースラインソルバー（ModSAT）は、数十年の最適化を経たKissatのような最先端システムよりも単純である。一部の改善はベースラインの相対的な弱さを反映している。フレームワークは7つのヒューリスティック関数のみを公開し、一部のデータセットで重要なトップレベルの前処理パラメータには触れられない。Zamkellerデータセットでは、パラメータ調整されたKissatがAutoModSATを4倍上回った。その差はシステムが修正できないコンポーネントにあったためである。
本論文は『ネイチャー・コミュニケーションズ』（DOI: 10.1038/s41467-026-74949-2）に掲載され、著者はY. Sun、F. Ye、Z. Chen、K. Wei、S. Caiである。
出典
1. Y. Sun, F. Ye, Z. Chen, K. Wei, S. Cai、「Discovering Heuristics in a Complex SAT Solver with Large Language Models」、『ネイチャー・コミュニケーションズ』（2026年）。DOI: 10.1038/s41467-026-74949-2
雅子 訳