制約最適化問題のSAT変換による解法とその並列分散処理に関する研究

2011 年度 研究成果報告書

• 研究課題/領域番号: 20240003
• 研究種目: 基盤研究(A)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 神戸大学
• 研究代表者: 田村 直之 神戸大学, 情報基盤センター, 教授 (60207248)
• 研究分担者: 番原 睦則 神戸大学, 情報基盤センター, 准教授 (80290774) ; 平山 勝敏 神戸大学, 海事科学研究科, 准教授 (00273813) ; 井上 克巳 国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321) ; 岩沼 宏治 山梨大学, 医学工学総合研究部, 教授 (30176557) ; 鍋島 英知 山梨大学, 医学工学総合研究部, 准教授 (10334848) ; 山本 泰生 山梨大学, 医学工学総合研究部, 助教 (30550793) ; 横尾 真 九州大学, システム情報科学研究院, 教授 (20380678) ; 長谷川 隆三 九州大学, システム情報科学研究院, 教授 (20274483) ; 藤田 博 九州大学, システム情報科学研究院, 准教授 (70284552) ; 越村 三幸 九州大学, システム情報科学研究院, 助教 (30274492)
• 連携研究者: 上田 和紀 早稲田大学, 理工学術院情報理工学科, 教授 (10257206)
• 研究期間 (年度): 2008 – 2011
• キーワード: SAT / 制約最適化問題 / 並列処理・分散処理

研究概要

制約充足および最適化問題に対するSAT技術と,その並列分散実装に関する研究を進め, 105件の雑誌論文公表, 67件の学会発表を行った.また,世界をリードするソフトウェアを開発した. 2008年と2009年のCSPソルバー競技会グローバル制約部門優勝のSugar, 2011年SAT競技会応用UNSAT部門優勝のGlueMiniSat, 2010年と2011年のMax. SAT競技会部分Max. SAT応用部門優勝のQMaxSAT.

研究成果

• [雑誌論文] Glue Mini Sat2. 2. 5 :単位伝搬を促す学習節の積極的獲得戦略に基づく高速SATソルバー (2012)
  • 著者名/発表者名: 鍋島英知, 岩沼宏治, 井上克巳
  • 雑誌名: コンピュータソフトウェア
  • 査読あり
• [雑誌論文] Scala上の制約プログラミング用ドメイン特化言語Coprisについて (2012)
  • 著者名/発表者名: 田村直之, 丹生智也, 番原睦則
  • 雑誌名: コンピュータソフトウェア
  • 査読あり
• [雑誌論文] QMaxSAT : A Partial Max-SAT Solver, Journal on Satisfiabiliy (2012)
  • 著者名/発表者名: M. Koshimura, T. Zhang, H. Fujita, R. Hasegawa
  • 雑誌名: Boolean Modeling and Computation 巻: Vol.8 ページ: 95-100
  • 査読あり
• [雑誌論文] 値変更コスト付き動的SATの定式化とその解法 (2011)
  • 著者名/発表者名: 波多野大督, 平山勝敏
  • 雑誌名: 人工知能学会論文誌 巻: 26巻, 6号 ページ: 682-691
  • 査読あり
• [雑誌論文] 擬似木に基づく分散制約最適化問題の精度保証付き非厳密解法の提案 (2011)
  • 著者名/発表者名: 沖本天太, ジョヨンジュン, 岩崎敦, 横尾真
  • 雑誌名: 情報処理学会論文誌 巻: 52巻, 12号 ページ: 3786-3795
  • 査読あり
• [雑誌論文] A Compact and Efficient SAT-Encoding of Finite Domain CSP (2011)
  • 著者名/発表者名: T. Tanjo, N. Tamura, M. Banbara
  • 雑誌名: Proc of 14th Int' l Conf. on Theory and Applications of Satisfiability Testing(SAT 2011) ページ: 375-376
  • 査読あり
• [雑誌論文] SAT変換に基づく制約ソルバーとその性能評価 (2010)
  • 著者名/発表者名: 田村直之, 丹生智也, 番原睦則
  • 雑誌名: コンピュータソフトウェア 巻: 27巻 ページ: 183-196
  • 査読あり
• [雑誌論文] Solving Open Job-Shop Scheduling Problems by SAT Encoding (2010)
  • 著者名/発表者名: M. Koshimura, H. Nabeshima, H. Fujita, R. Hasegawa
  • 雑誌名: IEICE Trans. on Information and Systems 巻: Vol.E93-D ページ: 2316-2318
  • 査読あり
• [雑誌論文] A SAT-based Method for Solving the Two-dimensional Strip Packing Problem (2010)
  • 著者名/発表者名: T. Soh, K. Inoue, N. Tamura, M. Banbara, H. Nabeshima
  • 雑誌名: Fundamenta Informaticae 巻: Vol.102 ページ: 467-487
  • 査読あり
• [雑誌論文] From Inverse Entailment to Inverse Subsumption (2010)
  • 著者名/発表者名: Y. Yamamoto, K. Inoue, K. Iwanuma
  • 雑誌名: Proc of 20th Int' l Conf. on Inductive Logic Programming(ILP 2010)
  • 査読あり
• [雑誌論文] 分散制約最適化問題へのソフトアーク整合の適用 (2010)
  • 著者名/発表者名: 松井俊浩, M. C. Silaghi, 平山勝敏, 横尾真, 松尾啓志
  • 雑誌名: 人工知能学会論文誌 巻: 25巻 ページ: 410-422
  • 査読あり
• [雑誌論文] Compiling Finite Linear CSP into SAT (2009)
  • 著者名/発表者名: N. Tamura, A. Taga, S. Kitagawa, M. Banbara
  • 雑誌名: Constraints 巻: Vol.27 ページ: 254-272
  • 査読あり
• [学会発表] SAT型制約ソルバーSugarについて (2011)
  • 著者名/発表者名: 田村直之, 丹生智也, 番原睦則
  • 学会等名: 第81回人工知能学会人工知能基本問題研究会
  • 発表場所: 山梨大学
  • 年月日: 2011-01-31
• [学会発表] Solving Constraint Satisfaction Problems by a SAT Solver (2010)
  • 著者名/発表者名: N. Tamura, T. Tanjo, M. Banbara
  • 学会等名: Joint Workshop on Implementation of Constraint Logic Programming Systems and Logic-based Methods in Programming Environments
  • 発表場所: Edinburgh(Scotland)
  • 年月日: 2010-07-15
• [学会発表] Solving Constraint Satisfaction Problems with SAT Technology (2010)
  • 著者名/発表者名: N. Tamura, T. Tanjo, M. Banbara
  • 学会等名: 10th Int' l Symp. on Functional and Logic Programming
  • 発表場所: 東北大学(宮城県)
  • 年月日: 2010-04-19
• [学会発表] A Parallel SAT Solver for Clusters (2009)
  • 著者名/発表者名: K. Ohmura, K. Ueda
  • 学会等名: 12th Int' l Conf. on Theory and Applications of Satisfiability Testing
  • 発表場所: Swansea(Wales)
  • 年月日: 2009-07-03
• [学会発表] 並列分散型SATソルバにおける探索空間の分割手法の提案 (2009)
  • 著者名/発表者名: 高見明秀, 鍋島英知, 岩沼宏治
  • 学会等名: 電子情報通信学会
  • 発表場所: 佐賀大学
  • 年月日: 2009-03-02
• [備考]
  • URL: http://www.edu.kobe-u.ac.jp/istc-tamlab/cspsat/