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

2012 年度 実績報告書

命題論理の推論技術を用いた高性能かつ柔軟な制約プログラミングシステムの実現

研究課題

研究課題/領域番号 24300007
研究種目

基盤研究(B)

研究機関神戸大学

研究代表者

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

研究分担者 番原 睦則  神戸大学, 情報基盤センター, 准教授 (80290774)
宋 剛秀  神戸大学, 情報基盤センター, 助教 (00625121)
井上 克巳  国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321)
鍋島 英知  山梨大学, 医学工学総合研究部, 准教授 (10334848)
研究期間 (年度) 2012-04-01 – 2015-03-31
キーワード制約プログラミング / 充足可能性判定問題 / 命題論理
研究概要

命題論理の推論技術を用いた高性能かつ柔軟な制約プログラミングシステムの実現に関する研究開発を行い,18件の学会誌論文・国際会議論文の公表,14件の学会発表を行った.また,設定した各研究テーマに関しては以下の研究開発成果を得た.
A.フレキシブル制約に関する研究開発:フレキシブル制約の一種である重み付きソフト制約についていて,それらを擬似ブール制約に一旦符号化し,さらに命題論理の充足可能性判定問題(SAT)に符号化する方法について研究開発を行った.特に擬似ブール制約をSAT符号化するシステムとしてPBSugarを開発した.また,多目的制約最適化問題に関する研究を行った.
B.動的な制約変更に関する研究開発 : 制約充足問題(CSP)をSATに符号化し求解するシステムとしてCoprisおよびScarabを開発し,それらのシステム上で動的に制約変更を可能にする方法について研究開発を行った.また,本研究チームで開発しているGlueMiniSatについて,求解中に動的に制約を簡単化する軽量な手法について検討し,評価を行った.
C.ドメイン拡張に関する研究開発:多倍長整数をSAT符号化できるシステムとしてAzucarの研究開発を行った.また記号ドメインへの拡張として解集合プログラミング(ASP)に着目し,ASP上での制約記述とその符号化について研究を開始した.
D.応用研究開発 : システム生物学への応用として,遺伝子制御やシグナル伝達のネットワークの離散モデルであるブーリアンネットワークを取り上げ,論理プログラミング意味論による動的遷移およびアトラクターの解析を行った.また,時間割問題への応用研究を開始した.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

当初の計画で設定した各研究テーマに関し研究開発を進め,18件の学会誌論文・国際会議論文の公表,14件の学会発表を行った.また,GlueMiniSat, PBSugar, Copris, Scarab, Azucar等のソフトウェアを開発し公開している.以上の点から研究はおおむね順調に進展していると判断した.

今後の研究の推進方策

当初の計画に従い,設定した以下の各研究テーマに関する研究開発を進める.A.フレキシブル制約に関する研究開発:ソフト制約のSAT符号化.B.動的な制約変更に関する研究開発:ScarabとSat4jの連携による動的な制約変更への対応。C.ドメイン拡張に関する研究開発:ASP上の制約プログラミングの実現.D.応用研究開発:システム生物学,時間割問題への応用.

次年度の研究費の使用計画

応用研究の問題を実行する計算サーバーの導入を予定していたが,導入しなかった直接経費次年度使用額が生じた.平成25年度に同様の計算サーバーの導入を計画している.

研究成果

(33件)

すべて 2013 2012 その他

すべて 雑誌論文 学会発表 備考

  • [雑誌論文] 直観主義線形論理型言語LLPとそのコンパイラ処理系2013

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

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

      巻: 30 ページ: 83-89

    • 査読あり
  • [雑誌論文] 多目的制約最適化問題における対話型解法の提案2013

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

      人工知能学会論文誌

      巻: 28(1) ページ: 57-66

    • 査読あり
  • [雑誌論文] 位取り記数法に基づく整数有限傾域上の制約充足問題のコンパクトかつ効率的なSAT符号化2013

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

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

      巻: 30(1) ページ: 211-230

    • DOI

      10.11309/jssst.30.1.211

    • 査読あり
  • [雑誌論文] Scarab : A Rapid Prototyping Tool for SAT-based Constraint Programming Systems (Tool Paper)2013

    • 著者名/発表者名
      Takehide Soh, Naoyuki Tamura, Mutsunori Banbara
    • 雑誌名

      Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), LNCS, Springer

      巻: 掲載確定(掲載確定)

    • 査読あり
  • [雑誌論文] Non-Monotone Dualization via Monotone Duanzation2013

    • 著者名/発表者名
      Yoshitaka Yamamoto, Koji Iwanuma, Katsumi Inoue
    • 雑誌名

      The 22nd International Conference of Inductive Logic Programming (ILP 2013)

      巻: 掲載確定(掲載確定)

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

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

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

      巻: 29(4) ページ: 114-129

    • DOI

      10.11309/jssst.29.4.114

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

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

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

      巻: 29(4) ページ: 146-160

    • DOI

      10.11309/jssst.29.4.146

    • 査読あり
  • [雑誌論文] Event-Sequence Testing-Using Answer-Set Programming2012

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

      International Journal On Advances in Software

      巻: 5(3-4) ページ: 236-250

    • 査読あり
  • [雑誌論文] Evaluation of the Prediction of Gene Knockout Effects by Minimal Pathway Enumeration2012

    • 著者名/発表者名
      Takehide Soh, Katsumi Inoue, Tomoya Baba, Toyoyuki Takada, Toshihiko Shiroishi
    • 雑誌名

      International Journal on Advances in Life Sciences

      巻: 4(3-4) ページ: 154-165

    • 査読あり
  • [雑誌論文] Oscillating Behavior of Logic Programs2012

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

      Correct Reasoning-Essays on Logic-Based AI in Honour of Vladimir Lifschitz, LNCS, Springer

      巻: 7265 ページ: 345-362

    • DOI

      10.1007/978-3-642-30743-0

    • 査読あり
  • [雑誌論文] DNF Hypotheses In Bottom-Directed ILP2012

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

      Inducive Logic Programming: Revised Selected Papers from the 21st International Conference (ILP 2011), LNCS, Springer

      巻: 7207 ページ: 173-188

    • DOI

      10.1007/978-3-642-31951-8

    • 査読あり
  • [雑誌論文] Concretizing the Process Hitting into Biological Regulatory Networks2012

    • 著者名/発表者名
      Maxime Folscnette, Loic Pauleve, Katsumi Inoue, Morgan Magnin, Olivier Boux
    • 雑誌名

      The 10th International Conference on Computational Methods in Systems Biology (CMSB 2012), LNCS, Springer

      巻: 7605 ページ: 166-186

    • DOI

      10.1007/978-3-642-33636-2.11

    • 査読あり
  • [雑誌論文] Abducing Biological Regulatory Networks from Process Hitting Models2012

    • 著者名/発表者名
      Maxime Folscnette, Loic Pauleve, Katsumi Inoue, Magnin, Olivier Roux
    • 雑誌名

      ECML-PKDD 2012 Workshop on Learning and Discovery in Symbolic Systems Biology

      ページ: 24-35

    • 査読あり
  • [雑誌論文] Modular Reasoning in Multi-Agent Systems Using Mata-Knowledge and Answer Set Programming2012

    • 著者名/発表者名
      Tony Kibeiro, Katsumi Inoue, Uauvain Bourgne.
    • 雑誌名

      International Joint Agent Workshop and Symposium(iJAWS 2012)

    • 査読あり
  • [雑誌論文] Generating Event-Sequence Test Cases by Answer Set Programming with Incidence Matrix2012

    • 著者名/発表者名
      Mutsunori Banbara, Naoyuki Tamura、Katsumi Inoue
    • 雑誌名

      The 28th International Conference on Logic Programmimg(ICLP 2012)

      ページ: 86-97

    • DOI

      10.4230/LIPics.ICLP.2012.86

    • 査読あり
  • [雑誌論文] On the Neighborhood and Distance Between Qualitative Spatio-Temporal Configurations2012

    • 著者名/発表者名
      Dominique D'Almeida, Mouny Samy Modeliar, Nicolas Schwind
    • 雑誌名

      The International Workshop on Spatio-Temporal Dynamics (STeDy'12)

      ページ: 53-60

    • 査読あり
  • [雑誌論文] Azucar: A SAT-Based CSP Solver Using Compact Order Encoding2012

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

      The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012), LNCS, Springer

      巻: 7317 ページ: 456-462

    • 査読あり
  • [雑誌論文] Interactive Algorithm for Multi-Objective Constraint Optimization2012

    • 著者名/発表者名
      Tenda Okimoto, Yongjoon Joe, Atsushi Iwasaki, Toshihiro Matsui, Katsutoshi Hirayama, Makoto Yokoo
    • 雑誌名

      The 18th International Conference on Principles and Practice of Constraint Programming (CP 2012), LNCS, Springer.

      巻: 7514 ページ: 561-576

    • DOI

      10.1007/978-3-642-33558-7_41

    • 査読あり
  • [学会発表] SAT符号化を用いたパッキング配列の構成2013

    • 著者名/発表者名
      則武治樹,番原睦則、宋剛秀,田村直之,井上克巳
    • 学会等名
      第15回プログラミングおよびプログラミング言語ワークショップ(PPL 2013)
    • 発表場所
      会津若松市(福島県)
    • 年月日
      2013-03-05
  • [学会発表] Scarab: Scala上で実現されたSAT型制約プログラミングシステムのための高速開発ツール2013

    • 著者名/発表者名
      宋剛秀,田村直之,番原睦則
    • 学会等名
      第15回プログラミングおよびプログラミング言語ワークショップ(PPL 2013)
    • 発表場所
      会津若松市(福島県)
    • 年月日
      2013-03-05
  • [学会発表] Generating Event-Sequence Test Cass by Constraint Programming and Answer Set Programming2012

    • 著者名/発表者名
      Mutsunori Banbara, Naoyuki Tamura, Katsumi Inoue, Hidetomo Nabeshima
    • 学会等名
      The 2012 CRIL-Nil Collaborative Meeting on Reasoning about Dynamic Constraint Networks
    • 発表場所
      Universite d'Artois(France)
    • 年月日
      2012-11-23
  • [学会発表] Specific Language Copris for Constraint Programming in Scala2012

    • 著者名/発表者名
      Naoyuki Tamura, Tomoya Tanjo, Mutsunori Banbara
    • 学会等名
      The 2012 CRIL-Nil Collaborative Meeting on Reasoning about Dynamic Constraint Networks
    • 発表場所
      Universite d'Artois(France)
    • 年月日
      2012-11-23
  • [学会発表] Towards In Crelnental SAT-based CSP Solving: experimental Results for the Hamiltonian Cycle Problem2012

    • 著者名/発表者名
      Takehlde Soh, Funakoshi Taisuke, Naoyuki Tamura, Mutsunori Banhara.
    • 学会等名
      The 2012 CRIL-Nil Collaborative Meeting on Reasoning about Dynamic Constraint Networks
    • 発表場所
      Universite d'Artois(France)
    • 年月日
      2012-11-23
  • [学会発表] 多目的分散制約最適化問題における厳密/非厳密解法の提案2012

    • 著者名/発表者名
      沖本天太, Yongjoon Joe, 上田俊,岩崎敦、櫻井祐子、横尾真、井上克己
    • 学会等名
      合同エージェントワークショップ&シンポジウム(JAWS2012)
    • 発表場所
      掛川市(静岡県)
    • 年月日
      2012-10-26
  • [学会発表] BnB-ADOPTp:分散制約最適化問題におけるハイブリッド型の解法の提案2012

    • 著者名/発表者名
      沖本天太,山本将,櫻井佑子,横尾真,井上克巳
    • 学会等名
      合同エージェントワークショップ&シンポジウム(JAWS2012)
    • 発表場所
      掛川市(静岡県)
    • 年月日
      2012-10-26
  • [学会発表] 多目的制約最適化問題:ユーザとの対話型解法の提案2012

    • 著者名/発表者名
      沖本天太, Yongjoon Joe, 岩崎敦, 横尾真
    • 学会等名
      第11回情報科学技術フォーラム(FIT2012)
    • 発表場所
      法政大学(東京都)
    • 年月日
      2012-09-06
  • [学会発表] (学生奨励賞受賞)カリキュラムベースのコース時間罰問題の擬似プール最適化問題への符号化2012

    • 著者名/発表者名
      鈴江美奈,田村直之,番原睦則,宋剛秀,鳩野逸生
    • 学会等名
      日本ソフトウェア科学会第29回大会
    • 発表場所
      法政大学(東京都)
    • 年月日
      2012-08-24
  • [学会発表] SAT技術を用いた組合せテストケース生成2012

    • 著者名/発表者名
      番原睦則
    • 学会等名
      ERATOセミナー, JST ERATO湊離散構造処理系プロジェクト
    • 発表場所
      大阪市(大阪府)
    • 年月日
      2012-07-06
  • [学会発表] 高速充足可能性判定器を用いた命題論理の結論発見器の実装2012

    • 著者名/発表者名
      村松匠,鈴木健士郎,鍋島英知,岩沼宏治
    • 学会等名
      第26回人工知能学会全国大会
    • 発表場所
      山口県教育会館(山口県)
    • 年月日
      2012-06-12
  • [学会発表] 学習節評価尺度LBDに基づく並列SATソルバーの提案2012

    • 著者名/発表者名
      大橋弘幸,鍋島英知
    • 学会等名
      第26回人工知能学会全国大会
    • 発表場所
      山口県教育会館(山口県)
    • 年月日
      2012-06-12
  • [学会発表] 制約充足問題のSAT符号化を用いたパッキング配列の構成2012

    • 著者名/発表者名
      則武治樹,番原睦則,田村直之,井上克己
    • 学会等名
      第26回人工知能学会全国大会
    • 発表場所
      山口県教育会館(山口県)
    • 年月日
      2012-06-12
  • [学会発表] ハミルトン閉路問題のSAT符号化に関する`研究2012

    • 著者名/発表者名
      船越泰輔,番原睦則,田村直之
    • 学会等名
      第26回人工知能学会全国大会
    • 発表場所
      山口県教育会館(山口県)
    • 年月日
      2012-06-12
  • [備考]

    • URL

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

URL: 

公開日: 2014-07-16  

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

Powered by NII kakenhi