| 研究課題/領域番号 |
25330262
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
藤田 博 九州大学, システム情報科学研究科(研究院, 准教授 (70284552)
|
|---|
| 研究分担者 |
長谷川 隆三 九州大学, システム情報科学研究科(研究院, 教授 (20274483)
越村 三幸 九州大学, システム情報科学研究科(研究院, 助教 (30274492)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | 組合せ問題 / ラムゼー数 / 基数制約 / 最適化問題 / MaxSAT / SATソルバー / 帰納論理プログラミング |
|---|
| 研究実績の概要 |
対称性制約(テーマ項目A.2)に関して：今年度も、大規模組合せ問題として格好の題材であるラムゼー数に関する問題について、引き続き研究を行った。Z制約以外に格子制約などの様々な規則性制約、ならびに制約の静的緩和に関する新たな手法を開発した。これらに基づいてソルバーSCSat3を実装し、ラムゼー問題に適用していくつかの成果を得た。特に顕著な成果として、ラムゼー数R(4,11)の既知最良下界98を101に改善することに成功した。
基数制約(テーマ項目B.2)に関して：最適化問題を重み付きMaxSAT問題に帰着して解くためのソルバーQwMaxSATを開発した。その中核機能の一つである重み付き基数制約処理について、従来手法におけるコードサイズ爆発等の問題点を解決すべく、新たな符号化手法を開発した。これを実際にQwMaxSATへ組み込んで実験した結果、従来手法に比べて格段の効率改善が得られることを確認した。
MaxSAT応用(計画変更後のテーマ項目C.2)に関して：QMaxSATの効果的な応用として、AES暗号鍵の復元に関する研究および提携構造問題の解決法に関する研究の各成果について論文にまとめた。また、帰納論理プログラミングをMaxSATアプローチにより模擬実行する手法の実装と実験を行い、これを化学実験支援システムに応用し、その成果について発表を行った。
以上と並行して、上記各手法のための基盤技術として必須のSATソルバーの高速化に関する研究を行い、ベンチマーク問題等において性能改善を確認した。
|
| 現在までの達成度 |
現在までの達成度
2: おおむね順調に進展している
理由
対称性制約を用いた推論誘導手法により、ラムゼー数R(4,11)に対する下界の更新等、著しい成果を得た。
新たな重み付き基数制約手法の開発により、重み付きMaxSAT問題において従来手法より格段に効率を改善した。
いくつかの応用において、QMaxSATの有効性を実証した。
以上の成果については当初の計画以上に進展している。
ただし、主たる目標である各手法のEPR化についての進捗は十分でない。
|
| 今後の研究の推進方策 |
大規模組合せ問題ならびに最適化問題の効率的な解法として、これまでに主としてSATアプローチにて開発した手法をさらに発展・洗練させる。
その成果を踏まえた上で、MGTP等のEPR処理系を指向した技術に発展させる。
|
| 次年度使用額が生じた理由 |
今年度は人件費・謝金の支出が不要であったため。
|
| 次年度使用額の使用計画 |
次年度は人件費・謝金に充当する予定である。
|
