大規模SAT問題解決のためのEPRプルーバーに関する研究

2012 年度 研究成果報告書

• 研究課題/領域番号: 21300054
• 研究種目: 基盤研究(B)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 知能情報学
• 研究機関: 九州大学
• 研究代表者: 長谷川 隆三 九州大学, システム情報科学研究院, 教授 (20274483)
• 研究分担者: 藤田 博 九州大学, システム情報科学研究院, 准教授 (70284552) ; 越村 三幸 九州大学, システム情報科学研究院, 助教 (30274492) ; 力 規晃 徳山工業高等専門学校, 情報電子工学科, 助手 (50290804)
• 研究期間 (年度): 2009 – 2012
• キーワード: 探索・論理・推論アルゴリズム / SATソルバー / EPR論理

研究概要

大規模な制約充足問題および最適化問題の解法技術を,SAT技術とモデル生成法を組み合わせることによって開発し,10件の雑誌論文公表,36件の学会発表を行った.また,世界をリードするソフトウェアQMaxSATとSCMiniSatを開発した.前者は2010年から3年連続で国際競技会で優勝,後者はRamsey数R(4,8)の下界を56から58に更新した.

研究成果

• [雑誌論文] A New Lower Bound for the Ramsey (2012)
  • 著者名/発表者名: H. Fujita
  • 雑誌名: CoRR abs 巻: Number R(4, 8) ページ: 1212-1328
• [雑誌論文] Solving the Coalition Structure Generation Problem with MaxSAT (2012)
  • 著者名/発表者名: X. Liao, M. Koshimura, H. Fujita, R.Hasegawa
  • 雑誌名: Proc. of 24th Int'l Conf. on Tools with Artificial Intelligence ページ: 910-915
  • 査読あり
• [雑誌論文] A Partial Max-SAT Solver (2012)
  • 著者名/発表者名: M. Koshimura, T. Zhang, H. Fujita, R. Hasegawa, QMaxSAT
  • 雑誌名: J. on Satisfiability, Boolean Modeling and Computation 巻: Vol.8 ページ: 95-100
  • 査読あり
• [雑誌論文] QMaxSAT version 0.3 & 0.4 (2011)
  • 著者名/発表者名: X. An, M. Koshimura, H. Fujita, R. Hasegawa
  • 雑誌名: Proc. of FTP 2011 ページ: 7-15
  • 査読あり
• [雑誌論文] A Multi-Layer Hybrid Particle Swarm Optimization Model for Flow Shop Scheduling (2010)
  • 著者名/発表者名: X,-F. Zhang, B. Tong, M. Koshimura, H. Fujita, R. Hasegawa.
  • 雑誌名: Australian Journal of Intelligent Information Processing Systems 巻: Vol.12, No.4 ページ: 1-6
  • 査読あり
• [雑誌論文] 極小モデル生成器MiniMGの試作 (2010)
  • 著者名/発表者名: 矢野 明浩,中村 徹,長谷川 隆三,藤田 博,越村 三幸
  • 雑誌名: 九州大学大学院システム情報科学紀要 巻: 第15巻,第2号 ページ: 91-98
  • 査読あり
• [雑誌論文] Solving Open Job-Shop Scheduling Problems by SAT Encoding (2010)
  • 著者名/発表者名: M. Koshimura, H. Nabeshima, H. Fujita, R. Hasegawa
  • 雑誌名: IEICE TRANSACTIONS on Information and Systems (Letter) 巻: Vol.E93-D, No.8 ページ: 2316-2318
  • 査読あり
• [雑誌論文] モデル列挙とモデル計数 (2010)
  • 著者名/発表者名: 長谷川 隆三,藤田 博,越村 三幸
  • 雑誌名: 人工知能学会誌 巻: Vol.25,No.1 ページ: 96-104
  • 査読あり
• [雑誌論文] Minimal Model Generation with respect to an Atom Set (2009)
  • 著者名/発表者名: M. Koshimura, H. Nabeshima, H. Fujita, R.Hasegawa
  • 雑誌名: Proc. of FTP 2009 ページ: 49-59
  • 査読あり
• [学会発表] モデル生成型SATソルバーの学習節による分岐効果について (2012)
  • 著者名/発表者名: 佐々木 佑介,長谷川 隆三
  • 学会等名: 人工知能基本問題研究会(第87回)
  • 発表場所: 慶応義塾大学 日吉キャンパス
  • 年月日: 2012-11-17
• [学会発表] MaxSATの一拡張について (2012)
  • 著者名/発表者名: 越村 三幸,廖 暁鵑,藤田 博,長谷川 隆三
  • 学会等名: 第11回情報科学技術フォーラム(FIT 2012)
  • 発表場所: 法政大学 小金井キャンパス
  • 年月日: 2012-09-05
• [学会発表] 帰納論理プログラミングを用いた高分子の組成と物性との関係に関する考察 (2012)
  • 著者名/発表者名: 力 規晃,越村 三幸,橋 本 司,西田 光生,阿部 幸浩,藤田 博,長谷川 隆三
  • 学会等名: 第11回情報科学技術フォーラム(FIT 2012)
  • 発表場所: 政大学 小金井キャンパス
  • 年月日: 2012-09-04
• [学会発表] 部分MaxSATソルバーの簡便な一実装 (2011)
  • 著者名/発表者名: QMaxSAT
  • 学会等名: 日本ソフトウェア科学会第28回大会
  • 発表場所: 沖縄産業支援センター
  • 年月日: 2011-09-29
• [学会発表] UNIXのFORK機能に基づくSATソルバーの並列化 (2011)
  • 著者名/発表者名: 明石 裕子,越村 三幸,藤田 博,長谷川隆三
  • 学会等名: 日本ソフトウェア科学会第28回大会
  • 発表場所: 沖縄産業支援センター
  • 年月日: 2011-09-27
• [学会発表] QMaxSAT: Q-dai MaxSAT ソルバー (2011)
  • 著者名/発表者名: 越村 三幸,安 宣〓,藤田 博,長谷川 隆三.
  • 学会等名: 2011年度 人工知能学会全国大会(第25回)
  • 発表場所: アイーナ いわて県民情報交流センター
  • 年月日: 2011-06-03
• [学会発表] Partial Max-SAT ソルバー QMaxSATの評価 (2011)
  • 著者名/発表者名: 越村 三幸,張 〓,藤田 博,長谷川 隆三
  • 学会等名: 人工知能基本問題研究会(第81回)
  • 発表場所: 山梨大学甲府キャンパス
  • 年月日: 2011-01-31
• [学会発表] BOINCによるSATソルバーの並列実行 (2010)
  • 著者名/発表者名: 力 規晃,越村 三幸,藤田 博,長谷川 隆三
  • 学会等名: 第9回情報科学技術フォーラム(FIT2010)
  • 発表場所: 九州大学 伊都キャンパス
  • 年月日: 2010-09-08
• [学会発表] モデル生成によるSATソルバの並列化 (2010)
  • 著者名/発表者名: 矢野 明浩,越村 三幸,藤田 博,長谷川隆三
  • 学会等名: 情報処理学会創立50周年記念(第72回)全国大会
  • 発表場所: 東京大学本郷キャンパス
  • 年月日: 2010-03-09
• [学会発表] SAT変換による未解決ジョブショップスケジューリング問題への挑戦 (2009)
  • 著者名/発表者名: 越村 三幸,鍋島 英知,藤田 博,長谷川 隆三
  • 学会等名: スケジューリング・シンポジウム2009
  • 発表場所: 岡山大学
  • 年月日: 2009-09-17
• [備考]
  • URL: https://sites.google.com/site/qmaxsat/
• [備考]
  • URL: http://opal.inf.kyushu-u.ac.jp/~fujita/
• [産業財産権] 実験システム,実験支援方法,および実験支援プログラム (2013)
  • 発明者名: 長谷川 隆三,藤田 博,越村 三幸,力 規晃,阿部幸浩,西田光生
  • 権利者名: 長谷川 隆三,藤田 博,越村 三幸,力 規晃,阿部幸浩,西田光生
  • 産業財産権番号: 特願2013-031416
  • 出願年月日: 2013-02-20