2013 Fiscal Year Research-status Report
基数制約を用いたＳＡＴソルバーの拡張とその応用に関する研究
| Project/Area Number |
25330085
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
越村 三幸 九州大学, システム情報科学研究科(研究院, 助教 (30274492)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
長谷川 隆三 九州大学, システム情報科学研究科(研究院, 教授 (20274483)
藤田 博 九州大学, システム情報科学研究科(研究院, 准教授 (70284552)
力 規晃 徳山工業高等専門学校, 情報電子工学科, 助手 (50290804)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | SATソルバー / 組合せ最適 / SAT符号化 / 基数制約 |
|---|
| Research Abstract |
本年度は，(A) SATソルバー，(B) MaxSATソルバー，(C) MaxSATの応用，(D) 基数制約のSAT符号化について研究を進め，4件の査読付き論文の公表，4件の学会発表を行った．
(A)については，重複証明を回避するために作られる学習節の評価尺度と保持量に着目し，SATソルバーMiniSat2.2の改良を行った．（評価尺度として広く用いられている）LBDを改良した尺度で低い評価の学習節を積極的に削除すると性能が向上することを定量的に確かめた．また，SATソルバー競技会（SAT Competition 2013）に出品し，
SINNminisat 1.0.0がMiniSAT Hack-track部門で１位，ZENN 0.1.0がCore Solvers, Sequential Application SAT部門で２位の成績をおさめた．
(B) については，重み付きMaxSAT問題にも対応できるようにMaxSATソルバーQMaxSATを拡張した．QMaxSATの性能に大きく関わる基数制約のSAT符号化については，4種類を組込んで問題により切り替えられるようにした．また，MaxSATソルバー評価会（Max-SAT 2013）に出品し，QMaxSAT2-mtがPartial Max-SAT, Industrial部門で２位の成績をおさめた．
(C) については，MaxSATを用いたAES暗号鍵の復元法を考案し，SATによる従来手法に比べ，高速に復元できることを確かめた．(D) については，昨年度考案したModulo Totalizerについて，計算量的な解析を進めるとともにQMaxSATに組込んで性能評価を行った．
定期的な研究活動については，力研究分担者が２ヶ月に１回程度，九州大学を訪問し，成果発表・研究交流・情報交換を行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
(A)については，学習節の評価尺度/保持数の探究を進め，SATソルバーの性能改善に成功した．SAT競技会での結果によるとこのソルバーは世界トップクラスの性能を示しており，目的を上回る成果が得られた．
(B)については，基数制約のSAT符号化法を複数組込んだMaxSATソルバーの実装については，概ね計画通りであるが，UNSATコアを利用したソルバーについては着手できなかった．
(C)については，「MaxSATによるAES暗号鍵の復元」の着想に至り，論文が国際会議に採録されたことは，想定外の進展であった．(D)については，ソルバーの学習節生成機能を考慮したSAT符号化については着手できなかった．一方，arc consistencyを持つ符号化は，理論面では非常に重視されているが，実用上はそれほど重要ではないらしいことが定量的に明らかなったことは評価できる．
以上，それぞれ予定より進んだ項目もあればそうでない項目もあり，全体として「おおむね順調に進展している」と評価した．
|
| Strategy for Future Research Activity |
概ね，当初計画とおりに進めて行く予定であるが，(B)については，MaxSAT節の簡単化機能の組込みに着手したいと考えている．この機能については，当初の計画にはなかったものである．また，帰納論理プログラムのMaxSAT符号化についても取り組んでいきたい．
|
Research Products
(9 results)
