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

2011 年度 実績報告書

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

研究課題

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

研究代表者

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

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

最終年度として研究開発を行い,33件の学会誌論文・国際会議論文(うち査読付論文32件,ベストペーパー2件)の公表,18件の学会発表(うちベストペーパー1件)を行った.
特筆すべき研究開発成果としては以下のものが挙げられる,(1)SATソルバーGlueMiniSatが,SAT2011競技会の逐次型ソルバートラックのApplication部門においてUNSATクラスで1位,SAT+UNSATクラスで2位,さらに並列型ソルバートラックのApplication部門UNSATクラスで2位を獲得という非常に優秀な成績を収めた.(2)MaxSATソルバーQMaxSATが,MaxSAT Evaluation 2011のPartial MaxSAT部門において前年に引き続きIndustrialで1位,Craftedで2位という優れた成績を収めた.
その他,以下の研究を進めた:CSPのコンパクトかつ効率的な新しいSAT符号化;値変更コスト付き動的SATおよび動的CSPの解法;複数の背景理論を持つSMTへの部分評価法の導入;分散CSPの応用としての提携構造形成問題とメカニズムデザイン;SATソルバーにおける局所対称性除去手法;極小モデル生成器MiniMGの高速化手法;SAT技術の釣合い型不完備ブロック計画構成問題への応用;擬似ブールソルバーを応用した部分MaxSATソルバーの開発;SATソルバーを利用した極小モデル生成器を用いた代謝パスウェイの解析;GlueMiniSatの技術を応用した並列SATソルバーの開発;セマフォを利用した並列SATソルバーの開発.
また,全研究者の参加するCSPSAT研究会を3回,CSPSAT講演会を1回開催し(参加者数のべ93名),第25回人工知能学会全国大会のオーガナイズドセッションrSAT技術の理論,実装,応用」を企画した.

  • 研究成果

    (52件)

すべて 2012 2011 その他

すべて 雑誌論文 (33件) (うち査読あり 32件) 学会発表 (18件) 備考 (1件)

  • [雑誌論文] Scala上の制約プログラミング用ドメイン特化言語Coprisについて2012

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

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

    • 査読あり
  • [雑誌論文] SAT符号化を用いた釣合い型不完備ブロック計画の構成2012

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

      人工知能学会論文誌

      巻: 27巻2号 ページ: 10-15

    • DOI

      10.1527/tjsai.27.10

    • 査読あり
  • [雑誌論文] 私のブックマーク:SATソルバー2012

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

      人工知能学会誌

      巻: (掲載決定)

  • [雑誌論文] QMaxSAT : A Partial Max-SAT Solver2012

    • 著者名/発表者名
      Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, Ryuzo Hasegawa
    • 雑誌名

      Journal on Satisfiability, Boolean Modeling and Computation

      巻: 8 ページ: 95-100

    • 査読あり
  • [雑誌論文] GlueMiniSat2.2.5:単位伝搬を促す学習節の積極的獲得戦略に基づく高速SATソルバー2012

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

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

      巻: (掲載決定)

    • 査読あり
  • [雑誌論文] 値変更コスト付き動的SATの定式化とその解法2011

    • 著者名/発表者名
      波多野大督, 平山勝敏
    • 雑誌名

      人工知能学会論文誌

      巻: 26巻, 6号 ページ: 682-691

    • 査読あり
  • [雑誌論文] 擬似木に基づく分散制約最適化問題の精度保証付き非厳密解法の提案2011

    • 著者名/発表者名
      沖本天太, ジョヨンジュン, 岩崎敦, 横尾真
    • 雑誌名

      情報処理学会論文誌

      巻: 52巻, 12号 ページ: 3786-3795

    • 査読あり
  • [雑誌論文] 分散制約充足問題:特定の制約網に特化した変数順序付けヒューリスティックの提案2011

    • 著者名/発表者名
      沖本天太, 岩崎敦, 横尾真
    • 雑誌名

      情報処理学会論文誌

      巻: 52(4) ページ: 3018-3029

    • 査読あり
  • [雑誌論文] 架空名義操作不可能な施設配置メカニズムの特徴付け2011

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

      情報処理学会論文誌

      巻: 52(4) ページ: 1657-1666

    • 査読あり
  • [雑誌論文] モンテカルロゲーム木探索に基づく限量記号付き制約充足問題の実時間解決2011

    • 著者名/発表者名
      馬場里美, 岩崎敦, 横尾真
    • 雑誌名

      電子情報通信学会論文誌

      巻: Vol.J94-D No.11 ページ: 1729-1739

    • 査読あり
  • [雑誌論文] 協力ゲームにおける特性関数のエージェントのタイプに基づく簡略表記法2011

    • 著者名/発表者名
      上田俊, 北木真, 岩崎敦, 横尾真
    • 雑誌名

      電子情報通信学会論文誌

      巻: Vol.J94-D No.11 ページ: 1716-1728

    • 査読あり
  • [雑誌論文] MC-netsを用いた提携構造形成アルゴリズムの拡張:負の利得と外部性の導入2011

    • 著者名/発表者名
      一村良, 長谷川隆人, 上田俊, 岩崎敦, 横尾真
    • 雑誌名

      電子情報通信学会論文誌

      巻: Vol.J94-D No.11 ページ: 1707-1715

    • 査読あり
  • [雑誌論文] Distributed on-Line Multi-Agent Optimization under Uncertainty : Balancing Exploration and Exploitation2011

    • 著者名/発表者名
      Matthew E.Taylor, Manish Jain, Prateek Tandon, Makoto Yokoo, Milind Tambe
    • 雑誌名

      Advances in Complex Systems

      巻: 14(3) ページ: 471-528

    • DOI

      10.1142/S0219525911003104

    • 査読あり
  • [雑誌論文] Dynamic SAT with Decision Change Costs : Formalization and Solutions2011

    • 著者名/発表者名
      Daisuke Hatano, Katsutoshi Hirayama
    • 雑誌名

      Proc.of 22nd Int'l Joint Conf.on Artificial Intelligence (IJCAI 2011)

      ページ: 560-565

    • DOI

      10.5591/978-1-57735-516-8/IJCAI11-101

    • 査読あり
  • [雑誌論文] A Compact and Efficient SAT-Encoding of Finite Domain CSP2011

    • 著者名/発表者名
      Tomoya Tanjo, Naoyuki Tamura, Mutsunori Banbara
    • 雑誌名

      Proc.of 14th Int'l Conf.on Theory and Applications of Satisfiability Testing (SAT 2011)

      ページ: 375-376

    • DOI

      10.1007/978-3-642-21581-0_36

    • 査読あり
  • [雑誌論文] Proposal of a compact and efficient SAT encoding using a numeral system of any base2011

    • 著者名/発表者名
      Tomoya Tanjo, Naoyuki Tamura, Mutsunori Banbara
    • 雑誌名

      Proc.of 1st Int'l Workshop on the Cross-Fertilization Between CSP and SAT (CSPSAT 2011)

    • 査読あり
  • [雑誌論文] QMaxSAT version 0.3 & 0.42011

    • 著者名/発表者名
      Xuanye An, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
    • 雑誌名

      Proc.of 8th Int'l Workshop on First-Order Theorem Proving (FTP 2011)

      ページ: 7-15

    • 査読あり
  • [雑誌論文] Combining PSO and Local Search to Solve Scheduling Problems2011

    • 著者名/発表者名
      Xue-Feng Zhang, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
    • 雑誌名

      Proc.of 13th Annual Conf.Companion on Genetic and Evolutionary Computation (GECCO 2011)

      ページ: 347-354

    • DOI

      10.1145/2001858.2002017

    • 査読あり
  • [雑誌論文] Query-driven Coordination of Multiple Answer Sets2011

    • 著者名/発表者名
      Gauvain Bourgne, Katsumi Inoue
    • 雑誌名

      Proc.of 86h Int'l Workshop on Declarative Agent Languages and Technologies VIII (DALT 2010)

      ページ: 40-59

    • DOI

      10.1007/978-3-642-20715-0_3

    • 査読あり
  • [雑誌論文] Probabilistic Rule Learning in Nonmonotonic Domains2011

    • 著者名/発表者名
      Domenico Corapi, Daniel Sykes, Katsumi Inoue, Alessandra Russo
    • 雑誌名

      Proc.of 12th Int'l Workshop on the Computational Logic in Multi-Agent Systems (CLIMA-XII)

      ページ: 243-258

    • DOI

      10.1007/978-3-642-22359-4_17

    • 査読あり
  • [雑誌論文] Answer-Set Programming as a New Approach to Event-Sequence Testing2011

    • 著者名/発表者名
      Esra Erdem, Katsumi Inoue, Johannes Oetsch, Jorg Puhrer, Hans Tompits, Cemal Yilmaz
    • 雑誌名

      Proc.of 3rd Int'l Conf.on Advances in System Testing and Validation Lifecycle (VALID 2011)

      ページ: 25-34

    • 査読あり
  • [雑誌論文] Logic Programming for Boolean Networks2011

    • 著者名/発表者名
      Katsumi Inoue
    • 雑誌名

      Proc.of 22nd Int'l Joint Conf.on Artificial Intelligence (IJCAI 2011)

      ページ: 924-930

    • DOI

      10.5591/978-1-57735-516-8/IJCAI11-160

    • 査読あり
  • [雑誌論文] Confidentiality-Preserving Data Publishing for Credulous Users by Extended Abduction2011

    • 著者名/発表者名
      Katsumi Inoue, Chiaki Sakama, Lena Wiese
    • 雑誌名

      Proc.of 19th Int'l Conf.on Applications of Declarative Programming and Knowledge Management (INAP 2011)

    • 査読あり
  • [雑誌論文] Analyzing Pathways Using ASP-Based Approaches2011

    • 著者名/発表者名
      Oliver Ray, Takehide Soh, Katsumi Inoue
    • 雑誌名

      Proc of 2010 Int'l Conf.on Algebraic and Numeric Biology (ANB 2010)

      ページ: 167-183

    • DOI

      10.1007/978-3-642-28067-2_10

    • 査読あり
  • [雑誌論文] A Compact Representation Scheme of Coalitional Games Based on Multi-Terminal Zero-Suppressed Binary Decision Diagrams (Best Paper Award)2011

    • 著者名/発表者名
      Yuko Sakurai, Suguru Ueda, Atsushi Iwasaki, Shin-ichi Minato, Makoto Yokoo
    • 雑誌名

      Proc.of 14th Int'l Conf.on Principles and Practice of Multiagent Systems (PRIMA 2011)

      ページ: 4-18

    • DOI

      10.1007/978-3-642-25044-6_4

    • 査読あり
  • [雑誌論文] The Design of Cryptographic Substitution Boxes using CSPs (Best Application Paper Award)2011

    • 著者名/発表者名
      Venkatesh Ramamoorthy, Marius Silaghi, Toshihiro Matsui, Katsutoshi Hirayama Makoto Yokoo
    • 雑誌名

      Proc.of 17th Int'l Conf.on Principles and Practice of Constraint Programming (CP 2011)

      ページ: 54-68

    • DOI

      10.1007/978-3-642-23786-7_7

    • 査読あり
  • [雑誌論文] Reducing the Search Space of Resource Constrained DCOPs2011

    • 著者名/発表者名
      Toshihiro Matsui, Marius Silaghi, Katsutoshi Hirayama, Makoto Yokoo, Boi Faltings, Hiroshi Matsuo
    • 雑誌名

      Proc.of 17th Int'l Conf.on Principles and Practice of Constraint Programming (CP 2011)

      ページ: 576-590

    • DOI

      10.1007/978-3-642-23786-7_44

    • 査読あり
  • [雑誌論文] Pseudeo-Tree-Based Incomplete Algorithm for Distributed Constraint Optimization with Quality Bounds2011

    • 著者名/発表者名
      Tenda Okimoto, Yongjoon Joe, Atsushi Iwasaki, Makoto Yokoo, Boi Faltings
    • 雑誌名

      Proc.of 17th Int'l Conf.on Principles and Practice of Constraint Programming (CP 2011)

      ページ: 660-674

    • DOI

      10.1007/978-3-642-23786-7_50

    • 査読あり
  • [雑誌論文] Generalizing Envy-Freeness toward Group of Agents2011

    • 著者名/発表者名
      Taiki Todo, Runcong Li, Xuemei Hu, Takayuki Mouri, Atsushi Iwasaki, Makoto Yokoo
    • 雑誌名

      Proc.of 22nd Int'l Joint Conf.on Artificial Intelligence (IJCAI 2011)

      ページ: 386-392

    • DOI

      10.5591/978-1-57735-516-8/IJCAI11-073

    • 査読あり
  • [雑誌論文] Concise Characteristic Function Representations in Coalitional Games Based on Agent Types2011

    • 著者名/発表者名
      Suguru Ueda, Makoto Kitaki, Atsushi Iwasaki, Makoto Yokoo
    • 雑誌名

      Proc.of 22nd Int'l Joint Conf.on Artificial Intelligence (IJCAI 2011)

      ページ: 393-399

    • DOI

      10.5591/978-1-57735-516-8/IJCAI11-074

    • 査読あり
  • [雑誌論文] Real-Time Solving of Quantified CSPs Based on Monte-Carlo Game Tree Search2011

    • 著者名/発表者名
      Satomi Baba, Yongjoon Joe, Atsushi Iwasaki, Makoto Yokoo
    • 雑誌名

      Proc.of 22nd Int'l Joint Conf.on Artificial Intelligence (IJCAI 2011)

      ページ: 655-661

    • DOI

      10.5591/978-1-57735-516-8/IJCAI11-116

    • 査読あり
  • [雑誌論文] False-name bidding in first-price combinatorial aucitons with incomplete information2011

    • 著者名/発表者名
      Atsushi Iwasaki, Atsushi Katsuragi, Makoto Yokoo
    • 雑誌名

      Proc.of 10th Int'l Conf.on Autonomous Agents and Multiagent Systems (AAMAS 2011)

      ページ: 541-548

    • 査読あり
  • [雑誌論文] False-name-proof Mechanism Design without Money2011

    • 著者名/発表者名
      Taiki Todo, Atsushi Iwasaki, Makoto Yokoo
    • 雑誌名

      Proc.of 10th Int'l Conf.on Autonomous Agents and Multiagent Systems (AAMAS 2011)

      ページ: 651-658

    • 査読あり
  • [学会発表] Azucar:コンパクト順序符号化を用いたSAT型制約ソルバー2012

    • 著者名/発表者名
      丹生智也, 田村直之, 番原睦則,
    • 学会等名
      第14回プログラミングおよびプログラミング言語ワークショップ(PPL 2012)
    • 発表場所
      むさし(和歌山県)
    • 年月日
      2012-03-08
  • [学会発表] 充足可能性判定器に基づく命題論理の結論発見器の提案2012

    • 著者名/発表者名
      鈴木健士郎, 鍋島英知, 岩沼宏治
    • 学会等名
      人工知能学会第85回人工知能基本問題研究会
    • 発表場所
      下呂交流会館(岐阜県)
    • 年月日
      2012-02-03
  • [学会発表] SATソルバーの探索戦略効率化に向けた合理的尺度の導入検証2012

    • 著者名/発表者名
      村松匠, 鍋島英知
    • 学会等名
      人工知能学会第85回人工知能基本問題研究会
    • 発表場所
      下呂交流会館(岐阜県)
    • 年月日
      2012-02-03
  • [学会発表] 局所対称性除去によるCDCLソルバーの効率改善に向けて2011

    • 著者名/発表者名
      金澤潤二, 鍋島英知
    • 学会等名
      人工知能学会第84回人工知能基本問題研究会
    • 発表場所
      慶応義塾大学(神奈川県)
    • 年月日
      2011-12-16
  • [学会発表] SAT型制約ソルバーSugarとScalaインターフェイスについて2011

    • 著者名/発表者名
      田村直之, 丹生智也, 番原睦則
    • 学会等名
      日本ソフトウェア科学会第28回大会
    • 発表場所
      沖縄産業支援センター(沖縄県)
    • 年月日
      2011-09-29
  • [学会発表] QMaxSAT:部分MaxSATソルバーの簡便な一実装2011

    • 著者名/発表者名
      越村三幸, 安宣〓, 藤田博, 長谷川隆三
    • 学会等名
      日本ソフトウェア科学会第28回大会
    • 発表場所
      沖縄産業支援センター(沖縄県)
    • 年月日
      2011-09-29
  • [学会発表] GlueMiniSat2.2.5:単位伝搬を促す学習節の積極的獲得戦略に基づく高速SATソルバー2011

    • 著者名/発表者名
      鍋島英知, 岩沼宏治, 井上克巳
    • 学会等名
      日本ソフトウェア科学会第28回大会
    • 発表場所
      沖縄産業支援センター(沖縄県)
    • 年月日
      2011-09-29
  • [学会発表] 位取り記数法に基づく整数有限領域上の制約充足問題のコンパクトかつ効率的なSAT符号化2011

    • 著者名/発表者名
      丹生智也, 田村直之, 番原睦則
    • 学会等名
      日本ソフトウェア科学会第28回大会
    • 発表場所
      沖縄産業支援センター(沖縄県)
    • 年月日
      2011-09-27
  • [学会発表] UNIXのFORK機能に基づくSATソルバーの並列化2011

    • 著者名/発表者名
      明石裕子, 越村三幸, 藤田博, 長谷川隆三
    • 学会等名
      日本ソフトウェア科学会第28回大会
    • 発表場所
      沖縄産業支援センター(沖縄県)
    • 年月日
      2011-09-27
  • [学会発表] 局所対称性除去によるCDCLソルバーの効率化手法の検討2011

    • 著者名/発表者名
      金澤潤二, 鍋島英知
    • 学会等名
      日本ソフトウェア科学会第28回大会
    • 発表場所
      沖縄産業支援センター(沖縄県)
    • 年月日
      2011-09-27
  • [学会発表] 自動メカニズムデザインを利用した組合せオークションのルール抽出アルゴリズムの提案2011

    • 著者名/発表者名
      毛利貴之, 杉町勇和, 東藤大樹, 岩崎敦, 横尾真
    • 学会等名
      第10回情報科学技術フォーラム(FIT 2011)
    • 発表場所
      函館大学(北海道)
    • 年月日
      2011-09-07
  • [学会発表] 値変更コスト付き動的CSPの定式化とその解法2011

    • 著者名/発表者名
      波多野大督, 平山勝敏
    • 学会等名
      2011年度人工知能学会全国大会(JSAI 2011)
    • 発表場所
      いわて県民情報交流センター(岩手県)
    • 年月日
      2011-06-03
  • [学会発表] SAT符号化を用いた釣合い型不完備ブロック計画の構成2011

    • 著者名/発表者名
      松中春樹, 丹生智也, 番原睦則, 田村直之
    • 学会等名
      2011年度人工知能学会全国大会(JSAI 2011)
    • 発表場所
      いわて県民情報交流センター(岩手県)
    • 年月日
      2011-06-03
  • [学会発表] 整数有限領域上の制約充足問題のコンパクトかつ効率的なSAT符号化2011

    • 著者名/発表者名
      丹生智也, 田村直之, 番原睦則
    • 学会等名
      2011年度人工知能学会全国大会(JSAI 2011)
    • 発表場所
      いわて県民情報交流センター(岩手県)
    • 年月日
      2011-06-03
  • [学会発表] SOLタブロー計算法に基づく命題論理の充足可能性判定器の実現2011

    • 著者名/発表者名
      鈴木健士郎, 鍋島英知
    • 学会等名
      2011年度人工知能学会全国大会(JSAI 2011)
    • 発表場所
      いわて県民情報交流センター(岩手県)
    • 年月日
      2011-06-03
  • [学会発表] 一般双対化問題における冗長節生成の抑止法とその評価2011

    • 著者名/発表者名
      山本泰生, 鍋島英知, 岩沼宏治
    • 学会等名
      2011年度人工知能学会全国大会(JSAI 2011)
    • 発表場所
      いわて県民情報交流センター(岩手県)
    • 年月日
      2011-06-03
  • [学会発表] Nelson-Oppen法を組み込んだSMTソルバの設計2011

    • 著者名/発表者名
      福田寿志, 岩沼宏治, 山本泰生
    • 学会等名
      2011年度人工知能学会全国大会(JSAI 2011)
    • 発表場所
      いわて県民情報交流センター(岩手県)
    • 年月日
      2011-06-03
  • [学会発表] QMaxSAT : Q-dai MaxSATソルバー2011

    • 著者名/発表者名
      越村三幸
    • 学会等名
      2011年度人工知能学会全国大会(JSAI 2011)
    • 発表場所
      いわて県民情報交流センター(岩手県)
    • 年月日
      2011-06-03
  • [備考]

    • URL

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

URL: 

公開日: 2013-06-26  

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

Powered by NII kakenhi