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
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2022: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2021: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2020: ¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
|
|---|
| Keywords | SATソルバー / SAT符号化 / MDD / 制約充足問題 / 制約プログラミング / SAT (充足可能性判定問題) / CSP (制約充足問題) |
|---|
| Outline of Research at the Start |
近年，SAT問題を解くプログラムであるSATソルバーの飛躍的な進歩にともない，制約充足問題 (CSP) をSAT問題に符号化（SAT符号化）して解くSAT型CSPソルバーが成功している．
本研究の目的は，SAT型CSPソルバーの高速化であり，そのためにMDD (Multi-valued Decision Diagram) を用いたCSPの正規化と，MDDが表す制約 (MDD制約) のSAT符号化を研究開発する．
本研究の意義は，SAT型CSPソルバーの新しい一方式を開拓できる点，既存の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.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究成果の意義は，SAT符号化の新しい方向性を開拓した点，既存のCSPソルバーでは求解困難な問題に対して．より高性能な推論基盤の候補を提供した点である．またシステム生物学における定常状態の解析への応用を示したことも貢献として挙げられる．CSPソルバーは様々な分野に応用される実用性が高いシステムであり，研究成果の産業分野への応用も期待できると考えられる．
|
Report
(4 results)
Research Products
(15 results)
