グラフニューラルネットワークを用いた高速SATソルバの研究開発

充足可能性問題(Satisfiability problem, SAT問題)とは、真偽の二値をとるBoolean変数から構成される論理式に対して、式を真にする変数割り当てが存在するか証明する問題である。SATソルバはSAT問題の解を探索するプログラムであり、多くの実世界の問題を解く際に使用されており、高速化の意義は高い。本研究では、機械学習の予測を用いて、SATソルバに組み込まれているヒューリスティックの性能向上を目指す。具体的には、学習の対象となる入力にグラフ構造を直接取り入れることが可能なグラフニューラルネットワーク(GNN)を用いて、SATソルバの探索挙動の解析と改善を行う。SAT問題はグラフとして表現することで、その構造をより捉えやすいことが知られており、グラフの構造を本質的に組み込み可能なGNNと親和性が高いと考えられる。本年度はGNNの最新技術の調査と、一部のGNNの実装を行いSATソルバの出力を実際に学習させ、SATソルバの挙動の解析を行った。また、頂点被覆問題や巡回セールスマン問題等のグラフ理論の問題に対する、GNNを用いた解の探索に関する論文を調査し、それらのSAT問題への応用の検討も行った。

充足可能性問題(Satisfiability problem, SAT問題)とは、真偽の二値をとるBoolean変数から構成される論理式に対して、式を真にする変数割り当てが存在するか証明する問題である。SATソルバはSAT問題の解を探索するプログラムであり、多くの実世界の問題を解く際に使用されており、高速化の意義は高い。本研究では、機械学習の予測を用いて、SATソルバに組み込まれているヒューリスティックの性能向上を目指す。具体的には、学習の対象となる入力にグラフ構造を直接取り入れることが可能なグラフニューラルネットワーク(GNN)を用いて、SATソルバの探索挙動の解析と改善を行う。SAT問題はグラフとして表現することで、その構造をより捉えやすいことが知られており、グラフの構造を本質的に組み込み可能なGNNと親和性が高いと考えられる。本年度はGNNの最新技術の調査と、一部のGNNの実装を行いSATソルバの出力を実際に学習させ、SATソルバの挙動の解析を行った。また、頂点被覆問題や巡回セールスマン問題等のグラフ理論の問題に対する、GNNを用いた解の探索に関する論文を調査し、それらのSAT問題への応用の検討も行った。