| 研究実績の概要 |
近年， 命題論理式の充足可能性判定問題 (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ソルバーを用いて発見する方法を研究し， 国際会議で査読付き論文発表を行った．
|
