2022 Fiscal Year Annual Research Report
Acceleration of SAT-based CSP Solvers using MDD
| Project/Area Number |
20K11748
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
宋 剛秀 神戸大学, DX・情報統括本部, 准教授 (00625121)
|
|---|
| Project Period (FY) |
2020-04-01 – 2023-03-31
|
| Keywords | SATソルバー / SAT符号化 / MDD / 制約充足問題 / 制約プログラミング |
|---|
| Outline of Annual Research Achievements |
近年， 命題論理式の充足可能性判定問題 (SAT問題) を解くプログラムであるSATソルバーの飛躍的な進歩にともない， 制約充足問題 (CSP) をSAT問題に符号化（SAT符号化）して解くSAT型CSPソルバーが成功している． 本研究の目的は， SAT型CSPソルバーの高速化であり, そのために MDD (Multi-valued Decision Diagram) を用いたCSPの正規化と， MDD が表す制約 (MDD制約) のSAT符号化を研究開発する． 本研究の意義は, SAT型CSPソルバーの新しい一方式を開拓できる点， 既存のCSPソルバーでは求解困難な問題に対して， より高性能な推論基盤を提供できる点である． CSPソルバーはスケジューリング問題, パッキング問題, 時間割問題, クラウド上のソフトウェア要素最適配置問題等に使われるなど実用性が高く， 研究成果の産業分野への応用も期待できる．
2022年度は研究計画に記載された「(B) MDD 制約の SAT 符号化の研究開発」の研究を進めると共に，「(C) 提案SAT型CSPソルバーの特長的なアプリケーションの研究開発」について調査と研究を行った．(B) については， 提案する方法を実装したSAT型CSPソルバー Fun-sCOP の研究開発を進めた． Fun-sCOP は国際CSPソルバー競技会XCSP3 Competition 2022 において準優勝という成績を収めた． また新しく線形制約に特化した新しいデータ構造とその簡約化条件を考案した． (C) については， システム生物学における定常状態をSATソルバーを用いて発見する方法を研究し， 国際会議で査読付き論文発表を行った．
|
| Remarks |
(1) は XCSP国際CSPソルバー競技会の web ページである． 研究代表者が開発した Fun-sCOP が2位に入賞していることが記載されている． (2) は国際会議で発表した査読付き論文の補足資料を掲載した web ページである．
|
Research Products
(6 results)
