• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2009 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number 20240003
Research InstitutionKobe University

Principal Investigator

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

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

本年度は,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名を含む)だった.

  • Research Products

    (39 results)

All 2010 2009 Other

All Journal Article (28 results) (of which Peer Reviewed: 19 results) Presentation (10 results) Remarks (1 results)

  • [Journal Article] SOLAR : An Automated Deduction System for Consequence Finding2010

    • Author(s)
      H.Nabeshima, K.Iwanuma, K.Inoue.O.Ray
    • Journal Title

      AI Communications 23

      Pages: 183-203

    • Peer Reviewed
  • [Journal Article] 分散制約最適化問題へのソフトアーク整合の適用2010

    • Author(s)
      松井俊浩, M.C.Silaghi, 平山勝敏, 横尾真, 松尾啓志
    • Journal Title

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

    • Peer Reviewed
  • [Journal Article] 特集「最近のSAT技術の発展」にあたって2010

    • Author(s)
      井上克巳, 田村直之
    • Journal Title

      人工知能学会誌 25・1

      Pages: 56-56

  • [Journal Article] SATソルバーの基礎2010

    • Author(s)
      井上克巳, 田村直之
    • Journal Title

      人工知能学会誌 25・1

      Pages: 57-67

  • [Journal Article] 高速SATソルバーの原理2010

    • Author(s)
      鍋島英知, 宋剛秀
    • Journal Title

      人工知能学会誌 25・1

      Pages: 68-76

  • [Journal Article] 制約最適化問題とSAT符号化2010

    • Author(s)
      田村直之, 丹生智也, 番原睦則
    • Journal Title

      人工知能学会誌 25・1

      Pages: 77-85

  • [Journal Article] SMT:個別理論を取り扱うSAT技術2010

    • Author(s)
      岩沼宏治, 鍋島英知
    • Journal Title

      人工知能学会誌 25・1

      Pages: 86-95

  • [Journal Article] モデル列挙とモデル計数2010

    • Author(s)
      長谷川隆三, 藤田博, 越村三幸
    • Journal Title

      人工知能学会誌 25・1

      Pages: 96-104

  • [Journal Article] ★-SAT:SATの拡張2010

    • Author(s)
      平山勝敏, 横尾真
    • Journal Title

      人工知能学会誌 25・1

      Pages: 105-113

  • [Journal Article] SATによるプランニングとスケジューリング2010

    • Author(s)
      鍋島英知
    • Journal Title

      人工知能学会誌 25・1

      Pages: 114-121

  • [Journal Article] SATによるシステム検証2010

    • Author(s)
      番原睦則, 田村直之
    • Journal Title

      人工知能学会誌 25・1

      Pages: 122-129

  • [Journal Article] Compiling Finite Linear CSP into SAT2009

    • Author(s)
      N.Tamura, A.Taga, S.Kitagawa, M.Banbara
    • Journal Title

      Constraints 14・2

      Pages: 254-272

    • Peer Reviewed
  • [Journal Article] ADOPT-ing : unifying asynchronous distributed optimization with asynchronous backtracking2009

    • Author(s)
      M.C.Silaghi, M.Yokoo
    • Journal Title

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

      Pages: 89-123

    • Peer Reviewed
  • [Journal Article] Coordination Planning : Applying Control Synthesis Methods for a Class of Distributed Agents2009

    • Author(s)
      K.T.Seow, C.Ma, M.Yokoo
    • Journal Title

      IEEE Transactions on Control Systems Technology 17・2

      Pages: 405-415

    • Peer Reviewed
  • [Journal Article] 資源制約に束縛されない pseudo-tree を用いた資源制約付き分散制約最適化問題の解法2009

    • Author(s)
      松井俊活, M.C.Silaghi, 平山勝敏, 横尾真, 松尾啓志
    • Journal Title

      人工知能学会誌 24・5

      Pages: 417-427

    • Peer Reviewed
  • [Journal Article] 開環境での協力ゲームにおける解の簡略記述法2009

    • Author(s)
      大田直樹, 岩崎敦, 横尾真, V.Conitzer, T.Sandholm
    • Journal Title

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

      Pages: 3211-3221

    • Peer Reviewed
  • [Journal Article] 匿名操作不可能シャプレイ値:開環境での協力ゲームへのシャプレイ値の拡張2009

    • Author(s)
      大田直樹, 佐藤恭史, 岩崎敦, 横尾真, V.Conitzer
    • Journal Title

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

      Pages: 181-196

    • Peer Reviewed
  • [Journal Article] Take-it-or-Leave-it 方式の再配分オークションメカニズムの提案2009

    • Author(s)
      櫻井祐子, 斎藤恭昌, 岩崎敦, 横尾真
    • Journal Title

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

      Pages: 1861-1868

    • Peer Reviewed
  • [Journal Article] セキュアキーワード広告オークションプロトコルの提案2009

    • Author(s)
      櫻井祐子, 横尾真, 岩崎敦, 鈴木幸太郎
    • Journal Title

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

      Pages: 1881-1889

    • Peer Reviewed
  • [Journal Article] 架空名義操作不可能な組合せオークションの割当規則の特性2009

    • Author(s)
      東藤大樹, 岩崎敦, 横尾真, 櫻井祐子
    • Journal Title

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

      Pages: 1890-1901

    • Peer Reviewed
  • [Journal Article] Adaptive Price Update in Distributed Lagrangian Relaxation Protocol2009

    • Author(s)
      K.Hirayama, T.Matsui, M.Yokoo
    • Journal Title

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

      Pages: 1033-1040

    • Peer Reviewed
  • [Journal Article] Directed Soft Arc Consistency in Pseudo Trees2009

    • Author(s)
      T.Matsui, M.Silaghi, K.Hirayama, M.Yokoo, H.Matsuo
    • Journal Title

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

      Pages: 1065-1072

    • Peer Reviewed
  • [Journal Article] Characterizing False-name-proof Allocation Rules in Combinatorial Auctions2009

    • Author(s)
      T.Todo, A.Iwasaki, M.Yokoo, Y.Sakurai
    • Journal Title

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

      Pages: 265-272

    • Peer Reviewed
  • [Journal Article] Characterization of Strategy-proof, Revenue Monotone Combinatorial Auction Mechanisms and Connection with False-name-proofness2009

    • Author(s)
      T.Todo, A.Iwasaki, M.Yokoo
    • Journal Title

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

      Pages: 561-568

    • Peer Reviewed
  • [Journal Article] Coalition Structure Generation Utilizing Compact Characteristic Function Representations2009

    • Author(s)
      N.Ohta, V.Conitzer, R.Ichimura, Y.Sakurai, A.Iwasaki, M.Yokoo
    • Journal Title

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

      Pages: 623-638

    • Peer Reviewed
  • [Journal Article] DCOPs Meet the Real World : Exploring Unknown Reward Matrices with Applications to Mobile Sensor Networks2009

    • Author(s)
      M.Jain, M.Taylor, M.Tambe, M.Yokoo
    • Journal Title

      International Joint Conference on Artificial Intelligence(IJCAI-2009)

      Pages: 181-186

    • Peer Reviewed
  • [Journal Article] Minimal Model Generation with Respect to an Atom Set2009

    • Author(s)
      M.Koshimura, H.Nabeshima, H.Fujita, R.Hasegawa
    • Journal Title

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

      Pages: 49-59

    • Peer Reviewed
  • [Journal Article] A SAT-based Method for Solving the Two-dimensional Strip Packing Problem

    • Author(s)
      T.Soh, K.Inoue, N.Tamura, M.Banbara, H.Nabeshima
    • Journal Title

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

    • Peer Reviewed
  • [Presentation] モデル生成によるSATソルバの並列化2010

    • Author(s)
      矢野明浩
    • Organizer
      情報処理学会創立50周年記念(第72回)全国大会
    • Place of Presentation
      東京大学(東京都)
    • Year and Date
      2010-03-09
  • [Presentation] 共通記号を持つ背景理論の決定手続きの結合法と効率化について2010

    • Author(s)
      岩沼宏治
    • Organizer
      電子情報通信学会ソフトウエアサイエンス研究会 技術研究報告IEICE-SS2009-67, Vol.109, No.SS-456, pp.115-120
    • Place of Presentation
      鹿児島大学(鹿児島県)
    • Year and Date
      2010-03-08
  • [Presentation] 制約充足問題のSAT変換とグラフ彩色問題への応用2009

    • Author(s)
      丹生智也, 田村直之, 番原睦則
    • Organizer
      日本ソフトウェア科学会第26回大会
    • Place of Presentation
      島根大学(島根県)
    • Year and Date
      20090916-20090918
  • [Presentation] 架空名義入札に頑健な再配分メカニズムの提案2009

    • Author(s)
      櫻井祐子, V.Conitzer, 斎藤恭昌, 岩崎敦, 横尾真
    • Organizer
      第23回人工知能学会全国大会
    • Place of Presentation
      サンポートホール高松(香川県)
    • Year and Date
      20090617-20090619
  • [Presentation] 架空名義不可能な組合せオークションの割当規則の特性2009

    • Author(s)
      東藤大樹, 岩崎敦, 横尾真, 櫻井祐子
    • Organizer
      第23回人工知能学会全国大会
    • Place of Presentation
      サンポートホール高松(香川県)
    • Year and Date
      20090617-20090619
  • [Presentation] 第一価格入札における架空名義操作の影響の解析2009

    • Author(s)
      桂木敦史, 櫻井祐子, 岩崎敦, 横尾真
    • Organizer
      第23回人工知能学会全国大会
    • Place of Presentation
      サンポートホール高松(香川県)
    • Year and Date
      20090617-20090619
  • [Presentation] Solving Hard Combinatorial Problems with SAT Solvers2009

    • Author(s)
      Hiroshi Fujita
    • Organizer
      Dagstuhl Seminar 09461 Algorithms and Applications for Next Generation SAT Solvers
    • Place of Presentation
      Schloss Dagstuhl(ドイツ)
    • Year and Date
      2009-11-12
  • [Presentation] Minimal model generation with MGTP and DPLL2009

    • Author(s)
      Ryuzo Hasegawa
    • Organizer
      Dagstuhl Seminar 09461 Algorithms and Applications for Next Generation SAT Solvers
    • Place of Presentation
      Schloss Dagstuhl(ドイツ)
    • Year and Date
      2009-11-10
  • [Presentation] SAT変換による未解決ジョブショップスケジューリング問題への挑戦2009

    • Author(s)
      越村三幸
    • Organizer
      スケジューリング・シンポジウム2009
    • Place of Presentation
      岡山大学(岡山県)
    • Year and Date
      2009-09-17
  • [Presentation] SAT問題への変換を用いたフィードバックを含むパスウェイの解析2009

    • Author(s)
      宋剛秀, 井上克巳
    • Organizer
      第23回人工知能学会全国大会
    • Place of Presentation
      サンポートホール高松(香川県)
    • Year and Date
      2009-06-18
  • [Remarks]

    • URL

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

URL: 

Published: 2011-06-16   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi