代謝パスウェイ解析のための制約プログラミングシステムの研究開発

• 研究課題/領域番号: 25730042
• 研究種目: 若手研究(B)
• 配分区分: 基金
• 研究分野: ソフトウェア
• 研究機関: 神戸大学
• 研究代表者: 宋 剛秀 神戸大学, 情報基盤センター, 助教 (00625121)
• 研究期間 (年度): 2013-04-01 – 2016-03-31
• 研究課題ステータス: 完了 (2015年度)
• 配分額: 2,340千円 (直接経費: 1,800千円、間接経費: 540千円); 2015年度: 650千円 (直接経費: 500千円、間接経費: 150千円); 2014年度: 650千円 (直接経費: 500千円、間接経費: 150千円); 2013年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
• キーワード: SATソルバー / 制約プログラミング / 代謝パスウェイ / Elementary Mode / ハミルトン閉路 / ドメイン特化言語 / 命題論理 / ハイブリッド符号化 / SAT型制約プログラミングシステム / システム生物学 / SAT符号化 / グラフ上の組合せ問題 / 制約充足問題 / 国際情報交換 / SAT技術 / 動的制約 / ハミルトン閉路問題 / 推論技術 / フランス

研究成果の概要

近年，命題論理式の充足可能性判定 (SAT) 問題を解くためのSAT技術が大きく発展を遂げており，その拡張・応用に注目が集まっている．本研究の目的は，制約の追加・削除に対応したSAT型制約プログラミンングシステムを研究開発することにより，既存のSAT技術では困難あるいは不可能だった代謝パスウェイの制約モデルを解析することである．研究成果としてSAT型制約プログラミングシステム Scarab を開発し，代謝パスウェイの Elementary Mode 解析に応用した結果，既存研究より優れた結果を得た．

研究成果

• [国際共同研究] Universite d'Artois/CRIL-CNRS UMR 8188(フランス)
• [国際共同研究] University of Potsdam(ドイツ)
• [雑誌論文] A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings (2015)
  • 著者名/発表者名: Takehide Soh, Mutsunori Banbara, and Naoyuki Tamura
  • 雑誌名: Proceedings of the 27th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2015, SAT and CSP track) 巻: - ページ: 421-428
  • DOI: 10.1109/ictai.2015.70
  • NAID: 40020657481
  • 査読あり
• [雑誌論文] aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming (2015)
  • 著者名/発表者名: Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Max Ostrowski, Andrea Peano, Torsten Schaub, Takehide Soh, Naoyuki Tamura, and Matthias Weise
  • 雑誌名: Proceedings of the 13th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR 2015) 巻: LNAI9345 ページ: 112-126
  • DOI: 10.1007/978-3-319-23264-5_10
  • ISBN: 9783319232638, 9783319232645
  • 査読あり / 国際共著
• [雑誌論文] Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem (2014)
  • 著者名/発表者名: Takehide Soh, Daniel Le Berre, Stephanie Roussel, Mutsunori Banbara, Naoyuki Tamura
  • 雑誌名: Proceedings of the 14th European Conference on Logics in Artificial Intelligence (JELIA 2014) 巻: Vol.8761 ページ: 684-693
  • DOI: 10.1007/978-3-319-11558-0_52
  • ISBN: 9783319115573, 9783319115580
  • 査読あり / 謝辞記載あり
• [雑誌論文] パッキング配列問題の制約モデリングとSAT符号化 (2014)
  • 著者名/発表者名: 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳
  • 雑誌名: コンピュータ ソフトウェア 巻: 31 号: 1 ページ: 1_116-1_130
  • DOI: 10.11309/jssst.31.1_116
  • NAID: 130004549327
  • ISSN: 0289-6540
  • 査読あり
• [雑誌論文] Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems (2013)
  • 著者名/発表者名: Takehide Soh, Naoyuki Tamura, and Mutsunori Banbara
  • 雑誌名: Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013) 巻: なし ページ: 429-436
  • DOI: 10.1007/978-3-642-39071-5_34
  • ISBN: 9783642390708, 9783642390715
  • 査読あり
• [雑誌論文] PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding (2013)
  • 著者名/発表者名: Naoyuki Tamura, Mutsunori Banbara, and Takehide Soh
  • 雑誌名: Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2013) 巻: なし ページ: 1020-1027
  • DOI: 10.1109/ictai.2013.153
  • 査読あり
• [雑誌論文] Aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming (2013)
  • 著者名/発表者名: Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Torsten Schaub, Takehide Soh, Naoyuki Tamura and Matthias Weise
  • 雑誌名: Proceedings of the Sixth Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2013) 巻: なし ページ: 33-48
  • 査読あり
• [雑誌論文] Answer Set Programming as a Modeling Language for Course Timetabling (2013)
  • 著者名/発表者名: Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue and Torsten Schaub
  • 雑誌名: Theory and Practice of Logic Programming 巻: 13(4-5) 号: 4-5 ページ: 783-798
  • DOI: 10.1017/s1471068413000495
  • 査読あり
• [学会発表] クラウド上のソフトウェア要素最適配置問題の解法 (2016)
  • 著者名/発表者名: 田村直之, 井上克巳, 鍋島英知, 番原睦則, 宋剛秀
  • 学会等名: 人工知能基本問題研究会(第100回)
  • 発表場所: 熊本市民会館（熊本県・熊本市）
  • 年月日: 2016-03-27
• [学会発表] 分子ネットワーク上の状態推定とその可視化による知識発見支援 (2016)
  • 著者名/発表者名: 平沼祐人, 山本泰生, 守屋央朗, 宋剛秀, 岩沼宏治
  • 学会等名: 第45回バイオ情報学研究発表会
  • 発表場所: 北陸先端科学技術大学院大学（石川県・能美市）
  • 年月日: 2016-03-18
• [学会発表] インクリメンタルSAT解法を用いた高速ナンバーリンクソルバー (2016)
  • 著者名/発表者名: 迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知
  • 学会等名: 第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016)
  • 発表場所: ダイヤモンド瀬戸内マリンホテル（岡山県・玉野市）
  • 年月日: 2016-03-07
• [学会発表] 解集合プログラミングを用いた制約組合せテストケース生成 (2016)
  • 著者名/発表者名: 兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳, 沖本天太
  • 学会等名: 第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016)
  • 発表場所: ダイヤモンド瀬戸内マリンホテル（岡山県・玉野市）
  • 年月日: 2016-03-07
• [学会発表] SATソルバーを用いた制約プログラミングシステムとその応用 (2016)
  • 著者名/発表者名: 宋剛秀
  • 学会等名: 第57回プログラミング・シンポジウム
  • 発表場所: ラフォーレ倶楽部伊東温泉湯の庭（静岡県・伊東市）
  • 年月日: 2016-01-08
• [学会発表] SATソルバーとそのアプリケーション開発について (SAT型制約ソルバー) (2015)
  • 著者名/発表者名: 宋剛秀
  • 学会等名: 第9回AIツール入門講座
  • 発表場所: 国立情報学研究所（東京都・千代田区）
  • 年月日: 2015-12-14
  • 招待講演
• [学会発表] Scala 上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について (2015)
  • 著者名/発表者名: 宋剛秀, 馬場知哉
  • 学会等名: 日本ソフトウェア科学会第32回大会
  • 発表場所: 早稲田大学（東京都・新宿区）
  • 年月日: 2015-09-08
• [学会発表] SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価 (2015)
  • 著者名/発表者名: 川原征大, 宋剛秀, 番原睦則, 田村直之
  • 学会等名: 日本ソフトウェア科学会第32回大会
  • 発表場所: 早稲田大学（東京都・新宿区）
  • 年月日: 2015-09-08
• [学会発表] iSugar : インクリメンタルSAT解法が利用可能なSAT型制約ソルバー (2015)
  • 著者名/発表者名: 迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳
  • 学会等名: 日本ソフトウェア科学会第32回大会
  • 発表場所: 早稲田大学（東京都・新宿区）
  • 年月日: 2015-09-08
• [学会発表] 順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化 (2015)
  • 著者名/発表者名: 宋剛秀, 番原睦則, 田村直之
  • 学会等名: 日本ソフトウェア科学会第32回大会
  • 発表場所: 早稲田大学（東京都・新宿区）
  • 年月日: 2015-09-08
• [学会発表] 組合せテストケース生成問題に対する制約解集合プログラミングの適用 (2015)
  • 著者名/発表者名: 兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳
  • 学会等名: 2015年度人工知能学会全国大会
  • 発表場所: 公立はこだて未来大学（北海道・函館市）
  • 年月日: 2015-05-30
• [学会発表] 制約充足問題のハイブリッド符号化に向けて (2015)
  • 著者名/発表者名: 宋剛秀, 佐古田淳史, 番原睦則, 田村直之
  • 学会等名: 人工知能学会 第97回人工知能基本問題研究会
  • 発表場所: 別府国際コンベンションセンター (大分県)
  • 年月日: 2015-03-22
• [学会発表] Scarab: 高度なSAT解法を利用可能な制約プログラミングシステム (2015)
  • 著者名/発表者名: 宋剛秀, 番原睦則, 田村直之
  • 学会等名: 第17回プログラミングおよびプログラミング言語ワークショップ (PPL 2015)
  • 発表場所: 道後プリンスホテル (愛媛県)
  • 年月日: 2015-03-04
• [学会発表] Scala上で実現されたSAT型制約プログラミングシステムのための開発ツール (2014)
  • 著者名/発表者名: 宋剛秀, 番原睦則, 田村直之
  • 学会等名: 日本ソフトウェア科学会第31回大会
  • 発表場所: 名古屋大学 (愛知県)
  • 年月日: 2014-09-09
• [学会発表] 制約解集合プログラミングシステムの設計方式に関する考察 (2014)
  • 著者名/発表者名: 宋剛秀, 則武治樹, 番原睦則, 田村直之, 井上克巳
  • 学会等名: 日本ソフトウェア科学会第31回大会
  • 発表場所: 名古屋大学 (愛知県)
  • 年月日: 2014-09-08
• [学会発表] SAT型制約ソルバーを用いたナンバーリンクの解法 (2014)
  • 著者名/発表者名: 田村直之, 宋剛秀, 番原睦則, 鍋島英知
  • 学会等名: DAシンポジウム2014
  • 発表場所: 水明館 (岐阜県)
  • 年月日: 2014-08-29
• [学会発表] Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem (2014)
  • 著者名/発表者名: Takehide Soh, Daniel Le Berre, Stéphanie Roussel, Mutsunori Banbara, Naoyuki Tamura
  • 学会等名: The 5th International Workshop on Pragmatics of SAT (PoS 2014)
  • 発表場所: ウィーン工科大学 (オーストリア)
  • 年月日: 2014-07-13
• [学会発表] 登録後コース時間割問題の基数制約を用いた制約モデルとSATソルバーを用いた解法 (2014)
  • 著者名/発表者名: 佐古田淳史, 宋剛秀, 番原睦則, 田村直之
  • 学会等名: 第28回人工知能学会全国大会
  • 発表場所: ひめぎんホール (愛媛県)
  • 年月日: 2014-05-12
• [学会発表] SATソルバーと密に結合された制約プログラミングシステムScarabとハミルトン閉路問題への応用 (2014)
  • 著者名/発表者名: 宋剛秀, Daniel Le Berre, Stéphanie Roussel, 番原睦則, 田村直之
  • 学会等名: 第28回人工知能学会全国大会
  • 発表場所: ひめぎんホール (愛媛県)
  • 年月日: 2014-05-12
• [学会発表] Answer Set Programming as a Modeling Language for Course Timetabling (2014)
  • 著者名/発表者名: Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
  • 学会等名: 第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014)
  • 発表場所: 阿蘇の司ビラパークホテル
• [学会発表] Scala 上で実現されたSAT型制約プログラミングシステムのための開発ツール Scarab について (2013)
  • 著者名/発表者名: 宋剛秀, 番原睦則, 田村直之, Daniel Le Berre, Stephanie Roussel
  • 学会等名: 日本ソフトウェア科学会第30回大会
  • 発表場所: 東京大学
• [学会発表] System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems (2013)
  • 著者名/発表者名: Takehide Soh, Naoyuki Tamura, Mutsunori Banbara, Daniel Le Berre, and Stephanie Roussel
  • 学会等名: The 4th International Workshop on Pragmatics of SAT (PoS 2013)
  • 発表場所: University of Helsinki, Finland
• [学会発表] PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding (2013)
  • 著者名/発表者名: Naoyuki Tamura, Mutsunori Banbara, and Takehide Soh
  • 学会等名: The 4th International Workshop on Pragmatics of SAT (PoS 2013)
  • 発表場所: University of Helsinki, Finland
• [学会発表] 正方形詰込み問題の制約モデルとSAT符号化を用いた解法 (2013)
  • 著者名/発表者名: 佐古田淳史, 宋剛秀, 番原睦則, 田村直之
  • 学会等名: 2013年度人工知能学会全国大会
  • 発表場所: 富山国際会議場
• [学会発表] パッキング配列問題の制約モデリングとSAT符号化 (2013)
  • 著者名/発表者名: 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳
  • 学会等名: 日本ソフトウェア科学会第30回大会
  • 発表場所: 東京大学
• [学会発表] CSPSAT Projects and their SAT Related Tools (2013)
  • 著者名/発表者名: Naoyuki Tamura, Takehide Soh, Mutsunori Banbara, and Katsumi Inoue
  • 学会等名: The 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), Combined tool demo and poster session
  • 発表場所: University of Helsinki, Finland
• [学会発表] SAT型制約プログラミングシステムのための高速開発ツール (2013)
  • 著者名/発表者名: 宋 剛秀
  • 学会等名: 論理と推論の理論, 実装, 応用に関する合同セミナー
  • 発表場所: 北海道大学
• [備考] Scarabio: SATソルバーを用いた Elementary Mode 解析システム
  • URL: http://kix.istc.kobe-u.ac.jp/~soh/scarab/scarabio/
• [備考] Diet-Sugar: SATソルバーを用いたCSPソルバー
  • URL: http://kix.istc.kobe-u.ac.jp/~soh/dsugar/
• [備考] Scarab --- SAT-based Constraint Programming System
  • URL: http://kix.istc.kobe-u.ac.jp/~soh/scarab/
• [備考] 研究実績（宋剛秀）
  • URL: http://kix.istc.kobe-u.ac.jp/~soh/jp/publications.html
• [備考] 研究業績（宋剛秀）
  • URL: http://kix.istc.kobe-u.ac.jp/~soh/jp/publications.html
• [備考] Scarab: a Tool for SAT-based CP Systems
  • URL: http://kix.istc.kobe-u.ac.jp/~soh/scarab/
• [備考] hss: HCP Solver based on Scarab and Sat4j
  • URL: http://kix.istc.kobe-u.ac.jp/~soh/scarab/hcp.html
• [備考] muffin: Constraint ASP (CASP) System
  • URL: http://www.edu.kobe-u.ac.jp/istc-tamlab/cspsat/mfn/
• [備考] Scarab: a Tool for SAT-based CP Systems
  • URL: http://kix.istc.kobe-u.ac.jp/~soh/scarab/