2021 Fiscal Year Research-status Report
Acceleration of SAT-based CSP Solvers using MDD
| Project/Area Number |
20K11748
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
宋 剛秀 神戸大学, 情報基盤センター, 准教授 (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ソルバーはスケジューリング問題, パッキング問題, 時間割問題, クラウド上のソフトウェア要素最適配置問題等に使われるなど実用性が高く， 研究成果の産業分野への応用も期待できる．
2021年度は研究計画に記載された「(B) MDD 制約の SAT 符号化の研究開発」の研究を進めると共に，「(C) 提案SAT型CSPソルバーの特長的なアプリケーションの研究開発」について調査と研究を行った． (C) については， CEGAR (Counterexample-guided Abstraction Refinement) の並列化とSATソルバーを用いたハミルトン閉路問題への応用を研究し， 査読付き国際ワークショップで発表を行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画通り，2021年度は「(B) MDD 制約の SAT 符号化の研究開発」の研究を進めた． また当初の計画とは異なるが， 「(C) 提案SAT型CSPソルバーの特長的なアプリケーションの研究開発」について先行して，調査研究を行った． これらより本研究課題は概ね順調に進展していると考えている．
|
| Strategy for Future Research Activity |
2020年度および2021年度に先行して「(C) 提案SAT型CSPソルバーの特長的なアプリケーションの研究開発」に研究を開始した． 2022年度は「(A) MDD 制約を用いた内包的制約，外延的制約, グローバル制約の正規化の研究」および「(B) MDD 制約のSAT符号化の研究」の研究も併せて進める予定である．
|
