| 研究実績の概要 |
近年，SAT問題を解くプログラムであるSATソルバーの飛躍的な進歩にともない，制約充足問題 (CSP) をSAT問題に符号化（SAT符号化）して解くSAT型CSPソルバーが成功している．本研究の目的は，SAT型CSPソルバーの高速化であり, そのために MDD (Multi-valued Decision Diagram) を用いたCSPの正規化と，MDD が表す制約 (MDD制約) のSAT符号化を研究開発する．本研究の意義は, SAT型CSPソルバーの新しい一方式を開拓できる点，既存のCSPソルバーでは求解困難な問題に対して，より高性能な推論基盤を提供できる点である．CSPソルバーはスケジューリング問題, パッキング問題, 時間割問題,クラウド上のソフトウェア要素最適配置問題等に使われるなど実用性が高く，研究成果の産業分野への応用も期待できる．
2020年度は研究計画に記載された「(A) MDD 制約を用いた内包的制約，外延的制約, グローバル制約の正規化の研究」の研究環境を整えて研究を進めると共に，「(C) 提案SAT型CSPソルバーの特長的なアプリケーションの研究開発」について調査と研究を行った． (A) については， 正規化方法を実装するSAT型CSPソルバー sCOP の研究開発を進めた． (C) については，一層平面配置配線問題への応用を研究し， 国内の研究会で発表を行った．
|
