| 研究課題/領域番号 |
25330262
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
藤田 博 九州大学, システム情報科学研究科(研究院, 准教授 (70284552)
|
|---|
| 研究分担者 |
長谷川 隆三 九州大学, システム情報科学研究科(研究院, 教授 (20274483)
越村 三幸 九州大学, システム情報科学研究科(研究院, 助教 (30274492)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | EPRソルバー / SATソルバー / ラムゼー数 / 対称性制約 / 基数制約 / MaxSAT問題 / 最適化問題 / 帰納論理プログラミング |
|---|
| 研究概要 |
A.1. 対称性制約の強制と緩和
ラムゼー問題を主たる対象として研究を行った。順当な対称性制約として、Zebra制約そのほかいくつかの効果的な制約を考案した。これらの対称性制約を問題毎に最適の割合で緩和する探索制御の手法を開発した。本方式に基づき、SCSatと称するソルバーを実装した。SCSatをラムゼー問題に適用していくつかの注目すべき成果を得た。特に著しい成果として、ラムゼー数R(4,8)の最良既知下界56を58に改善することができた。
B.1. モジュラー基数制約
MaxSAT問題のソルバーQMaxSATに必須の基数制約として、従来のTotalizerを剰余演算によって拡張したModulo Totalizerを考案した。従来方式で基数制約式が莫大となってメモリアウトしていた問題も本方式では式が格段に簡単となり、実行可能なサイズに抑えられる。QMaxSATに実装し、多くのベンチマーク問題で顕著な効率改善が得られることを確認した。
C.1. EPRのための進化計算
今年度は、最適化問題対応の処理系としてのQMaxSAT自体の応用可能性の追究に焦点を当てて研究を行った。その結果、二つの効果的な応用例を見出すことができた。一つは、AES暗号系に対する攻撃の一種におけるQMaxSATの効果的な利用方法の提示である。もう一つは、帰納論理プログラミングをMaxSAT問題として模擬実行する手法の考案と実装である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
1. 対称性制約の強制と緩和の手法により、ラムゼー数R(4,8)に対する下界の更新等、著しい成果を得た。
2. モジュラー基数制約の考案と実装により、MaxSAT問題解決を従来手法より格段に効率改善できた。
3. QMaxSATの新たな応用分野を開拓できた。
4. 一方、全体的にEPR化の進捗は十分でない。
5. また、SA,GA,PSO等の進化計算に関しては不十分な進捗である。
|
| 今後の研究の推進方策 |
全体的にSATソルバーの拡張から、MGTP等のEPR処理系を指向した研究に発展させる。
また、テーマC.1～C.2について見直しを行い、進化計算に関する研究からMaxSAT応用に関する研究にシフトする。
|
