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

2010 年度 自己評価報告書

• 研究課題/領域番号: 20240003
• 研究種目: 基盤研究(A)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 神戸大学
• 研究代表者: 田村 直之 神戸大学, 情報基盤センター, 教授 (60207248)
• 研究期間 (年度): 2008 – 2011
• キーワード: SAT / 制約最適化問題 / 並列処理・分散処理

研究概要

(1)制約最適化問題と制約充足問題(以下まとめてCSPと呼ぶ),SAT変換に基づく並列SATソルバーによる解法に着目し,実用的規模の問題を高速に解くための手法の研究,実証ソフトウェアの開発,および評価を目的とした
(2)既存SAT技術のCSPへの適用について,適用分野の拡大,大規模な問題への対応,高速な求解の実現を研究課題とし,対応する研究グループを組織して研究を進めた

研究成果

• [雑誌論文] 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
  • 査読あり
• [雑誌論文] 分散制約最適化問題へのソフトアーク整合の適用 (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 Systerns and Logic-based Methods in Prograrmming 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
• [学会発表] c-sat : A Parallel SAT Solver for Clusters (2009)
  • 著者名/発表者名: K.Ohmura, K.Ueda
  • 学会等名: 12th Int' l Conf on Theory and Applications of Satisfiability Testing (SAT 2009)
  • 発表場所: Swansea (Wales).
  • 年月日: 2009-07-03
• [学会発表] 並列分散型SATソルベにおける探索空間の分割手法の提案 (2009)
  • 著者名/発表者名: 高見明秀, 鍋島英知, 岩沼宏治
  • 学会等名: 電子情報通信学会IEICE-SS-444
  • 発表場所: 佐賀大学
  • 年月日: 2009-03-02
• [備考] ホームページ
  • URL: http://www.edu.kohe-u.ac.jp/istc-tamlab/cspsat/