A Study on EPR Prover for Solving Large-scale SAT Problems

2012 Fiscal Year Final Research Report

• Project/Area Number: 21300054
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Intelligent informatics
• Research Institution: Kyushu University
• Principal Investigator: HASEGAWA Ryuzo 九州大学, システム情報科学研究院, 教授 (20274483)
• Co-Investigator(Kenkyū-buntansha): FUJITA Hiroshi 九州大学, システム情報科学研究院, 准教授 (70284552) ; KOSHIMURA Miyuki 九州大学, システム情報科学研究院, 助教 (30274492) ; CHIKARA Noriaki 徳山工業高等専門学校, 情報電子工学科, 助手 (50290804)
• Project Period (FY): 2009 – 2012
• Keywords: 探索・論理・推論アルゴリズム / SATソルバー / EPR論理

Research Abstract

We conducted the research on technologies solving large-scale Constraint Satisfaction/Optimization Problems by combining SAT technologies and model generation technologies, and published 9 refereed papers and made 36 presentations. In addition, world’s leading softwares QMaxSAT and SCMiniSat were developed. QMaxSAT won at the 2010, 2011, and 2012 Max-SAT evaluations in an industrial category and SCMiniSat increased the lower bound of Ramsey number R(4,8) from 56 to 58.

Research Products

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