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

2021 Fiscal Year Research-status Report

• Project/Area Number: 21K12023
• Research Institution: National Institute of Informatics
• Principal Investigator: 薗部 知大 国立情報学研究所, ビッグデータ数理国際研究センター, 特任研究員 (50747269)
• Project Period (FY): 2021-04-01 – 2024-03-31
• Keywords: 充足可能性問題 / SATソルバ / グラフニューラルネットワーク

Outline of Annual Research Achievements

充足可能性問題(Satisfiability problem、SAT問題)とは、真偽の二値のどちらかを取るBoolean変数から構成される論理式に対して、その論理式を真にするような変数割り当てが存在するかどうか証明する問題である。この問題を解くツールとしてSATソルバがあり、実世界の多くの問題を解く際に使われているため高速化の意義は高い。本研究では、機械学習の予測を用いて、SATソルバに組み込まれている多くのヒューリスティックの性能向上を目指す。具体的には、機械学習手法の中で近年発展の著しいグラフニューラルネットワーク(GNN)を用いて、SATソルバの探索挙動の改善を目指す。GNNでは、ニューラルネットワークにおけるネットワークの構造自体を入力として与えることができ、入力データの構造をより捉えやすいと考えられている。加えて、現実世界の問題から派生するSAT問題は、グラフとして表現するとその構造が捉えやすくなることが知られているため、グラフ構造を直接入力として与えることが可能なGNNとの親和性が高く、その出力をSATソルバの探索に活用することで、問題の構造をより正確に把握でき、性能の向上が期待できる。
本年度はGNNの最新技術の調査と、一部のGNNの実装を行い、SATソルバの出力を実際に学習させてどれくらいの精度を達成できるかの確認を行った。それを元に、SATソルバのどの処理の高速化に適用させるかの検討を行った。

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

SATソルバの出力するデータを用いて、それをグラフニューラルネットワークに入力し、例えばどの変数がどれくらい重要なのかを解析したが、それらの結果を用いて実際にSATソルバの性能を向上させるところまで到達できなかったため。

Strategy for Future Research Activity

引き続きグラフニューラルネットワークの最新技術の調査を進め、それらの実装を行いつつ、SATソルバのデータの分析をグラフニューラルネットワーク用いて進める。分析対象のデータの種類を増やしつつ、SATソルバの高速化だけに着目するのではなく、SATソルバの挙動の解析も行う予定である。

Causes of Carryover

学会への参加が無かったことと、実験に使用するPCの購入を控えたため。次年度は学会への参加とPCの購入を行う予定である。