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 |
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
(14 results)
-
-
-
-
-
-
-
-
-
-
[Presentation] CSPSAT Projects and their SAT Related Tools2013
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
-
-
-
-
