2023 Fiscal Year Research-status Report
Speeding-up SAT-based Constraint Optimization Solvers
| Project/Area Number |
23K11047
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
宋 剛秀 神戸大学, DX・情報統括本部, 准教授 (00625121)
|
|---|
| Project Period (FY) |
2023-04-01 – 2027-03-31
|
| Keywords | SATソルバー / SAT符号化 / 制約最適化問題 / 制約充足問題 / 制約プログラミング |
|---|
| Outline of Annual Research Achievements |
近年, 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件論文発表した．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
4年の研究計画の初年度に，4つある研究課題のうち4つに着手し，2つについては初期成果の研究発表まで行うことができた．また1つについては国際ソルバー競技会XCSP3で準優勝 (CSP部門)という成績を収めた．このことから，研究は当初の計画以上に進展していると考えている．
|
| Strategy for Future Research Activity |
2024年度は，(B) について研究発表の準備を進め，(C) についてもCOPソルバーの開発を本格的に開始する予定である．
|
| Causes of Carryover |
より高性能な計算機クラスタを購入するために初年度に予定していた計算機の購入を二年目に変更したため．
|
