| 研究実績の概要 |
充足可能性問題(Satisfiability problem, SAT問題)とは、真偽の二値をとるBoolean変数から構成される論理式に対して、式を真にする変数割り当てが存在するか証明する問題である。SAT問題の解を探索するプログラムはSATソルバと呼ばれ、ソフトウェアの検証や定理証明など多くの実世界の問題を解く際に使用されており、活発に研究開発が進められている。本研究では、機械学習の予測を用いてSATソルバの性能向上を目指す。具体的には、学習の対象となる入力にグラフ構造を直接取り入れることが可能なグラフニューラルネットワーク(GNN)を用いて、SAT問題における探索に影響を与える変数や節の予測を行う。SAT問題はグラフとして表現することで、その構造をより捉えやすいことが知られており、グラフの構造を本質的に組み込み可能なGNNと親和性が高いと考えられる。本年度は、SAT問題における充足不可能な問題のunsatisfiable coreに該当する節を予測するようなGNNを構築し、その予測を元にincrementalに問題を解く手法の提案を行った。実験の結果、一部の問題群に対してSATソルバの高速化に成功した。
|
