| 研究実績の概要 |
近年, SAT問題を解くプログラムであるSATソルバーの飛躍的な進歩にともない, 制約充足問題 (CSP) をSAT問題に符号化(SAT符号化)して解くSAT型CSPソルバーが成功している. 本研究では,対象を CSP から制約最適化問題 (COP) へ発展させる.
本研究の目的は, SATソルバーを用いた高速なSAT型COPソルバーを実現することである. そのために2つの方法を研究する.1つは,目的関数を表す線形比較制約の MDD (Multi‐valued Decision Diagram) を用いた表現とその符号化方法である.もう1つの方法は極小モデル生成を用いた新しい最適化方法である.
具体的な研究課題は4つある．(A) MDD を用いた線形比較制約の符号化の研究開発, (B) 極小モデル生成の研究開発, (C) 提案方法を用いたSAT型COPソルバーの実装, (D) 提案SAT型COPソルバーの特長的なアプリケーションの研究開発. それぞれの研究課題は密接に関係しているため逐次的に進めるのではなく同時並行的に取り組む計画である.2023年度は (A), (B), (C), (D) それぞれに取り組んだ．(A) については，MDDと似た圧縮データ構造である ZDD を用いた疑似ブール制約の符号化について研究を行い，発表した．(B) については，適用できる問題は限定されるものの符号化を用いた極小モデル生成方法を考案することができた．得られた成果を発表する準備を現在行っている．(C) については，また最新の制約への対応を実装したソルバーsCOPが国際ソルバー競技会XCSP3で準優勝 (CSP部門)という成績を収めた．(D) についてはシステム生物学および組合せ遷移問題の解法を研究し，国際会議で4件論文発表した．
|
