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: ¥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符号化 / 制約最適化問題 / 制約プログラミング

Outline of Research at the Start

近年，SAT問題を解くプログラムであるSATソルバーの性能が飛躍的に向上している．
本研究の目的は， SATソルバーを用いた高速なSAT型COPソルバーを実現することである．
そのために2つの方法を研究する．1つは，目的関数を表す線形比較制約の MDD を用いた表現とその符号化方法である． もう1つの方法は極小モデル生成を用いた新しい最適化方法である．
COPソルバーはスケジューリング問題，パッキング問題，時間割問題， クラウド上のソフトウェア要素最適配置問題等の組合せ最適化問題に使われるなど実用性が高く， 高速なSAT型COPソルバーを実現できれば産業分野への応用も期待できる．