2018 Fiscal Year Annual Research Report
High Performance SAT-based Constraint Programming System using Hybrid Encoding
| Project/Area Number |
16K16036
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
宋 剛秀 神戸大学, 情報基盤センター, 助教 (00625121)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | SATソルバー / SAT符号化 / 順序符号化 / 対数符号化 / ハイブリッド符号化 / 制約充足問題 / 制約プログラミング |
|---|
| Outline of Annual Research Achievements |
近年，SAT問題を解くプログラムであるSATソルバーの飛躍的な進歩にともない，CSPをSAT問題に符号化（SAT符号化）して解くSAT型の制約プログラミング（CP）システムが成功している．本研究の目的は，複数のSAT符号化を変数レベルで融合可能なハイブリッドSAT符号化を実現し，それを実装した高性能なSAT型CPシステムを研究開発することである．本研究の意義は，SAT符号化の新しい方向性を開拓できる点，既存のCPシステムでは求解困難な問題に対して．より高性能な推論基盤を提供できる点である．CPシステムはサッカーのJリーグの対戦スケジュール開発に使われるなど実用性が非常に高く，研究成果の産業分野への応用も期待できる．
平成30年度は研究計画に記載された提案方法を基に実装を行なったSAT型制約プログラミングシステムである sCOP の研究開発を継続して行なった. また sCOP の有効性の評価を行うために sCOP を制約プログラミングシステム (CSPソルバー) の国際的な競技会である 2018 XCSP3 Competition に参加登録した. 具体的には, sCOP はこの競技会のスタンダードソルバーCSP部門（逐次・並列）の2部門に登録した．結果として登録した両方の部門で優勝した. XCSP3 Competition は, 2005年にその前身が始まった歴史のある競技会であり, 欧米各国の教育研究機関で研究開発されたシステムが毎年参加している.
|
