Prolog処理系を用いた複数SATソルバ並列実行システム

2009 年度 研究成果報告書

• 研究課題/領域番号: 19700025
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 神戸大学
• 研究代表者: 番原 睦則 神戸大学, 学術情報基盤センター, 准教授 (80290774)
• 研究期間 (年度): 2007 – 2009
• キーワード: Prolog / SAT / 制約充足問題

研究概要

論理プログラミング・システム上で,複数のSATソルバーを並行動作させるハイブリッド型SATソルバーに関する研究を行った.組合せテストのテストケース生成問題をベンチマークとして,複数のSATソルバーを用いて求解した結果,最適値が未知であった問題(3問)について,既知の上限が最適値であることを証明することに成功した.

研究成果

• [雑誌論文] 制約最適化問題とSAT符号化 (2010)
  • 著者名/発表者名: 田村直之, 丹生智也, 番原睦則
  • 雑誌名: 人工知能学会誌 25巻1号 ページ: 77-85
  • 査読あり
• [雑誌論文] SATによるシステム検証 (2010)
  • 著者名/発表者名: 番原睦則, 田村直之
  • 雑誌名: 人工知能学会誌 25巻1号 ページ: 122-129
  • 査読あり
• [雑誌論文] Compiling Finite Linear CSP into SAT, Constraints (2009)
  • 著者名/発表者名: N. Tamura, A. Taga, S. Kitagawa, M. Banbara
  • 雑誌名: Vol.14Issue.2 ページ: 254-272
  • 査読あり
• [雑誌論文] System Description of a SAT-based CSP Solver Sugar (2008)
  • 著者名/発表者名: N. Tamura, T. Tanjo, M. Banbara
  • 雑誌名: Proceedings of the Third International CSP Solver Competition ページ: 71-75
  • 査読あり
• [雑誌論文] Sugar++: A SAT-based MAX-CSP/COP Solver (2008)
  • 著者名/発表者名: T. Tanjo, N. Tamura, M. Banbara
  • 雑誌名: Proceedings of the Third International CSP Solver Competition ページ: 77-82
  • 査読あり
• [雑誌論文] Sugar: A CSP to SAT Translator Based on Order Encoding (2008)
  • 著者名/発表者名: N. Tamura, M. Banbara
  • 雑誌名: Proceedings of the Second International CSP Solver Competition ページ: 65-69
  • 査読あり
• [雑誌論文] PrologからJavaへのトランスレータ処理系とその応用 (2007)
  • 著者名/発表者名: 番原睦則, 田村直之, 井上克己
  • 雑誌名: コンピュータソフトウェア 24巻3号 ページ: 75-86
  • 査読あり
• [学会発表] 制約充足問題のSAT変換とグラフ彩色問題への応用 (2009)
  • 著者名/発表者名: 丹生智也, 田村直之, 番原睦則
  • 学会等名: 日本ソフトウェア科学会第26回大会
  • 発表場所: 島根大学(島根県)
  • 年月日: 20090916-20090918
• [学会発表] PrologからJavaへのトランスレータ処理系の設計と実装 (2009)
  • 著者名/発表者名: 丹生智也, 番原睦則, 田村直之
  • 学会等名: 第11回プログラミングおよびプログラミング言語ワークショップ(PPL2009)
  • 発表場所: 高山グリーンホテル
  • 年月日: 2009-03-10
• [学会発表] SAT変換に基づく制約ソルバーSugar (2009)
  • 著者名/発表者名: 番原睦則, 丹生智也, 田村直之
  • 学会等名: 第11回プログラミングおよびプログラミング言語ワークショップ(PPL2009)
  • 発表場所: 高山グリーンホテル
  • 年月日: 2009-03-10
• [学会発表] ショップ・スケジューリング問題のSAT変換による解法 (2007)
  • 著者名/発表者名: 田村直之, 多賀明子, 番原睦則, 宋剛秀, 鍋島英知, 井上克己
  • 学会等名: スケジューリング・シンポジウム
  • 発表場所: 京都大学
  • 年月日: 20070929-20070930
• [学会発表] グリッド計算環境上でのショップ・スケジューリング問題のSAT変換による解法 (2007)
  • 著者名/発表者名: 多賀明子, 田村直之, 北川哲, 番原睦則, 田村直之
  • 学会等名: スケジューリング・シンポジウム
  • 発表場所: 京都大学
  • 年月日: 20070929-20070930
• [学会発表] Sugar:SAT変換による制約解消システムのデモ (2007)
  • 著者名/発表者名: 田島宏史, 多賀明子, 丹生智也, 田村直之, 番原睦則
  • 学会等名: 日本ソフトウェア科学会第24回大会
  • 発表場所: 奈良先端科学技術大学院大学
  • 年月日: 20070912-20070914
• [学会発表] Prolog Cafe:PrologからJavaへのトランスレータ処理系のデモ (2007)
  • 著者名/発表者名: 丹生智也, 田村直之, 番原睦則
  • 学会等名: 日本ソフトウェア科学会第24回大会
  • 発表場所: 良先端科学技術大学院大学
  • 年月日: 20070912-20070914
• [備考]
  • URL: http://kaminari.istc.kobe-u.ac.jp/PrologCafe/