SAT変換を用いた制約充足問題の解法とシステム生物学への応用

点击翻译按钮获取中文摘要

最終年度の報告として、これまでの研究成果について以下にまとめる。本研究では化学反応法則を満たしつつ入力代謝物集合から出力代謝物集合を生成可能なパスウェイを活性パスウェイ呼び、特にその包含関係において極小なものを極小活性パスウェイと呼ぶ。研究ではまず極小活性パスウェイを列挙する問題を極小活性パスウェイ同定問題として定義を行った。代謝パスウェイの解析を行う際には既存のデータから問題を構築する必要がある。そこで更新頻度において優れていることから、生物学的知識のデータベースEcoCyc(http://ecocyc.org/)から問題を構成して評価を行った。このデータから構成した問題をSAT技術によって解くために本研究では次の枠組みを用いた:(1)まず問題を命題論理式に符号化する、(2)SATソルバを漸増的に適用するインクリメンタルSAT解法を用いて符号化された命題論理式から極小モデルを計算する、(3)得られた極小モデルを逆符号化することで問題の解である極小活性パスウェイを得る。提案した問題および解法の評価のためにEcoCycのデータから極小活性パスウェイ同定問題を構成し、SAT技術を用いて解を求めた。結果として9個の極小活性パスウェイを同定し、その中の2個が生物学における既存の知識と一致したパスウェイ(参照パスウェイ)であることを確認している。また専門家との議論で提案された制約を命題論理式に追加することでより精緻なパスウェイを計算することに成功した。この成果は国内雑誌論文として発表を行った。また代謝パスウェイに対する解集合プログラミングを用いた解析研究についても国際会議の会議録で発表を行った。さらにより具体的な生物学の問題に適用するために、大腸菌における単一遺伝子ノックアウトの影響予測を極小活性パスウェイの同定によって行う手法の研究を国立遺伝学研究所の研究チームと共同して進めた。大腸菌の解糖系に対して計算機実験を行った結果,提案手法の予測が生物実験の結果とよく一致することを確認した。この成果は国際会議において発表を行った。