| 研究実績の概要 |
近年, 命題論理式の充足可能性判定 (SAT) 問題を解くためのSAT技術が大きく発展を遂げており, その拡張と応用に注目が集まっている. 本研究の目的は,制約の追加・削除に対応したSAT型制約プログラミングシステムを研究開発することにより, 既存のSAT技術では困難あるいは不可能だった代謝パスウェイの複合モデルを解析することである.
平成27年度は，これまで期間で研究開発したSAT型制約プログラミングシステム Scarab のさらなる拡張と応用に関する研究を進めた．主要な成果の一つはScarab の代謝パスウェイにおける Elementary Mode (EM) 解析への応用である．従来手法では EM の極小性を保証するためには解を全列挙する必要があったが，Scarab を用いた方法では EM を1つずつ計算することが可能である．公開されている大腸菌の代謝パスウェイ E. coli core [Orth, Fleming, Palsson 2010] を使って計算機実験を行ったところ EM 解析で最もよく使われている efmtool と比較して大きく性能を向上することに成功した．この成果の一部は日本ソフトウェア科学会第32回大会で発表し，開発ソフトウェアを web page で公開した．また順序符号化と対数符号化という2つのSAT符号化の長所を組み合わせたハイブリッド符号化の研究も今年度の成果の一つである．計算機実験の結果，ハイブリッド符号化の性能は順序符号化および対数符号化より優れており，両方の符号化で解くことが出来ない問題を解くことにも成功した．研究成果は査読付き国際学会 IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2015) で発表し，開発ソフトウェアを web page で公開した．
上記の成果の他に国際会議を含む11件の研究発表を行った．
|
