2016 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リーグの対戦スケジュール開発に使われるなど実用性が非常に高く，研究成果の産業分野への応用も期待できる．
平成28年度は研究計画に記載された「(A) ハイブリッド符号化の理論的枠組の完成」と「(B-1) 既存符号化の網羅的評価の開始」に取り組んだ．
(A) については，変数毎に異なる任意の符号化をハイブリッドする方法を研究し，理論的枠組みを完成した．成果の一部を国際論文誌 "International Journal on Artificial Intelligence Tools" で発表した．また (B-1) については，評価のためのサーバーシステムを構築し，CPシステムの国際競技会のベンチマークを用いた評価を開始した．またこれまでの研究成果も含んだ内容で「SATソルバーの最新動向と利用技術」と題した研究発表を「日本ソフトウェア科学会・第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)」で行い，``PPL2017発表賞（一般の部）''を受賞した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画通り，平成28年度は研究計画に記載された「(A) ハイブリッド符号化の理論的枠組の完成」と「(B-1) 既存符号化の網羅的評価の開始」を行い成果を得た．また上記課題に関する国際論文誌への成果発表や国内研究発表を行った．これより本研究課題は概ね順調に進展している．
|
| Strategy for Future Research Activity |
平成28年度について計画していた研究内容は，順調に進めることができた．今後は，「(B-1) 既存符号化の網羅的評価の開始」の結果を確認しながら，「(B-2) ハイブリッド符号化の自動構成の研究の開始」「(C) アプリケーション研究の開始」を行う．
|
| Remarks |
申請者の実績・業績は次の2つのページにまとめられている ：http://kix.istc.kobe-u.ac.jp/~soh/jp/，http://kix.istc.kobe-u.ac.jp/~soh/jp/publications.html
SAT型制約ソルバー「Diet-Sugar」は次のページで公開されている：http://kix.istc.kobe-u.ac.jp/~soh/dsugar/
|
Research Products
(20 results)
