• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2013 Fiscal Year Research-status Report

大規模組合せ最適化問題のEPR解法に関する研究

Research Project

Project/Area Number 25330262
Research Category

Grant-in-Aid for Scientific Research (C)

Research InstitutionKyushu University

Principal Investigator

藤田 博  九州大学, システム情報科学研究科(研究院, 准教授 (70284552)

Co-Investigator(Kenkyū-buntansha) 長谷川 隆三  九州大学, システム情報科学研究科(研究院, 教授 (20274483)
越村 三幸  九州大学, システム情報科学研究科(研究院, 助教 (30274492)
Project Period (FY) 2013-04-01 – 2016-03-31
KeywordsEPRソルバー / SATソルバー / ラムゼー数 / 対称性制約 / 基数制約 / MaxSAT問題 / 最適化問題 / 帰納論理プログラミング
Research Abstract

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問題として模擬実行する手法の考案と実装である。

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

1. 対称性制約の強制と緩和の手法により、ラムゼー数R(4,8)に対する下界の更新等、著しい成果を得た。
2. モジュラー基数制約の考案と実装により、MaxSAT問題解決を従来手法より格段に効率改善できた。
3. QMaxSATの新たな応用分野を開拓できた。
4. 一方、全体的にEPR化の進捗は十分でない。
5. また、SA,GA,PSO等の進化計算に関しては不十分な進捗である。

Strategy for Future Research Activity

全体的にSATソルバーの拡張から、MGTP等のEPR処理系を指向した研究に発展させる。
また、テーマC.1~C.2について見直しを行い、進化計算に関する研究からMaxSAT応用に関する研究にシフトする。

  • Research Products

    (13 results)

All 2013 Other

All Journal Article (4 results) (of which Peer Reviewed: 4 results) Presentation (7 results) (of which Invited: 1 results) Remarks (2 results)

  • [Journal Article] SCSat: A Soft Constraint Guided SAT Solver,2013

    • Author(s)
      Hiroshi Fujita, Miyuki Koshimura, and Ryuzo Hasegawa
    • Journal Title

      Proceedings of 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013)

      Volume: 1 Pages: 415-421

    • DOI

      10.1007/978-3-642-39071-5_32

    • Peer Reviewed
  • [Journal Article] Modulo 計算に基づく基数制約のCNF符号化方式の提案と評価2013

    • Author(s)
      小川 徹,劉 洋洋,長谷川 隆三,越村 三幸,藤田 博
    • Journal Title

      九州大学 システム情報科学紀要

      Volume: 第18巻 Pages: 85-92

    • Peer Reviewed
  • [Journal Article] Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers2013

    • Author(s)
      Toru Ogawa, YangYang Liu, Ryuzo Hasegawa, Miyuki Koshimura, and Hiroshi Fujita
    • Journal Title

      Proceedings of IEEE 25th International Conference on Tools with Artificial Intelligence(ICTAI 2013)

      Volume: 1 Pages: 9-17

    • DOI

      10.1109/ICTAI.2013.13

    • Peer Reviewed
  • [Journal Article] Using MaxSAT to Correct Errors in AES Key Schedule Images2013

    • Author(s)
      Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Hiroshi Fujita, and Ryuzo Hasegawa
    • Journal Title

      Proceedings of IEEE 25th International Conference on Tools with Artificial Intelligence(ICTAI 2013)

      Volume: 1 Pages: 284-291

    • DOI

      10.1109/ICTAI.2013.51

    • Peer Reviewed
  • [Presentation] Using MaxSAT to Correct Errors in AES Key Schedule Images2013

    • Author(s)
      Xiaojuan Liao, 越村 三幸,藤田 博,長谷川 隆三
    • Organizer
      論理と推論の理論, 実装, 応用に関する合同セミナー
    • Place of Presentation
      北海道大学 工学部C304 ERATOセミナ室
    • Year and Date
      20130726-20130726
  • [Presentation] 〔招待講演〕制約を利用したSAT解法2013

    • Author(s)
      長谷川 隆三
    • Organizer
      論理と推論の理論, 実装, 応用に関する合同セミナー
    • Place of Presentation
      北海道大学 工学部C304 ERATOセミナ室
    • Year and Date
      20130725-20130725
    • Invited
  • [Presentation] 〔デモ発表〕QwMaxSAT: a Weighted Partial MaxSAT Solver2013

    • Author(s)
      越村 三幸
    • Organizer
      論理と推論の理論, 実装, 応用に関する合同セミナー
    • Place of Presentation
      北海道大学 工学部C304 ERATOセミナ室
    • Year and Date
      20130725-20130725
  • [Presentation] 〔デモ発表〕SCSat: A Soft Constraint Guided SAT Solver2013

    • Author(s)
      藤田 博
    • Organizer
      論理と推論の理論, 実装, 応用に関する合同セミナー
    • Place of Presentation
      北海道大学 工学部C304 ERATOセミナ室
    • Year and Date
      20130725-20130725
  • [Presentation] SATソルバーの学習節を考慮した新高速化法2013

    • Author(s)
      早田 翔,長谷川 隆三,藤田 博,越村 三幸
    • Organizer
      2013年度 人工知能学会全国大会(第27回)
    • Place of Presentation
      富山国際会議場
    • Year and Date
      20130605-20130605
  • [Presentation] SCSatを用いたラムゼー数の下界更新について2013

    • Author(s)
      藤田 博
    • Organizer
      2013年度 人工知能学会全国大会(第27回)
    • Place of Presentation
      富山国際会議場
    • Year and Date
      20130605-20130605
  • [Presentation] MaxSATソルバ用いた高分子の組成と物性との関係に関する考察2013

    • Author(s)
      力 規晃,越村 三幸,西田 光生,阿部 幸浩,藤田 博,長谷川 隆三
    • Organizer
      2013年度 人工知能学会全国大会(第27回)
    • Place of Presentation
      富山国際会議場
    • Year and Date
      20130605-20130605
  • [Remarks] SCMiniSAT

    • URL

      https://sites.google.com/site/scminisat/

  • [Remarks] Ramsey Graphs

    • URL

      https://sites.google.com/site/ramseygraphs/

URL: 

Published: 2015-05-28  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi