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
|
Project Status |
Completed (Fiscal Year 2023)
|
Budget Amount *help |
¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
Fiscal Year 2023: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000)
Fiscal Year 2022: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2021: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
|
Keywords | SATソルバ / 探索 / 充足可能性問題 / SAT / グラフニューラルネットワーク |
Outline of Research at the Start |
充足可能性問題(SAT問題)は計算機科学において重要な問題として知られていて、その問題を解くためのツールであるSATソルバはこの20年でその性能が大きく向上し、ハードウェアの検証や暗号解析など、実世界の多くの問題を解く際に使われている。本研究では、深層学習の一種であるグラフニューラルネットワークを用いて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.
|
Academic Significance and Societal Importance of the Research Achievements |
充足可能性問題は回路検証、プログラムのバグの発見、ニューラルネットワークの検証、数学の定理証明などの、様々な現実世界の問題に変換可能であり、それらの問題をSATソルバで解くことで実用的な時間で解の発見が可能であることが知られており、高速化が活発に行われている。本研究では、グラフニューラルネットワークを用いて、特定の問題に対してSATソルバの高速化を実現した。
|