2022 Fiscal Year Final Research Report
Acceleration of SAT-based CSP Solvers using MDD
| Project/Area Number |
20K11748
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
Soh Takehide 神戸大学, DX・情報統括本部, 准教授 (00625121)
|
|---|
| Project Period (FY) |
2020-04-01 – 2023-03-31
|
| Keywords | SATソルバー / SAT符号化 / MDD / 制約充足問題 / 制約プログラミング / SAT (充足可能性判定問題) / CSP (制約充足問題) |
|---|
| Outline of Final Research Achievements |
Constraint Satisfaction Problem (CSP) is a problem of finding assignments that satisfy given constraints. CSP has various applications across academia and industry, and it is an important research topic in fields such as artificial intelligence. In this study, we conducted research and development on methods using the MDD representation of constraints and SAT encoding to realize a high-performance CSP solving system using a SAT solver (SAT-based CSP solver). As a result, we achieved success in terms of winning in international competitions and speeding up the system. Additionally, we applied SAT-based solving methods to compute the steady state (attractor) of automata networks, which are mathematical models of gene regulatory networks occurring within cells in systems biology. Furthermore, we proposed a SAT-based solving method for the Hamiltonian cycle problem.
|
| Free Research Field |
情報学基礎
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究成果の意義は，SAT符号化の新しい方向性を開拓した点，既存のCSPソルバーでは求解困難な問題に対して．より高性能な推論基盤の候補を提供した点である．またシステム生物学における定常状態の解析への応用を示したことも貢献として挙げられる．CSPソルバーは様々な分野に応用される実用性が高いシステムであり，研究成果の産業分野への応用も期待できると考えられる．
|
