Speeding-up SAT-based Constraint Optimization Solvers
| Project/Area Number |
23K11047
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
宋 剛秀 神戸大学, DX・情報統括本部, 准教授 (00625121)
|
|---|
| Project Period (FY) |
2023-04-01 – 2027-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2026: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2025: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2024: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2023: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
|
|---|
| Keywords | SATソルバー / SAT符号化 / 制約最適化問題 / 制約充足問題 / 制約プログラミング / SATソルバー |
|---|
| Outline of Research at the Start |
近年，SAT問題を解くプログラムであるSATソルバーの性能が飛躍的に向上している．
本研究の目的は， SATソルバーを用いた高速なSAT型COPソルバーを実現することである．
そのために2つの方法を研究する．1つは，目的関数を表す線形比較制約の MDD を用いた表現とその符号化方法である． もう1つの方法は極小モデル生成を用いた新しい最適化方法である．
COPソルバーはスケジューリング問題，パッキング問題，時間割問題， クラウド上のソフトウェア要素最適配置問題等の組合せ最適化問題に使われるなど実用性が高く， 高速なSAT型COPソルバーを実現できれば産業分野への応用も期待できる．
|
| 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ソルバーの開発を本格的に開始する予定である．
|
Report
(1 results)
Research Products
(14 results)
-
-
-
[Journal Article] ZDD-based algorithmic framework for solving shortest reconfiguration problems2023
Author(s)
Takehiro Ito, Jun Kawahara, Yu Nakahata, Takehide Soh, Akira Suzuki, Junichi Teruyama and Takahisa Toda
-
Journal Title
Proceedings of the 20th International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR 2023), Lecture Notes in Computer Science (LNCS)
Volume: 13884
Pages: 1-17
DOI
ISBN
9783031332708, 9783031332715
Related Report
Peer Reviewed / Open Access
-
-
[Journal Article] Hamiltonian Cycle Reconfiguration with Answer Set Programming2023
Author(s)
Hirate Takahiro、Banbara Mutsunori、Inoue Katsumi、Lu Xiao-Nan、Nabeshima Hidetomo、Schaub Torsten、Soh Takehide、Tamura Naoyuki
-
Journal Title
Proceedings of the 18th European Conference on Logics in Artificial Intelligence (JELIA 2023)
Volume: LNAI 14281
Pages: 262-277
DOI
ISBN
9783031436185, 9783031436192
Related Report
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
-
-
-
-
-
