[4F3-OS-8b] AIと制約プログラミング(2/2)

[4F3-OS-8b-03] GNN-MatSat: グラフニューラルネットワークによる初期化に基づく微分可能なSATソルバー

〇渡邉 晃司^1,2、佐藤 泰介²、小島 諒介³、小高 充弘^1,2、井上 克巳^1,2 (1. 総合研究大学院大学、2. 国立情報学研究所、3. 京都大学大学院医学研究科)

キーワード：人工知能、充足可能性問題、グラフニューラルネットワーク

本研究では, 深層学習と最適化手法を組み合わせることで, SATの解法に新しい手法を確立することを目指す. 一般に, 深層学習モデルは, 微分可能なコスト関数を最適化することで学習させることができる. 深層学習モデルの特性を考慮すると, SAT問題に対するコスト関数が与えられれば, SAT問題を解くモデルを 誤差逆伝播法により学習させることが可能である. そこで, SAT問題に対する微分可能なコスト関数を定義し, ニュートン法によりこのコスト関数を最小化することで解を探索する. ニュートン法は初期値が解に近い場合, 解に2次収束するので, 深層学習の予測値を初期値として使用する. この手法をGNN-MatSatとして実装し, SAT Competition 2017および2018 Random Trackベンチマークで性能を評価する実験を行った. 評価実験の結果, GNN-MatSatはGNNの予測値から探索を開始することで, 従来のMatSatよりもニュートン法による更新回数を大きく削減するとともに, 求解時間を削減することを確認した.