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

2013 Fiscal Year Research-status Report

• Project/Area Number: 25730042
• Research Category: Grant-in-Aid for Young Scientists (B)
• Research Institution: Kobe University
• Principal Investigator: 宋 剛秀 神戸大学, 学内共同利用施設等, 助教 (00625121)
• Project Period (FY): 2013-04-01 – 2016-03-31
• Keywords: SAT技術 / 制約プログラミング / 動的制約 / ドメイン特化言語 / ハミルトン閉路問題 / 推論技術 / 国際情報交換 / フランス

Research Abstract

近年，命題論理式の充足可能性判定 (SAT) 問題を解くためのSAT技術が大きく発展を遂げており，その拡張と応用に注目が集まっている．本研究の目的は，制約の追加・削除に対応したSAT型制約プログラミングシステムを研究開発することにより，既存のSAT技術では困難あるいは不可能だった代謝パスウェイおよびそれを動的に制御する遺伝子調節ネットワークの複合モデルを解析することである．
平成25年度は動的な制約の追加・削除を行うことが可能なSAT型制約プログラミングシステムであるScarabの研究開発を行い，その応用を進めた．Scarabは制約プログラミングのためのドメイン特化言語 (DSL) であるScarab DSL，SAT符号化モジュール，そしてバックエンドのSATソルバーへのインターフェースから構成される．SAT型システム開発者はScarab DSLを用いることで様々な問題を柔軟に制約モデル化可能になる．またScarabはSAT, Max-SAT, 擬似ブール制約など命題論理およびその拡張における推論技術のライブラリであるSat4jと密に結合されており，Java 仮想マシン上で連携して動作することが可能である．
Scarabの基本性能を評価するためにScarabを用いたハミルトン閉路問題のインクリメンタル解法の研究を進め，従来方法と比較して高速な解法システムを実現することに成功した．
これまでSAT技術を応用したシステムは数多く提案されてきたが，Scarabのように制約プログラミングのためのDSLを備えて，Java仮想マシン上でSATソルバーと連携しながら実行できるシステムは少ない．Scarab開発には進歩を続けるSAT技術の応用基盤の提供という意義が存在する．

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

本研究における研究課題は大きく分けて次の3つである: (A) パスウェイの制約モデル, (B) 求解システム, (C) 評価と成果物公開. 平成25年度は (B) の求解システムの開発を行い，SAT型制約プログラミングシステムである Scarab を実現し性能を確認した．このことから研究は順調に進行していると考えている．

Strategy for Future Research Activity

本研究における研究課題は大きく分けて次の3つである: (A) パスウェイの制約モデル, (B) 求解システム, (C) 評価と成果物公開. 平成25年度は (B) の求解システムの開発を行い，SAT型制約プログラミングシステムである Scarab を実現し性能を確認した．平成26年度は (A) のパスウェイの制約モデルに取り組む予定である．この課題に取り組む中で Scarab に機能や性能についての不足がある場合には適宜改善を行う予定である．

Research Products

• [Journal Article] パッキング配列問題の制約モデリングとSAT符号化 (2014)
  • Author(s): 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳
  • Journal Title: コンピュータソフトウェア Volume: 31(1) Pages: 116-130
  • DOI: 10.11309/jssst.31.1_116
  • Peer Reviewed
• [Journal Article] Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems (2013)
  • Author(s): Takehide Soh, Naoyuki Tamura, and Mutsunori Banbara
  • Journal Title: Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013) Volume: LNCS Vol. 7962 Pages: 429-436
  • DOI: 10.1007/978-3-642-39071-5_34
  • Peer Reviewed
• [Journal Article] PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding (2013)
  • Author(s): Naoyuki Tamura, Mutsunori Banbara, and Takehide Soh
  • Journal Title: Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2013) Volume: なし Pages: 1020-1027
  • DOI: 10.1109/ICTAI.2013.153
  • Peer Reviewed
• [Journal Article] Aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming (2013)
  • Author(s): Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Torsten Schaub, Takehide Soh, Naoyuki Tamura and Matthias Weise
  • Journal Title: Proceedings of the Sixth Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2013) Volume: なし Pages: 33-48
  • Peer Reviewed
• [Journal Article] Answer Set Programming as a Modeling Language for Course Timetabling (2013)
  • Author(s): Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue and Torsten Schaub
  • Journal Title: Theory and Practice of Logic Programming Volume: 13(4-5) Pages: 783-798
  • DOI: 10.1017/S1471068413000495
  • Peer Reviewed
• [Presentation] Answer Set Programming as a Modeling Language for Course Timetabling (2014)
  • Author(s): Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
  • Organizer: 第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014)
  • Place of Presentation: 阿蘇の司ビラパークホテル
  • Year and Date: 20140306-20140306
• [Presentation] Scala 上で実現されたSAT型制約プログラミングシステムのための開発ツール Scarab について (2013)
  • Author(s): 宋剛秀, 番原睦則, 田村直之, Daniel Le Berre, Stephanie Roussel
  • Organizer: 日本ソフトウェア科学会第30回大会
  • Place of Presentation: 東京大学
  • Year and Date: 20130913-20130913
• [Presentation] パッキング配列問題の制約モデリングとSAT符号化 (2013)
  • Author(s): 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳
  • Organizer: 日本ソフトウェア科学会第30回大会
  • Place of Presentation: 東京大学
  • Year and Date: 20130913-20130913
• [Presentation] SAT型制約プログラミングシステムのための高速開発ツール (2013)
  • Author(s): 宋 剛秀
  • Organizer: 論理と推論の理論, 実装, 応用に関する合同セミナー
  • Place of Presentation: 北海道大学
  • Year and Date: 20130725-20130725
• [Presentation] CSPSAT Projects and their SAT Related Tools (2013)
  • Author(s): Naoyuki Tamura, Takehide Soh, Mutsunori Banbara, and Katsumi Inoue
  • Organizer: The 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), Combined tool demo and poster session
  • Place of Presentation: University of Helsinki, Finland
  • Year and Date: 20130711-20130711
• [Presentation] System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems (2013)
  • Author(s): Takehide Soh, Naoyuki Tamura, Mutsunori Banbara, Daniel Le Berre, and Stephanie Roussel
  • Organizer: The 4th International Workshop on Pragmatics of SAT (PoS 2013)
  • Place of Presentation: University of Helsinki, Finland
  • Year and Date: 20130708-20130708
• [Presentation] PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding (2013)
  • Author(s): Naoyuki Tamura, Mutsunori Banbara, and Takehide Soh
  • Organizer: The 4th International Workshop on Pragmatics of SAT (PoS 2013)
  • Place of Presentation: University of Helsinki, Finland
  • Year and Date: 20130708-20130708
• [Presentation] 正方形詰込み問題の制約モデルとSAT符号化を用いた解法 (2013)
  • Author(s): 佐古田淳史, 宋剛秀, 番原睦則, 田村直之
  • Organizer: 2013年度人工知能学会全国大会
  • Place of Presentation: 富山国際会議場
  • Year and Date: 20130605-20130605
• [Remarks] Scarab: a Tool for SAT-based CP Systems
  • URL: http://kix.istc.kobe-u.ac.jp/~soh/scarab/