| 研究課題/領域番号 |
16K16036
|
|---|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
宋 剛秀 神戸大学, 情報基盤センター, 助教 (00625121)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| キーワード | SATソルバー / SAT符号化 / 順序符号化 / 対数符号化 / ハイブリッド符号化 / 制約充足問題 / 制約プログラミング |
|---|
| 研究実績の概要 |
近年，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発表賞（一般の部）''を受賞した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初の計画通り，平成28年度は研究計画に記載された「(A) ハイブリッド符号化の理論的枠組の完成」と「(B-1) 既存符号化の網羅的評価の開始」を行い成果を得た．また上記課題に関する国際論文誌への成果発表や国内研究発表を行った．これより本研究課題は概ね順調に進展している．
|
| 今後の研究の推進方策 |
平成28年度について計画していた研究内容は，順調に進めることができた．今後は，「(B-1) 既存符号化の網羅的評価の開始」の結果を確認しながら，「(B-2) ハイブリッド符号化の自動構成の研究の開始」「(C) アプリケーション研究の開始」を行う．
|
| 備考 |
申請者の実績・業績は次の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/
|
