仮説を立てて考えてみよう
Let's Hypothesize and Reason!
井上 克巳 (Katsumi Inoue)， 丹生 智也 (Tomoya Tanjo)，Nicolas Schwind，Gauvain Bourgne*1，佐藤 泰介 (Taisuke Sato)*2，Andrei Doncescu*3*1: Université d‘Artois， *2: 東京工業大学， *3: LAAS-CNRS- Intelligent machines:
Thinking like human being.
- Automated discovery of scientific knowledge,in particular biological knowledge.

- Automated hypothesis-finding throughdeductively complete methods.
- Abduction of missing links in networks.
- Induction of causal laws in action
theories.
- Applications to systems biology.

BackgroundAbduction and Induction: Logic
Input:How Human Beings Think ?

B : background theory
E : examples / observations

Observation
Everyday Life

Experiments
BusinessScience

Prediction

HypothesizingandReasoning

Output:Abduction
Induction

H : hypothesis satisfying that
1. B ∧ H ⊨ E

2. B ∧ H is consistent

Hypothesis

Inverse Entailment (IE)

Deduction
The genius people are able to mix thesethree fundamental modes of reasoning.

H can be computed deductively by:
B ∧￢E ⊨￢H

Computation and Application
IE for Abduction: SOLAR(Nabeshima, Iwanuma & Inoue 2003, 2010)
B : full clausal theory, E : conjunction of literals
H : conjunction of literals

Closed-loop Architecture for Biological Inference
Background
Knowledge

IE for Induction: CF-induction (Inoue 2004, 2007)
B : full clausal theory, E : full clausal theory
H : full clausal theory

Observations

SOLAR

Example: graph completion problem

Hypotheses
B ∧H⊨EBDD-EM• Inoue et al. Proc. IJCAIT-09, 2009.
• Synnaeve et al. Proc. BIOINFORMATICS 2011.

Find an arc which enables a path from a to d.
Axioms:node(X) ∧ node(Y) ∧ arc(X, Y) → path(X, Y).
node(X) ∧ node(Y) ∧ node(Z) ∧ arc(X, Y)∧ path(Y, Z) → path(X, Z).

PathwayAnalysis
BestHypotheses

Research Goals- Modeling, explaining andpredicting metabolic
pathwaysnode(a). node(b). node(c). node(d). arc(a, b). arc(c, d).
Observation: path(a, d).
Abducibles:arc(_, _).

acbd

SOLAR outputs four hypotheses.
arc(a, d), arc(a, c), arc(b, d), arc(b, c).

Pathway Model(Qualitative / Kinetic)
Pathway Data(from lab + KEGG)

Target Problems

1. Predicting the inhibitoryeffect of toxins including
hydrazine with qualitativemodeling
2. Explaining dynamic
behavior of E. coli pathways
with kinetic modeling

Correspondence： 井上 克巳 （Katsumi Inoue）／ 情報学ﾌﾟﾘﾝｼﾌﾟﾙ研究系 教授, Email : inoue@nii.ac.jp

制約ネットワークと制約充足
Constraint Networks and Solving
井上 克巳 (Katsumi Inoue)， 丹生 智也 (Tomoya Tanjo)，
Nicolas Schwind，宋 剛秀 (Takehide Soh，神戸大学)

・ QCN 間の距離の効率的な特徴解析
・ SATソルバーを推論エンジンとして用いた制約ソルバーの開発
・ スケジューリング問題等の，実用的問題への応用
・ システムズ・レジリエンスへの応用

・制約ネットワークとして記述された問題を自動的に解くための計算原理の確立
・ 動的に変化する制約に対する計算原理の確立

背景
・ 制約ネットワークは，各変数を頂点，変数間の関係を辺として表したグラフ
・ 解きたい問題を制約の形で記述する．
・ 制約ソルバーは，記述された制約を満たす解あるいは最適解を自動的に探索する．
・ 以下では，変数間の関係の自然な記述が可能な定性的制約ネットワーク(QCN)への取り組みと，近年活発に研究が行われているSATソルバーを推論エンジンとして用いるSAT型制約ソルバーを紹介する．

定性的制約ネットワーク(QCN) 間の距離

Modeling
Problem(Encoding)Constraint
Network

Constraint Solver
Solution of
the Problem

Decoding

Solution of
the Constraint
Network

Azucar
SAT型制約ソルバー
Azucar とは・ 国際制約ソルバー競技会2年連続複数部門で優勝した，SAT型制約ソルバー Sugar の改良版

Azucar の特徴

・ QCN は，空間や時間に関する関係を，自然に表現することができる．
・ 上の2つのスケジュールは，直感的には「隣接」しているが，QCN 上では3個の制約が異なっている．
・このため，2つのQCNの距離を測るのにハミング距離を用いることはできない．
・ この問題を解決するため，以下のことを行った．
- 要素の「変形」の概念を形式化- QCN間での「隣接」の概念を形式化- これらの概念の効率的な特徴解析の方法の提供- QCN 間の「距離」を定義 (計算量は NP困難)

・ 新しいSAT符号化法であるコンパクト順序符号化を用いて，大規模な問題を高速に求解が可能
・ BSDライセンスに基づくオープンソースソフト
ウェア
・ 制約最適化問題・最大制約充足問題に対応
・ 整数有限領域上の非線形制約に対応
・ バックエンドのSATソルバーとして，MiniSat やGlueMiniSat を利用可能
URL: http://code.google.com/p/azucar-solver/

Correspondence： 井上 克巳 （Katsumi Inoue）／ 情報学ﾌﾟﾘﾝｼﾌﾟﾙ研究系 教授, Email: inoue@nii.ac.jp