日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集

Scala 上に実現した生物の代謝パスウェイ解析用のドメイン特化言語について
宋 剛秀

馬場 知哉

生体内の細胞は多くの化学反応の連鎖によって活動を維持している. システム生物学において，そのような化学反応の相互作用は代謝パスウェイと呼ばれるネットワークによって表現され，その解析を行うことは重要な課題の一つとなっている．本発表では，オブジェクト指向言語と関数型言語が融合された Scala 上に実現した代謝パスウェイ解
析用のドメイン特化言語 Scarabio の説明をを行う．

Cells in living organism maintain their activity by chains of chemical reactions. In Systems Biology, suchinteractions of chemical reactions are represented in a network called metabolic pathway. Nowadays, theanalysis of metabolic pathways is an important research topic in Systems Biology. In this paper, we describea Domain-Specific Language in Scala for the Analysis of Metabolic Pathways.

されている [6]．例えば米科学誌セルに 2012 年に発表

1 はじめにされ話題を集めたマイコプラズマ菌の細胞解析にも生体内の細胞は多くの化学反応の連鎖によって活動制約モデルが採用されるなど [17]，制約モデルを用いを維持している．システム生物学において，そのようた解析の注目度は高い．このため制約モデルを用いたな化学反応の相互作用は代謝パスウェイと呼ばれる

代謝パスウェイの解析ツールが活発に研究・開発されネットワークによって表現される．代謝パスウェイのている [30] [36] [5] [16] [18] [5].

数学的なモデルを構築し解析することで遺伝子欠損
が細胞に与える影響の予測が可能となり，創薬に必要なアミノ酸などの代謝物を効率よく合成する微生物の設計への応用などを期待できる [26].

このような代謝パスウェイ解析ツールの開発では以下の点が課題になると考えられる．

• 解析ツールの利用者は生物学（システム生物学）、
創薬・代謝工学、計算機科学分野の研究者と想定

これまで小規模の代謝パスウェイに対しては微分される．利用者が幅広く背景知識も異なるため，方程式系を用いる数学的モデルが一般的であったが，誰でも簡単に代謝パスウェイを記述できる必要が大きな代謝パスウェイに対しては方程式中のパラメーある．

タの決定が困難になるため適用が少なかった．それに• 代謝パスウェイの制約モデルの代表的なものと対して近年では細胞規模の巨大な代謝パスウェイに対して Elementary Mode (EM) 解析 [29] [28] [27] がして制約を用いた数学的モデル (制約モデル) が研究あるが，さらに高度な解析を行うためには文献[2] [13] [37] [32] [21] で研究されているような遺伝子

A Domain-Specific Language in Scala for the Analysis
of Metabolic Pathways.
Takehide Soh, 神戸大学 情報基盤センター, Information
Science and Technology Center, Kobe University.
Tomoya Baba, 情報・システム研究機構 新領域融合研
究センター, Transdisciplinary Research Integration
Center, Research Organization of Information and
Systems.

欠損の影響を考慮する等の様々な拡張を容易に行える必要がある．

• 標準的な計算機上で動作し，高速に解析結果を返す必要がある．
これまで提案されてきたツール [36] [5] [16] [18] は，与えられたパスウェイの EM を求めるために Double

1: import jp.kobe_u.scarabio._2:
3: val p = Pathway()4:
5: p.add(CSum() ==> ’A as "R1")
6: p.add(’P ==> CSum() as "R2")
7: p.add(’E ==> CSum() as "R3")
8: p.add(’A ==> ’B as "R4")
9: p.add(’A ==> ’C as "R5")
10: p.add(’A ==> ’D as "R6")
11: p.add(’B <=> ’C as "R7")
12: p.add(’B ==> ’P as "R8")
13: p.add(’C + ’D ==> ’E + ’P as "R9")
14: p.add(’D ==> CSum() as "R10")
15:
16: val esol = EmSolver(p)17: esol.findEM
図1

代謝パスウェイの例 (文献 [6])図2Scarabio を用いたプログラム例

Description (DD) 法 [9] を用いたアルゴリズムを実

本論文の構成は以下になる．まず第 2 節で簡単な装しているが，専用のアルゴリズムのため二つ目の課

代謝パスウェイの例を通して Scarabio を使ったプロ題である制約モデルの拡張を行うのが難しい．またグラムについて説明する．本節の目的は Scarabio のDD 法では，一つだけ解を出力することが出来ず，常感触を伝えることである．第 3 節で, Scarabio を構成に全解列挙を行う．そのためパスウェイが大きくなるする要素技術である汎用プログラミング言語 Scala とと計算に時間がかかったり大量のメモリが必要になる

SAT 型制約プログラミングシステム Scarab の説明ことがあった．

を行う．次に第 4 節で，Scala 上に実現した Scarabio

本論文では，上記の課題を解決することを目的として設計・実装した，生物の代謝パスウェイ解析用のドDSL と Scarab を利用した EM 解析について説明する．最後に第 5 節で本論文をまとめる．

メイン特化言語 (Domain-specific Language; DSL)
である Scarabio について述べる. Scarabio は Scala2 代謝パスウェイと Scarabio プログラム例の内部 DSL として実装され，近年急速に発展してい2. 1 代謝パスウェイの例

る SAT ソルバーを用いた SAT 型制約プログラミン

図 1 は，代謝パスウェイをネットワーク（グラフ）グシステム Scarab [33] を制約モデルの記述および計で表したものである．一般的にパスウェイはこのよう算エンジンとして採用しており，次の特長を持つ．

にラベル付きの有向ハイパーグラフで表されることが• Scala の持つ演算子の多重定義や暗黙変換を用多い．頂点は化学化合物 (Chemical Compounds) をいることで代謝パスウェイの構成要素を簡潔に記表しており，有向辺は化学反応 (Chemical Reaction)

述することができる．

を表している．以降，化学化合物，化学反応を単純に• Scarab の制約記述用 DSL を用いることで EM

化合物，反応と呼ぶ．このパスウェイには A, B, C,の制約モデルを簡潔に記述することができる．

D, E, P の 6 個の化合物と R1 から R10 までの 10

Scarab は動的な制約の追加や削除にも対応して個の反応が含まれている．R1, R2, R3, R10 は反応

おり，制約モデルの拡張を容易にすることを期待物もしくは生成物を持たない特別な反応であり，パできる．

スウェイの入力と出力を表す．R7 は可逆反応であり，• SAT ソルバーの求解能力を利用し，高速に複数の EM を計算することができる．

双方向の反応が可能である．

2. 2 代謝パスウェイ例の Scarabio DSL 表現．

の親和性は高く，Java のクラス・ライブラリをその

前節のパスウェイを Scarabio DSL で記述したもの

まま利用できる．

を図 2 に示す．1 行目はパスウェイに関する DSL ク

さらに Scala は，関数型言語およびオブジェクト

ラスをインポートしている．3 行目はパスウェイ p の指向言語としての高度な記述能力，リスト，マップ，定義を行っている．5 行目から 14 行目は，上述した集合等の豊富なコレクションフレームワーク，演算子

10 個の反応を定義しパスウェイ p へと追加している．

の多重定義や柔軟な構文，オブジェクトのメソッド

このように Scarabio DSL では Scala 言語の特長であのインポート機能など，埋込みの ドメイン特化言語

る暗黙変換，演算子の多重定義，メソッドにおけるピ(DSL; Domain-specific Language) を実装するため

リオドの省略などを用いることで，化学反応式とそのに適した機能を数多く備えている [20]. 特に Scarabio

名前の紐付けを自然に記述可能である．次に 16 行目

DSL ではケースクラス，暗黙変換，シングルトンオ

は EM 解析を行うための解析ソルバーを定義しておブジェクトおよびそのオブジェクトからのインポート

り，17 行目はソルバーを使って EM を計算している．

などの機能を利用しているが，これらの詳細について

Scarabio では，このプログラムが示すように基本的は文献 [24] を参照されたい．

な機能として代謝パスウェイの記述と EM を用いた解析を行うことができる．また第 4. 3 節に記述するよ3. 2 Scarab の概要と特徴

うに EM を解析する Scarabio のプログラム自体も 402000 年以降命題論理の充足可能性判定 (SAT) 問題

行ほどで書かれており，利用者は自由に追加の条件をを解くためのプログラムである SAT ソルバーの性能

記述してより高度な解析へと応用することができる．

が飛躍的に向上しており [7] [12] [23]，このような性能向上は与えられた問題を SAT 問題に符号化し，SAT

3 Scala と Scarab

ソルバーを用いて解を求める SAT 型システムの開

本節では Scarabio の説明の準備として，Scarabio発を促進してきた．これまで論理合成，プランニンを構成する要素技術である汎用プログラミング言語グ，スケジューリング，ハードウェア・ソフトウェア

Scala と SAT 型制約プログラミングシステム Scarabの検証などで SAT 型システムが成功をおさめているについて概説する．なおこれらの詳細については本[12] [4] [35] [22]．

論文の範囲外である．Scala については文献 [24] をScarab については文献 [33] を参照されたい．

Scarab は制約プログラミングのためのドメイン特化言語, SAT 符号化モジュール, SAT ソルバーへのイ
ンターフェースから構成されており，制約プログラミ

3. 1 Scala の概要と特徴
Scala†1 は Martin Odersky により設計された比較

ングシステム利用者を対象に，表現性，変更容易性，的新しいプログラミング言語で，Twitter の分散 DBとしたツールである [33]．Scarab は Scala 言語上にコ

フレームワークに用いられたことなどもあり，近年注

ンパクトに実装されている．バックエンドの SAT ソ

目を集めている [24]. 言語上の特長としては，関数型ルバーに Java で実装された Sat4j を用いることによ

言語とオブジェクト指向言語の融合，強力な型推論，り，インクリメンタル解法等の高度な解法を容易に実型安全性，高階関数，不変コレクションなどが挙げら現できる点も特長の一つである．

効率性を備えたワークベンチを提供することを目的

れる．
処理系としては，JVM (Java Virtual Machine) へ

4 代謝パスウェイ解析用 DSL: Scarabioのコンパイラとインタラクティブな実行環境 (REPL;

Scarabio の設計方針は代謝パスウェイ解析を行う

Read Eval Print Loop) が用意されている．Java と研究者・開発者に表現性，効率性，変更性，可搬性を備えたツールを提供することである．このために関数†1 http://www.scala-lang.org/

型言語とオブジェクト指向言語が融合され DSL の表CExprPathway

Reaction

CTermcompounds: Set [Compound]Set [Reaction]

1 reactions:

EmSolvercsp:

CSP

encoder:solver:EncoderSolver

1 1 satSolver: SatSolver

1

1
1

CSum

Compound

IvReaction

RvReaction

図3

ScarabScarabio のクラス図

1: abstract class CExpr
2: abstract class CTerm extends CExpr
3: case class Compound(name: String, compartment: String = "c") extends CTerm
4: case class CSum(coef: Map[Compound, Int]) extends CTerm5:
6: abstract class Reaction(l: CSum, r: CSum) extends CExpr
7: case class IvReaction(l: CSum, r: CSum) extends Reaction(l,r)
8: case class RvReaction(l: CSum, r: CSum) extends Reaction(l,r)
図4化合物と反応に関するクラス定義 (一部)

現力に優れた Scala を記述言語として採用し，また制で構成される．EM 解析のためのソルバー (EmSolver

約記述の簡潔さと SAT ソルバーの求解能力を備えたクラス) はパスウェイを入力にとし，SAT 型制約プ

Scarab を計算エンジンに採用する．

ログラミングシステム Scarab と連携して，EM を計• 表現性: Scala 言語の全ての機能に加えてパス算する．以降の節では，パスウェイを記述するためのウェイの記述に Scarabio DSL, 制約モデルの記

Scarabio DSL 用のクラス，EM ソルバー用のクラス

述に Scarab DSL を用いる．

について説明する．

• 変更性: Scarab DSL で記述可能な制約を使って自由に制約モデルを拡張・変更可能にする．

4. 2 Scarabio DSL 用のクラス• 効率性: 求解性能が近年飛躍的に向上している

パスウェイにおける化合物や化学反応式を Scala 中

SAT ソルバーをパスウェイ解析に用いる．

で自然に書けるように図 4 に示すようにケースクラ• 可搬性: ツール全体を JVM 上で動作させ，可搬スを定義する．なお図ではクラスの宣言のみを抽出し性のあるシステムを実現する．

て記述しているので注意されたい．1 行目から 4 行目

以降では，まず Scarabio の全体構成を説明し，そのは化学反応式の項に関するクラスの定義であり，6 行

後パスウェイ記述のための DSL クラス，Scarab を利目から 8 行目は化学反応式に関するクラスの定義で用した EM 解析のためのソルバークラスについて説ある．これらの定義と併せて Scala の機能である暗明する．

黙変換，演算子の多重定義，ピリオドの省略などを用いることで，以下の BNF 記法に従った化学反応式の4. 1 Scarabio の構成
Scarabio 全体のクラス図を図 3 に示す．図の左側のクラスがパスウェイ (Pathway クラス) を記述する
ための Scarabio DSL のためのクラスであり，反応(Reaction クラス) や化合物 (Compound クラス) など記述が可能になっている．
Reaction ::= CTerm ==> CTerm
CTerm <=> CTerm
CTerm ::= Compound
Compound * Int
CTerm + CTerm
CSum (Compound * Int, ...)

図5

代謝パスウェイ (図 1) の化学量論行列

4. 3 Scarabio によるパスウェイの EM 解析
代謝パスウェイを解析するための代表的な制約モデルに Elementary Mode (EM) [29] [28] [27] がある．EM を用いた代謝パスウェイの解析では化学量論行列と呼ばれる表現を使う．図 5 に図 1 の代謝パ
スウェイを表した化学量論行列を示す．既存ツール[36] [5] [16] [18] では，Double Description (DD) 法 [9]を用いた EM アルゴリズムを実装しているが，DD法では，一つだけ解を出力することが出来ず，常に全解列挙を行う．そのためパスウェイが大きくなると計算に時間がかかったり大量のメモリが必要になることがあった．
本論文では，EM を制約充足問題の形式に定式化・符号化し SAT ソルバー用いた EM の計算方法を提案
する．提案方法は SAT 型制約プログラミングシステ
ム Scarab を用いて Scarabio 上に実装する．

SAT ソ ル バ ー を 用 い た EM の 計 算 方 法 を 説 明する．いまパスウェイの化学反応が c × q の化学
量論行列 N で与えられたとする．ここで，c は化 合 物 の 数 ， q は 反 応 の 数 で あ る ．N の 要 素
は nij (1 ≤ i ≤ m, 1 ≤ j ≤ q) で 表 す．ま た

xj (1 ≤ j ≤ q) を反応の度合いを表す整数変数と1: import jp.kobe_u.scarab.csp._
2: import jp.kobe_u.scarab.solver._3:
4: case class EmSolver(p: Pathway) {5:
val csp = CSP()
6:
val satSolver = new Sat4j
7:
val encoder = new LogEncoder(csp,satSolver)8:
val solver = new Solver(csp,satSolver,encoder)9:
val d = 510:11:
var bmap = Map.empty[String, Bool]
12:
13:
def define {14:for (r <- p.Reactions)15:
csp.int(’x(r.name), if(r.isRev)-d else 0,d)16:
17:
for (r <- p.Reactions) {18:
val b = Bool(r.name)19:bmap += r.name -> b20:
csp.bool(b)21:csp.add(b ==> (’x(r.name) !== 0))22:
csp.add(Not(b) ==> (’x(r.name) === 0))
23:
}
24:
25:
for (c <- p.Compounds) {26:
val eq = p.rsInvolving(c).map(
27:
r => ’x(r.name) * r.coef(c))
28:
csp.add(Sum(eq.toSeq) === 0)
29:
}
30:
csp.add(Or(bmap.keys.map(bmap(_))))
31:
}
32:
33:
def findEM = {34:define35:
val bset = bmap.values.toSeq
36:
while (solver.findMinimal(bset.toSeq)) {37:
csp.add(Or(bset.filter(i =>38:solver.solution.boolMap(i)).map(Not(_))))
39:
}
40:
}
41:
42: }
図6

SAT ソルバーを用いた EM の解法を実装した
EmSolver クラス

する．パスウェイの定常状態における制約式は以下に
なる．

q
m ∑
∧

要がある．そのため反応の度合いを表す変数 xi に対

nij xj = 0(1)

i=1 j=1

xj ≥ 0(Rj ∈ Irrev)

して，反応の活性・不活性を表す命題変数 bi を導入する．二つの変数を紐付けるチャネリング制約は以下(2)

上式は定常状態においては細胞内の化合物の生成と消費が均衡していることを表している．EM 解析では，
このような制約を満たす極小な反応集合を求める必になる．

bi → xi ̸= 0

(3)

¬bi → xi = 0(4)

最終的に上式 (1), (2), (3), (4) を SAT 符号化し，命題変数集合 {bi | (1 ≤ i ≤ q)} に関する極小モデル

Scarabio を ノ ー ト PC （CPU は Intel Core i7を計算することで SAT ソルバーを用いて EM を計

3.1GHz，メモリ 8GB）上で実行したところ，上記

算することができる．SAT 符号化には順序符号化

パスウェイの 1 つの EM は 1 秒未満で計算することが[8] [3] [1] [11] [31] [34] や対数符号化 [14] [10] が利用可能

できた．また 100 個の EM を求めるのに要した CPUであり，極小モデルの計算には文献 [19] の方法を利用

時間は 74 秒であった．Scarabio では，興味のある反できる．SAT 型制約プログラミングシステム Scarab

応が含まれる EM を計算したり，EM に含まれる反は，これらの機能をデフォルトで提供している．図 6

応の数を制限することも可能である．このことからに Scarabio における，EM ソルバーの実装を示す．1

SAT ソルバーを用いた EM の計算方法，またそれを行目から 8 行目までで，Scarab の関連クラスのイン実装したツール Scarabio は代謝パスウェイ解析におポートと CSP ソルバーの定義を行っている．14，15

ける有効な手法になると考えられる．

行目では反応の度合いを表す整数変数 xi を定義している．17 行目から 23 行目は式 (3), (4) を表してい

5 おわりにる．25 行目から 29 行目は式 (1) を表している．33

本論文では，生物の代謝パスウェイ解析用の DSL行目から 39 行目で bi の集合に関する極小モデルをScarabio について述べた．Scarabio は Scala の内部

Scarab を用いて求め，EM を計算している．

DSL として実装されており，近年急速に発展している

このように EM を解析する Scarabio のプログラム

SAT ソルバーを用いた SAT 型制約プログラミングシ

自体も 40 行ほどで簡潔に記述できる．これにより，

ステム Scarab [33] を制約モデルの記述および計算エ

利用者が直接 EmSolver を編集することも可能であンジンとして採用することで，簡潔なパスウェイ・制り，文献 [2] [13] [37] [32] [21] で研究されているような遺約モデルの記述と高速な EM の計算が可能である．今伝子欠損の影響を考慮することも可能である．

後の課題は，極小非充足コアなどの高度な SAT 技術
をパスウェイ解析に応用することである．Scarabio は

4. 4 EM 求解性能の評価

以下の URL からダウンロード可能である. http://

Scarabio の EM 解析ツールとしての基本性能を評

kix.istc.kobe-u.ac.jp/~soh/scarab/scarabio/

価するために，制約モデル解析のベンチマークとしてよく使われる大腸菌の代謝パスウェイ E. coli core

参 考 文 献[25] を用いて簡単な計算機実験を行った．この代謝[ 1 ] Ansótegui, C. and Manyà, F.: Mapping Problems with Finite-Domain Variables into Problems
with Boolean Variables, SAT 2004 - The SeventhInternational Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004,
Vancouver, BC, Canada, Online Proceedings, 2004.
[ 2 ] Baba, T., Ara, T., Hasegawa, M., Takai, Y.,
Okumura, Y., Baba, M., Datsenko, K. A., Tomita,
M., Wanner, B. L., and Mori, H.: Construction ofEscherichia coli K-12 in-frame, single-gene knockout mutants: the Keio collection, Molecular Systems Biology, Vol. 2, No. 2006.0008(2006).
[ 3 ] Bailleux, O. and Boufkhad, Y.: Eﬃcient CNF
Encoding of Boolean Cardinality Constraints, Proceedings of the 9th International Conference on
Principles and Practice of Constraint Programming(CP 2003), LNCS 2833, 2003, pp. 108–122.
[ 4 ] 番原睦則, 田村直之: SAT によるシステム検証, 人
工知能学会誌, Vol. 25, No. 1(2010), pp. 122–129.
[ 5 ] Becker, S. A., Feist, A. M., Mo, M. L., Hannum, G., Palsson, B. Ø., and Herrgard, M. J.:

パスウェイは 72 の化合物と 94 の反応で構成される．
図 7 にこの代謝パスウェイを示す．
文献 [15] では，6 コアの Intel Xeon CPU を 2 個とメモリ 190GB (153GB を実際に使用) を搭載した計算機を使って，上記のパスウェイの EM を現在最も高速といわれる efmtool を用いて計算している．結果
として，全ての EM (226.6 × 106 個) を求めるのに

34 時間かかることが報告されている．efmtool ツー
ルは他のツールと同様に Double Description 法を用いており全ての EM を列挙するまでは 1 つも解を返すことができないことに注意されたい．現実的には

226.6 × 106 個もの全ての EM を解析するのは不可能であり，高速に興味がある EM が見つかるほうが望
ましい．

図7

計算機実験のベンチマークとして用いた E. coli core の代謝パスウェイ

http://2014.igem.org/Team:TU_Delft-Leiden/Modeling/EET/FBA#EETCoreModel より引用
Quantitative prediction of cellular metabolism withconstraint-based models: the COBRA Toolbox, Nature Protocols, Vol. 2, No. 3(2007), pp. 727–738.
[ 6 ] Benner, P., Findeisen, R., Flockerzi, D., Reichl,
U., and Sundmache, K.: Large-Scale Networks in
Engineering and Life Sciences, Springer, 2014.
[ 7 ] Biere, A., Heule, M., van Maaren, H., andWalsh, T.(eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications(FAIA), Vol. 185, IOS Press, 2009.
[ 8 ] Crawford, J. M. and Baker, A. B.: Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems, Proceedings of the
12th National Conference on Artificial Intelligence(AAAI 1994), 1994, pp. 1092–1097.
[ 9 ] Fukuda, K. and Prodon, A.: Double description method revisited, Combinatorics and Computer Science, Vol. 1120(1996), pp. 91–111.
[10] Gelder, A. V.: Another Look at Graph Coloring via Propositional Satisfiability, Discrete Applied

Mathematics, Vol. 156, No. 2(2008), pp. 230–243.
[11] Gent, I. P. and Nightingale, P.: A New Encoding of Alldiﬀerent into SAT, Proceedings of the 3rdInternational Workshop on Modelling and Reformulating Constraint Satisfaction Problems, 2004.
[12] 井上克巳, 田村直之: SAT ソルバーの基礎, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 57–67.
[13] Ishii, N., Nakahigashi, K., Baba, T., Robert, M.,
Soga, T., Kanai, A., Hirasawa, T., Naba, M., Hirai,
K., Hoque, A., Ho, P. Y., Kakazu, Y., Sugawara,
K., Igarashi, S., Harada, S., Masuda, T., Sugiyama,N., Togashi, T., Hasegawa, M., Takai, Y., Yugi, K.,
Arakawa, K., Iwata, N., Toya, Y., Nakayama, Y.,
Nishioka, T., Shimizu, K., Mori, H., and Tomita,
M.: Multiple High-Throughput Analyses Monitor
the Response of E. coli to Perturbations, Science,Vol. 316, No. 5824(2007), pp. 593–597.
[14] Iwama, K. and Miyazaki, S.: SAT-Variable
Complexity of Hard Combinatorial Problems,Proceedings of the IFIP 13th World Computer

Congress, 1994, pp. 253–258.
[15] Jungreuthmayer, C., Ruckerbauer, D. E., andZanghellini, J.: Utilizing gene regulatory information to speed up the calculation of elementary flux
modesx, ArXiv e-prints, (2012).
[16] Kamp, A. v. and Schuster, S.: Metatool 5.0: fast
and flexible elementary modes analysis, Bioinformatics, Vol. 22, No. 15(2006), pp. 1930–1931.
[17] Karr, J. R., Sanghvi, J. C., and Derek N. Macklin, e. a.: A whole-cell computational model predicts phenotype from genotype, Cell, Vol. 150,
No. 2(2012), pp. 389–401.
[18] Klamt, S., Saez-Rodriguez, J., and Gilles, E. D.:
Structural and functional analysis of cellular networks with CellNetAnalyzer, BMC Systems Biology, Vol. 1, No. 2(2007).
[19] Koshimura, M., Nabeshima, H., Fujita, H., andHasegawa, R.: Minimal model generation with respect to an atom set, Proceedings of the the 7thInternational Workshop on First-Order Theorem
Proving (FTP ’09), 2009, pp. 49–59.
[20] Mernik, M., Heering, J., and Sloane, A. M.:
When and How to Develop Domain-Specific
Languages, ACM Computing Surveys, Vol. 37,
No. 4(2005), pp. 316–344.
[21] Mori, H., Baba, T., Yokoyama, K., Takeuchi, R.,
Nomura, W., Makishi, K., Otsuka, Y., Dose, H., andWanner, B.: Identification of Essential Genes andSynthetic Lethal Gene Combinations in Escherichia
coli K-12, Gene Essentiality, Lu, L. J.(ed.), Methods in Molecular Biology, Vol. 1279, Springer New
York, 2015, pp. 45–65.
[22] 鍋島英知: SAT によるプランニングとスケジューリ
ング, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 114–
121.
[23] 鍋島英知, 宋剛秀: 高速 SAT ソルバーの原理, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 68–76.
[24] Odersky, M., Spoon, L., and Venners, B.: Programming in Scala, Artima, Inc., second edition,
2010.
[25] Orth, J., Fleming, R., and Palsson, B.: Reconstruction and Use of Microbial Metabolic Networks:
the Core Escherichia coli Metabolic Model as an Educational Guide, EcoSal Plus, (2010).
[26] Schmid, A., Dordick, J. S., Hauer, B., Kiener,A., Wubbolts, M., and Witholt, B.: Industrial biocatalysis today and tomorrow, Nature,
Vol. 409(2001), pp. 258–268.

[27] Schuster, S.: A general definition of metabolic
pathways useful for systematic organization andanalysis of complex metabolic networks, Nature
Biotechnology, Vol. 18, No. 3(2000), pp. 326–332.
[28] Schuster, S., Dandekar, T., and Fell, D. A.:
Detection of elementary flux modes in biochemical networks: a promising tool for pathway analysis
and metabolic engineering, Trends in Biotechnology, Vol. 17, No. 2(1999), pp. 53–60.
[29] Schuster, S. and Hillgetag, C.: On Elementary Flux Modes in Biochemical Reaction Systems
at Steady State, Journal of Biological Systems,
Vol. 02, No. 02(1994), pp. 165–182.
[30] Schwarz, R., Musch, P., von Kamp, A., Engels,
B., Schirmer, H., Schuster, S., and Dandekar, T.:
YANA a software tool for analyzing flux modes,
gene-expression and enzyme activities, BMC Bioinformatics, Vol. 6, No. 135(2005).
[31] Sinz, C.: Towards an Optimal CNF Encoding ofBoolean Cardinality Constraints, Proceedings of the
11th International Conference on Principles andPractice of Constraint Programming (CP 2005),
LNCS 3709, 2005, pp. 827–831.
[32] Soh, T., Inoue, K., Baba, T., Takada, T., andShiroishi, T.: Evaluation of the Prediction of Gene
Knockout Eﬀects by Minimal Pathway Enumeration, International Journal On Advances in Life
Sciences, Vol. 4, No. 3-4(2012), pp. 154–165.
[33] Soh, T., Tamura, N., and Banbara, M.: Scarab:
A Rapid Prototyping Tool for SAT-based Constraint Programming Systems, Proceedings of the
16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013),
LNCS 7962, July 2013, pp. 429–436.
[34] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Constraints, Vol. 14, No. 2(2009), pp. 254–272.
[35] 田村直之, 丹生智也, 番原睦則: 制約最適化問題とSAT 符号化, 人工知能学会誌, Vol. 25, No. 1(2010),
pp. 77–85.
[36] Terzer, M. and Stelling, J.: Accelerating theComputation of Elementary Modes Using Pattern
Trees, Algorithms in Bioinformatics, Lecture Notes
in Computer Science, Vol. 4175, Springer Berlin
Heidelberg, 2006, pp. 333–343.
[37] 宋剛秀, 井上克巳: モデル生成を用いた代謝ネット
ワークにおける極小活性パスウェイの列挙, 人工知能学
会論文誌, Vol. 27, No. 3(2012), pp. 204–212.