| 研究課題/領域番号 |
25330085
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
越村 三幸 九州大学, システム情報科学研究科(研究院, 助教 (30274492)
|
|---|
| 研究分担者 |
長谷川 隆三 九州大学, システム情報科学研究科(研究院, 教授 (20274483)
藤田 博 九州大学, システム情報科学研究科(研究院, 准教授 (70284552)
力 規晃 徳山工業高等専門学校, その他部局等, 助手 (50290804)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | SATソルバー / 組合せ最適 / SAT符号化 / 基数制約 |
|---|
| 研究実績の概要 |
本年度も，(A)SATソルバー，(B)MaxSATソルバー，(C)MaxSATの応用，(D)基数制約のSAT符号化について研究を進め，2件の査読付き論文の公表，9件の学会発表（うち招待講演2件）を行った．
(A)については，「SATソルバーの傾向判定による高速化手法の探求」と「並列SATソルバーSATzilla2012の開発」を行った．(B)については，「節集合の簡単化，緩和法の適用，及び二分探索によるMaxSATソルバーの高速化」を図った．
(C)については，「MaxSATソルバーを用いた帰納論理プログラミング」の幾つかの手法の試作を行った．また，MaxSATを利用したAES暗号鍵の復元法の改良案について検討を始めた．また，MaxSAT評価会（MaxSAT2014）に出品し，PMS-crafted部門とWPMS-crafted部門で５位，PMS-industrail部門で７位，WPMS-industrail部門で８位の成績を収めた．
(D)については，新しい符号化Weighted Totalizerの提案と試作，そして，ある特徴を持つMaxSATインスタンスに効果のあるPartial Encodingの試作を行った．
研究打ち合わせを九州大学で7回，徳山高専で3回行った．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
(A)については，当初予定になかったSATソルバーの並列化ができた点は評価できる．
(B)については，当初予定になかった高速化手法の評価ができたのは進展であったが，PBソルバーの開発に進めなかった点が，遅れている点である．
(C)については，帰納論理プログラミングのMaxSAT符号化の昨年度の手法に若干の問題があることが判明したが，対応策を講じることができた．また，雑誌論文として今年度再録されたAES暗号鍵の復元法に関して改良案の着想に至った点は進展であった．
(D)については，二つの新しい手法Weighted TotalizerとPartial Encodingを提案できたのは進展であった．
以上，それぞれ予定より進んだ項目もあればそうでない項目もあり，全体として「おおむね順調に進展している」と評価した．
|
| 今後の研究の推進方策 |
現在作成しているMaxSATソルバーはsat-basedの探索を行う．当初これとは別に，unsatコアに基づく探索を行うMaxSATソルバーも作成する予定であったが，これを現在のMaxSATソルバーの探索にunsatコアに基づく探索を組み込む新方式に変更することにした．
その他の項目については，概ね当初計画通りに進めていく予定である．
|
| 次年度使用額が生じた理由 |
計算機使用料（今年度の前半は，さつき施設サービス利用料，後半は共同研究費として支払）が来年度から引き上げられることになったので，それに一部充当するために，次年度使用額が生じた．
|
| 次年度使用額の使用計画 |
次年度は，謝金を当初予定より減額し，それと上記「次年度使用額」を合わせて，計算機使用料に当てる予定である．その他の費目については当初予定通りに進める．
|
