2017 Fiscal Year Research-status Report
ハイブリッド符号化を用いた高性能なSAT型制約プログラミングシステム
| 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リーグの対戦スケジュール開発に使われるなど実用性が非常に高く，研究成果の産業分野への応用も期待できる．
平成29年度は研究計画に記載された「(B-2) 解析結果を用いたハイブリッド符号化の自動構成」と「(C) 提案 SAT 型 CP システムの特長的なアプリケーションの研究と開発」に取り組んだ．(B-2) については，自動構成を実装したSAT型制約プログラミングシステムである scop の開発を開始した．(C) については，多目的制約最適化問題に対してハイブリッド符号化を適用する研究に取り組んだ．多目的制約最適化問題では，目的変数を順序符号化し，それ以外の変数を対数符号化するようにハイブリッド符号化を構成した．計算機実験の結果，提案方法を実装したシステムが既存方法を実装したシステムと競争的な結果を示すことが分かった．この研究成果は国際会議 CP2017 で発表した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画通り，平成29年度は研究計画に記載された「(B-2) 解析結果を用いたハイブリッド符号化の自動構成」と「(C) 提案 SAT 型 CP システムの特長的なアプリケーションの研究と開発」を行い成果を得た．また上記課題に関する国際論文誌，国際学会への成果発表を行った．これより本研究課題は概ね順調に進展している．
|
| Strategy for Future Research Activity |
平成29年度について計画していた研究内容は，順調に進めることができた．最終年度も計画通り「(B-2) ハイブリッド符号化の自動構成の研究」と「(C) アプリケーション研究」を行う．
|
