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

[4F3-OS-8b-03] GNN-MatSat: A Differentiable SAT Solver Based on Initialization by Graph Neural Networks

〇Koji Watanabe^1,2, Taisuke Sato², Ryosuke Kojima³, Mitsuhiro Odaka^1,2, Katsumi Inoue^1,2 (1. The Graduate University for Advanced Studies, SOKENDAI, 2. National Institute of Informatics, 3. Graduate School of Medicine, Kyoto University)

Keywords:AI, SAT, Graph Neural Networks

In this work, we aim to establish a novel technique for SAT solving by combining deep learning and optimization methods. In general, deep learning models can be trained by optimizing a differentiable cost function. Considering the properties of deep learning models, we can build a deep learning model for SAT solving using back-propagation once the cost function is given for SAT solving. Therefore, we define a differentiable cost function for SAT solving and minimize the cost function by updating the assignment in a continuous vector space using Newton's method. Since Newton's method converges quadratically to a solution when an initial assignment is close to a solution, we use the prediction of deep learning as an initial assignment. The proposed technique is denoted as GNN-MatSat, which solves SAT instances by minimizing a differentiable cost function using Newton's method starting from the prediction of GNN. We conducted experiments to evaluate the performance of GNN-MatSat on the random track benchmarks of SAT Competition 2017 and 2018. The experimental results show that GNN-MatSat successfully found a solution for all benchmarks. We also compared GNN-MatSat with MatSat and observed that GNN-MatSat found a solution faster with fewer iterations than MatSat by starting the search from the predicted assignment close to a solution.