Development of SAT Solvers by Graph Neural Networks

2023 Fiscal Year Final Research Report

• Project/Area Number: 21K12023
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 61030:Intelligent informatics-related
• Research Institution: National Institute of Informatics
• Principal Investigator: Sonobe Tomohiro 国立情報学研究所, ビッグデータ数理国際研究センター, 特任研究員 (50747269)
• Project Period (FY): 2021-04-01 – 2024-03-31
• Keywords: SATソルバ / 探索

Outline of Final Research Achievements

The satisfiability problem (SAT problem) is known as an important problem in computer science. To solve SAT problems, the SAT solvers are developed and used to tackle real-world problems. The research aims to enhance SAT solvers by leveraging Graph Neural Networks (GNNs), which are suitable for the graph structure of SAT instances. The proposed method shows good performance on specific families of SAT problems.

Free Research Field

SATソルバ

Academic Significance and Societal Importance of the Research Achievements

充足可能性問題は回路検証、プログラムのバグの発見、ニューラルネットワークの検証、数学の定理証明などの、様々な現実世界の問題に変換可能であり、それらの問題をSATソルバで解くことで実用的な時間で解の発見が可能であることが知られており、高速化が活発に行われている。本研究では、グラフニューラルネットワークを用いて、特定の問題に対してSATソルバの高速化を実現した。