• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2009 年度 実績報告書

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

研究課題

研究課題/領域番号 20240003
研究機関神戸大学

研究代表者

田村 直之  神戸大学, 学術情報基盤センター, 教授 (60207248)

研究分担者 番原 睦則  神戸大学, 学術情報基盤センター, 准教授 (80290774)
井上 克巳  国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321)
岩沼 宏治  山梨大学, 医学工学総合研究部, 教授 (30176557)
横尾 真  九州大学, システム情報科学研究院, 教授 (20380678)
長谷川 隆三  九州大学, システム情報科学研究院, 教授 (20274483)
キーワードSAT / 制約最適化問題 / 並列処理・分散処理
研究概要

本年度は,CSPのSAT変換(SAT符号化),動的SATに対するラグランジュ分解法の適用,SMT(Satisfiability Modulo Theories),分散制約最適化問題および提携構造形成問題とメカニズムデザイン,極小モデル生成アルゴリズム,極小集合被覆を用いたSAT解の列挙アルゴリズム,組合せテストケース生成への応用,システム生物学における代謝パスウェイ解析への応用,ジョブショップスケジューリング問題への応用,準群の存在問題への応用について研究を進め,19件の査読付論文の公表,10件の学会発表(うち大会優勝賞4件)を行った.また,「最近のSAT技術の発展」についての解説論文9編を全研究者で分担執筆し,人工知能学会誌25巻1号(2010年1月)で公表した.
本研究の研究成果の一つであるCSPソルバーSugarは,2009年国際CSPソルバー競技会の全7部門のうち3部門で優勝し,優れた性能を示した.ジョブショップスケジューリング問題への応用では,20年以上未解決であった2問について最適値決定に成功し,ソフトウェア開発という面でも,大きな成果を得た.
定期的な研究活動については,全研究者の参加するCSPSAT研究会を3回(7月,11月,3月),CSPSAT講演会を1回(2月)開催し,成果発表・研究交流・情報交換を行った.これらの集会への参加者はのべ79名(海外研究者8名を含む)だった.

  • 研究成果

    (39件)

すべて 2010 2009 その他

すべて 雑誌論文 (28件) (うち査読あり 19件) 学会発表 (10件) 備考 (1件)

  • [雑誌論文] SOLAR : An Automated Deduction System for Consequence Finding2010

    • 著者名/発表者名
      H.Nabeshima, K.Iwanuma, K.Inoue.O.Ray
    • 雑誌名

      AI Communications 23

      ページ: 183-203

    • 査読あり
  • [雑誌論文] 分散制約最適化問題へのソフトアーク整合の適用2010

    • 著者名/発表者名
      松井俊浩, M.C.Silaghi, 平山勝敏, 横尾真, 松尾啓志
    • 雑誌名

      人工知能学会論文誌 25・3(掲載確定)

    • 査読あり
  • [雑誌論文] 特集「最近のSAT技術の発展」にあたって2010

    • 著者名/発表者名
      井上克巳, 田村直之
    • 雑誌名

      人工知能学会誌 25・1

      ページ: 56-56

  • [雑誌論文] SATソルバーの基礎2010

    • 著者名/発表者名
      井上克巳, 田村直之
    • 雑誌名

      人工知能学会誌 25・1

      ページ: 57-67

  • [雑誌論文] 高速SATソルバーの原理2010

    • 著者名/発表者名
      鍋島英知, 宋剛秀
    • 雑誌名

      人工知能学会誌 25・1

      ページ: 68-76

  • [雑誌論文] 制約最適化問題とSAT符号化2010

    • 著者名/発表者名
      田村直之, 丹生智也, 番原睦則
    • 雑誌名

      人工知能学会誌 25・1

      ページ: 77-85

  • [雑誌論文] SMT:個別理論を取り扱うSAT技術2010

    • 著者名/発表者名
      岩沼宏治, 鍋島英知
    • 雑誌名

      人工知能学会誌 25・1

      ページ: 86-95

  • [雑誌論文] モデル列挙とモデル計数2010

    • 著者名/発表者名
      長谷川隆三, 藤田博, 越村三幸
    • 雑誌名

      人工知能学会誌 25・1

      ページ: 96-104

  • [雑誌論文] ★-SAT:SATの拡張2010

    • 著者名/発表者名
      平山勝敏, 横尾真
    • 雑誌名

      人工知能学会誌 25・1

      ページ: 105-113

  • [雑誌論文] SATによるプランニングとスケジューリング2010

    • 著者名/発表者名
      鍋島英知
    • 雑誌名

      人工知能学会誌 25・1

      ページ: 114-121

  • [雑誌論文] SATによるシステム検証2010

    • 著者名/発表者名
      番原睦則, 田村直之
    • 雑誌名

      人工知能学会誌 25・1

      ページ: 122-129

  • [雑誌論文] Compiling Finite Linear CSP into SAT2009

    • 著者名/発表者名
      N.Tamura, A.Taga, S.Kitagawa, M.Banbara
    • 雑誌名

      Constraints 14・2

      ページ: 254-272

    • 査読あり
  • [雑誌論文] ADOPT-ing : unifying asynchronous distributed optimization with asynchronous backtracking2009

    • 著者名/発表者名
      M.C.Silaghi, M.Yokoo
    • 雑誌名

      Journal of Autonomous Agents and Multi-Agent Systems 19・2

      ページ: 89-123

    • 査読あり
  • [雑誌論文] Coordination Planning : Applying Control Synthesis Methods for a Class of Distributed Agents2009

    • 著者名/発表者名
      K.T.Seow, C.Ma, M.Yokoo
    • 雑誌名

      IEEE Transactions on Control Systems Technology 17・2

      ページ: 405-415

    • 査読あり
  • [雑誌論文] 資源制約に束縛されない pseudo-tree を用いた資源制約付き分散制約最適化問題の解法2009

    • 著者名/発表者名
      松井俊活, M.C.Silaghi, 平山勝敏, 横尾真, 松尾啓志
    • 雑誌名

      人工知能学会誌 24・5

      ページ: 417-427

    • 査読あり
  • [雑誌論文] 開環境での協力ゲームにおける解の簡略記述法2009

    • 著者名/発表者名
      大田直樹, 岩崎敦, 横尾真, V.Conitzer, T.Sandholm
    • 雑誌名

      情報処理学会論文誌 50・12

      ページ: 3211-3221

    • 査読あり
  • [雑誌論文] 匿名操作不可能シャプレイ値:開環境での協力ゲームへのシャプレイ値の拡張2009

    • 著者名/発表者名
      大田直樹, 佐藤恭史, 岩崎敦, 横尾真, V.Conitzer
    • 雑誌名

      コンピュータソフトウェア 26・4

      ページ: 181-196

    • 査読あり
  • [雑誌論文] Take-it-or-Leave-it 方式の再配分オークションメカニズムの提案2009

    • 著者名/発表者名
      櫻井祐子, 斎藤恭昌, 岩崎敦, 横尾真
    • 雑誌名

      電子情報通信学会論文誌 J92-D・11

      ページ: 1861-1868

    • 査読あり
  • [雑誌論文] セキュアキーワード広告オークションプロトコルの提案2009

    • 著者名/発表者名
      櫻井祐子, 横尾真, 岩崎敦, 鈴木幸太郎
    • 雑誌名

      電子情報通信学会論文誌 J92-D・11

      ページ: 1881-1889

    • 査読あり
  • [雑誌論文] 架空名義操作不可能な組合せオークションの割当規則の特性2009

    • 著者名/発表者名
      東藤大樹, 岩崎敦, 横尾真, 櫻井祐子
    • 雑誌名

      電子情報通信学会論文誌 J92-D・11

      ページ: 1890-1901

    • 査読あり
  • [雑誌論文] Adaptive Price Update in Distributed Lagrangian Relaxation Protocol2009

    • 著者名/発表者名
      K.Hirayama, T.Matsui, M.Yokoo
    • 雑誌名

      8th International Joint Conference on Autonomous Agents & Multi-Agent Systems(AAMAS-2009)

      ページ: 1033-1040

    • 査読あり
  • [雑誌論文] Directed Soft Arc Consistency in Pseudo Trees2009

    • 著者名/発表者名
      T.Matsui, M.Silaghi, K.Hirayama, M.Yokoo, H.Matsuo
    • 雑誌名

      8th International Joint Conference on Autonomous Agents & Multi-Agent Systems(AAMAS-2009)

      ページ: 1065-1072

    • 査読あり
  • [雑誌論文] Characterizing False-name-proof Allocation Rules in Combinatorial Auctions2009

    • 著者名/発表者名
      T.Todo, A.Iwasaki, M.Yokoo, Y.Sakurai
    • 雑誌名

      8th International Joint Conference on Autonomous Agents & Multi-Agent Systems(AAMAS-2009)

      ページ: 265-272

    • 査読あり
  • [雑誌論文] Characterization of Strategy-proof, Revenue Monotone Combinatorial Auction Mechanisms and Connection with False-name-proofness2009

    • 著者名/発表者名
      T.Todo, A.Iwasaki, M.Yokoo
    • 雑誌名

      Fifth Workshop on Internet & Network Economics(WINE-09)

      ページ: 561-568

    • 査読あり
  • [雑誌論文] Coalition Structure Generation Utilizing Compact Characteristic Function Representations2009

    • 著者名/発表者名
      N.Ohta, V.Conitzer, R.Ichimura, Y.Sakurai, A.Iwasaki, M.Yokoo
    • 雑誌名

      15th International Conference on Principles and Practice of Constraint Programming(CP-2009)

      ページ: 623-638

    • 査読あり
  • [雑誌論文] DCOPs Meet the Real World : Exploring Unknown Reward Matrices with Applications to Mobile Sensor Networks2009

    • 著者名/発表者名
      M.Jain, M.Taylor, M.Tambe, M.Yokoo
    • 雑誌名

      International Joint Conference on Artificial Intelligence(IJCAI-2009)

      ページ: 181-186

    • 査読あり
  • [雑誌論文] Minimal Model Generation with Respect to an Atom Set2009

    • 著者名/発表者名
      M.Koshimura, H.Nabeshima, H.Fujita, R.Hasegawa
    • 雑誌名

      7th International Workshop on First-Order Theorem Proving(FTP 2009)

      ページ: 49-59

    • 査読あり
  • [雑誌論文] A SAT-based Method for Solving the Two-dimensional Strip Packing Problem

    • 著者名/発表者名
      T.Soh, K.Inoue, N.Tamura, M.Banbara, H.Nabeshima
    • 雑誌名

      Jouranal of Algorithms in Cognition, Informatics and Logic (掲載確定)

    • 査読あり
  • [学会発表] モデル生成によるSATソルバの並列化2010

    • 著者名/発表者名
      矢野明浩
    • 学会等名
      情報処理学会創立50周年記念(第72回)全国大会
    • 発表場所
      東京大学(東京都)
    • 年月日
      2010-03-09
  • [学会発表] 共通記号を持つ背景理論の決定手続きの結合法と効率化について2010

    • 著者名/発表者名
      岩沼宏治
    • 学会等名
      電子情報通信学会ソフトウエアサイエンス研究会 技術研究報告IEICE-SS2009-67, Vol.109, No.SS-456, pp.115-120
    • 発表場所
      鹿児島大学(鹿児島県)
    • 年月日
      2010-03-08
  • [学会発表] 制約充足問題のSAT変換とグラフ彩色問題への応用2009

    • 著者名/発表者名
      丹生智也, 田村直之, 番原睦則
    • 学会等名
      日本ソフトウェア科学会第26回大会
    • 発表場所
      島根大学(島根県)
    • 年月日
      20090916-20090918
  • [学会発表] 架空名義入札に頑健な再配分メカニズムの提案2009

    • 著者名/発表者名
      櫻井祐子, V.Conitzer, 斎藤恭昌, 岩崎敦, 横尾真
    • 学会等名
      第23回人工知能学会全国大会
    • 発表場所
      サンポートホール高松(香川県)
    • 年月日
      20090617-20090619
  • [学会発表] 架空名義不可能な組合せオークションの割当規則の特性2009

    • 著者名/発表者名
      東藤大樹, 岩崎敦, 横尾真, 櫻井祐子
    • 学会等名
      第23回人工知能学会全国大会
    • 発表場所
      サンポートホール高松(香川県)
    • 年月日
      20090617-20090619
  • [学会発表] 第一価格入札における架空名義操作の影響の解析2009

    • 著者名/発表者名
      桂木敦史, 櫻井祐子, 岩崎敦, 横尾真
    • 学会等名
      第23回人工知能学会全国大会
    • 発表場所
      サンポートホール高松(香川県)
    • 年月日
      20090617-20090619
  • [学会発表] Solving Hard Combinatorial Problems with SAT Solvers2009

    • 著者名/発表者名
      Hiroshi Fujita
    • 学会等名
      Dagstuhl Seminar 09461 Algorithms and Applications for Next Generation SAT Solvers
    • 発表場所
      Schloss Dagstuhl(ドイツ)
    • 年月日
      2009-11-12
  • [学会発表] Minimal model generation with MGTP and DPLL2009

    • 著者名/発表者名
      Ryuzo Hasegawa
    • 学会等名
      Dagstuhl Seminar 09461 Algorithms and Applications for Next Generation SAT Solvers
    • 発表場所
      Schloss Dagstuhl(ドイツ)
    • 年月日
      2009-11-10
  • [学会発表] SAT変換による未解決ジョブショップスケジューリング問題への挑戦2009

    • 著者名/発表者名
      越村三幸
    • 学会等名
      スケジューリング・シンポジウム2009
    • 発表場所
      岡山大学(岡山県)
    • 年月日
      2009-09-17
  • [学会発表] SAT問題への変換を用いたフィードバックを含むパスウェイの解析2009

    • 著者名/発表者名
      宋剛秀, 井上克巳
    • 学会等名
      第23回人工知能学会全国大会
    • 発表場所
      サンポートホール高松(香川県)
    • 年月日
      2009-06-18
  • [備考]

    • URL

      http://www.edu.kobe-u.ac.jp/istc-tamlab/cspsat/

URL: 

公開日: 2011-06-16   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi