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

• 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
• Project Status: Completed (Fiscal Year 2012)
• Budget Amount: ¥17,680,000 (Direct Cost: ¥13,600,000、Indirect Cost: ¥4,080,000); Fiscal Year 2012: ¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000); Fiscal Year 2011: ¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000); Fiscal Year 2010: ¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000); Fiscal Year 2009: ¥6,370,000 (Direct Cost: ¥4,900,000、Indirect Cost: ¥1,470,000)
• Keywords: 探索・論理・推論アルゴリズム / SATソルバー / EPR論理 / モデル生成法 / SAT / MaxSAT / 基数制約 / 並列化 / 戦略の統合 / 極小モデル生成 / SATソルバーの高速化 / 基数制約のSAT符合化 / モデル生成 / 分散処理・並列処 / 並列分散処理

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] Rule Extraction from Micro-Blog using Inductive Logic Programming (2012)
  • Author(s): Noriaki Chikara, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
  • Journal Title: Proc. of 2012 Spring World Congress on Engineering and Technology (SCET2012) Volume: 2 Pages: 257-260
  • DOI: 10.1109/scet.2012.6342076
  • Peer Reviewed
• [Journal Article] Hybrid Particle Swarm Optimization and Convergence Analysis for Scheduling Problems (2012)
  • Author(s): Xue-Feng Zhang, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
  • Journal Title: Evolutionary Computation and Multi-Agent Systems and Simulation (ECoMASS) Workshop, GECCO'12 Companion Publication Volume: なし Pages: 307-314
  • DOI: 10.1145/2330784.2330829
  • Peer Reviewed
• [Journal Article] Report on SAT Competition and Max-SAT Evaluation (2012)
  • Author(s): 鍋島 英知，越村 三幸，番原 睦則
  • Journal Title: Computer Software Volume: 29 Issue: 4 Pages: 4_9-4_14
  • DOI: 10.11309/jssst.29.4_9
  • NAID: 10031077880
  • ISSN: 0289-6540
  • Peer Reviewed
• [Journal Article] Solving the Coalition Structure Generation Problem with MaxSAT (2012)
  • Author(s): Xiaojuan Liao, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
  • Journal Title: Proc. of 24th International Conference on Tools with Artificial Intelligence Volume: なし
  • Peer Reviewed
• [Journal Article] A New Lower Bound for the Ramsey Number R(4, 8) (2012)
  • Author(s): Hiroshi Fujita
  • Journal Title: CoRR Volume: abs/1212.1328
• [Journal Article] QMaxSAT : A Partial Max-SAT Solver (2012)
  • Author(s): Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, Ryuzo Hasegawa
  • Journal Title: Journal on Satisfiability, Boolean Modeling and Computation Volume: 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] An Efficient Hybrid Particle Swarm Optimization for the Job Shop Scheduling Problem (2011)
  • Author(s): Xue-Feng Zhang, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
  • Journal Title: Proc.of 2011 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE 2011) Pages: 622-626
  • Peer Reviewed
• [Journal Article] QMaxSAT version 0.3 & 0.4 (2011)
  • Author(s): Xuanye An, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
  • Journal Title: Proc.of International Workshop on First-Order Theorem Proving (FTP 2011) Pages: 7-15
  • Peer Reviewed
• [Journal Article] Combining PSO and Local Search to Solve Scheduling Problems (2011)
  • Author(s): Xue-Feng Zhang, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
  • Journal Title: Proa.of 10th Annual Conference Companion on Genetic and Evolutionary Computation (GECCO'11) Pages: 347-357
  • Peer Reviewed
• [Journal Article] Hybrid Particle Swarm Optimization with Parameter Selection Approaches to Solve Flow Shop Scheduling Problem (2011)
  • Author(s): Xue-Feng Zhang, Xuanye An, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
  • Journal Title: Proc.of 10th IEEE Internationa Conference on Cybernetic Intelligent Systems Pages: 13-19
  • 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
  • NAID: 120002795249
  • 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
  • NAID: 10027365040
  • Peer Reviewed
• [Journal Article] モデル列挙とモデル計数 (2010)
  • Author(s): 長谷川 隆三,藤田 博,越村 三幸
  • Journal Title: 人工知能学会誌 Volume: Vol.25,No.1 Pages: 96-104
  • 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 Volume: E93-D・8 Pages: 2316-2318
  • NAID: 10027365040
  • Peer Reviewed
• [Journal Article] A Multi-Layer Hybrid Particle Swarm Optimization Model for Flow Shop Scheduling Problem (2010)
  • Author(s): X.-F.Zhang, B.Tong, M.Koshimura, Hiroshi Fujita, R.Hasegawa
  • Journal Title: Australian Journal of Intelligent Information Processing Systems Volume: 12・4 Pages: 1-6
  • Peer Reviewed
• [Journal Article] Rule Extraction from Blog Using Inductive Logic Programming (2010)
  • Author(s): N.Chikara, M.Koshimura, H.Fujita, R.Hasegawa
  • Journal Title: Int'l Workshop on Web Personalization and Recommender Systems Pages: 269-272
  • NAID: 130008064889
  • Peer Reviewed
• [Journal Article] モデル列挙とモテル計数 (2010)
  • Author(s): 長谷川, 藤田, 越村
  • Journal Title: 人工知能学会誌 25・1 Pages: 96-104
• [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
• [Journal Article] Minimal Model Generation with respect to an Atom Set (2009)
  • Author(s): M.Koshimura, H.Nabeshima, H.Fujita, R.Hasegawa
  • Journal Title: 7th International Workshop on First-Order Theorem Proving 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] SATソルバの学習節に対する新しい評価手法の提案 (2012)
  • Author(s): 奥川 巧，安本 猛，越村 三幸，藤田 博，長谷川 隆三
  • Organizer: 2012年度 人工知能学会全国大会（第26回）
  • Place of Presentation: 山口県教育会館
• [Presentation] 帰納論理プログラミングを用いた高分子の組成と物性との関係に関する考察 (2012)
  • Author(s): 力 規晃，越村 三幸，橋本 司，西田 光生，阿部 幸浩，藤田 博，長谷川 隆三
  • Organizer: 第11回情報科学技術フォーラム(FIT 2012)
  • Place of Presentation: 法政大学 小金井キャンパス
• [Presentation] モデル生成型SATソルバーの学習節による分岐効果について (2012)
  • Author(s): 佐々木 佑介，長谷川 隆三
  • Organizer: 人工知能基本問題研究会（第87回）
  • Place of Presentation: 慶応義塾大学 日吉キャンパス
• [Presentation] 部分MaxSATソルバーの簡便な一実装 (2011)
  • Author(s): QMaxSAT
  • Organizer: 日本ソフトウェア科学会第28回大会
  • Place of Presentation: 沖縄産業支援センター
  • Year and Date: 2011-09-29
• [Presentation] QMaxSAT:部分MaxSATソルバーの簡便な一実装 (2011)
  • Author(s): 越村三幸, 安宣〓, 藤田博, 長谷川隆三
  • 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] 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] 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] BOINCによるSATソルバーの並列実行 (2010)
  • Author(s): 力規晃
  • Organizer: 第9回情報科学技術フォーラム(FIT2010)
  • Place of Presentation: 九州大学(福岡)
  • Year and Date: 2010-09-08
• [Presentation] 基数制約を用いたMax-SATソルバーの試作 (2010)
  • Author(s): 張トウ
  • Organizer: 第9回情報科学技術フォーラム(FIT2010)
  • Place of Presentation: 九州大学(福岡)
  • Year and Date: 2010-09-08
• [Presentation] 帰納学習を用いたブログからのルール抽出 (2010)
  • Author(s): 力規晃
  • Organizer: 平成22年電気学会電子・情報・システム部門大会
  • Place of Presentation: 熊本大学(熊本)
  • Year and Date: 2010-09-03
• [Presentation] モデル生成型SATソルバーMiniMGの性能評価 (2010)
  • Author(s): 中村徹
  • Organizer: 人工知能基本問題研究会(第78回)
  • Place of Presentation: 兵庫県立大学(兵庫)
  • Year and Date: 2010-07-31
• [Presentation] モデル生成によるSATソルバの並列化 (2010)
  • Author(s): 矢野 明浩,越村 三幸,藤田 博,長谷川隆三
  • Organizer: 情報処理学会創立50周年記念(第72回)全国大会
  • Place of Presentation: 東京大学本郷キャンパス
  • Year and Date: 2010-03-09
• [Presentation] モデル生成によるSATソルバの並列化 (2010)
  • Author(s): 矢野, 越村, 藤田, 長谷川
  • Organizer: 情報処理学会創立50周年記念(第72回)全国大会
  • Place of Presentation: 東京大学(東京都)
  • Year and Date: 2010-03-09
• [Presentation] Solving Hard Combinatorial Problems with SAT Solvers (2009)
  • Author(s): H.Fujita
  • Organizer: Dagstuhl Seminar 09461 Algorithms and Applications for Next Generation SAT Solvers
  • Place of Presentation: SchlossDagstuhl(ドイツ)
  • Year and Date: 2009-11-12
• [Presentation] Minimal model generation with MGTP and DPLL (2009)
  • Author(s): R.Hasegawa
  • Organizer: Dagstuhl Seminar 09461 Algorithms and Applications for Next Generation SAT Solvers
  • Place of Presentation: SchlossDagstuhl(ドイツ)
  • Year and Date: 2009-11-10
• [Presentation] SAT変換による未解決ジョブショップスケジューリング問題への挑戦 (2009)
  • Author(s): 越村 三幸,鍋島 英知,藤田 博,長谷川 隆三
  • Organizer: スケジューリング・シンポジウム2009
  • Place of Presentation: 岡山大学
  • Year and Date: 2009-09-17
• [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/
• [Remarks] QMaxSAT: Q-dai MaxSAT Solver
  • URL: http://sites.google.com/site/qmaxsat/
• [Remarks]
  • URL: http://sites.google.com/site/qmaxsat/
• [Patent(Industrial Property Rights)] 実験システム,実験支援方法,および実験支援プログラム (2013)
  • Inventor(s): 長谷川 隆三,藤田 博,越村 三幸,力 規晃,阿部幸浩,西田光生
  • Industrial Property Rights Holder: 長谷川 隆三,藤田 博,越村 三幸,力 規晃,阿部幸浩,西田光生
  • Industrial Property Number: 2013-031416
  • Filing Date: 2013-02-20
• [Patent(Industrial Property Rights)] 実験支援システム、実験支援方法、および実験支援プログラム (2013)
  • Inventor(s): 長谷川隆三，藤田博，越村三幸，力規晃，阿部幸浩，西田光生
  • Industrial Property Rights Holder: 長谷川隆三，藤田博，越村三幸，力規晃，阿部幸浩，西田光生
  • Industrial Property Rights Type: 特許
  • Industrial Property Number: 2013-031416
  • Filing Date: 2013-02-20