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

• 研究課題/領域番号: 19700025
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 神戸大学
• 研究代表者: 番原 睦則 神戸大学, 学術情報基盤センター, 准教授 (80290774)
• 研究期間 (年度): 2007 – 2009
• 研究課題ステータス: 完了 (2009年度)
• 配分額: 3,270千円 (直接経費: 2,700千円、間接経費: 570千円); 2009年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2008年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2007年度: 800千円 (直接経費: 800千円)
• キーワード: Prolog / SAT / 制約充足問題 / 論理プログラミング / 並列計算

研究概要

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

研究成果

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