Biomedical Engineering Reference
In-Depth Information
Fig. 1.12
Implication graph
for current assignment
b=1 @ 6
a=1 @ 6
d=1 @ 6
K
c=1 @ 6
conflict
i=0 @ 1
k=0 @ 3
conflict clause to learn. The SAT algorithm then backtracks and the conflict clause
is included in the CNF. Learned clauses are removed if they are not used, thereby
ensuring that the CNF database does not grow uncontrollably.
In [
26
], each decision in the SAT algorithm is recorded with the time (or time
step) of the decision. For example, variable
x
1
was set to 1 value at time 6, or variable
x
9
was set to 0 value at time 1. All decisions up to the current assignment can be
shown on an implication graph, for example Fig.
1.12
.
When a conflict occurs at a decision
K
, the conflicting assignment
A
can be
determined by traversing the graph backwards from
K
. Only the assignments at
previous assignments of
K
are a sufficient condition for the conflict. For example,
from Fig.
1.12
, the conflicting assignment is
A
={
a
=
1
@6,
i
=
0@1,
k
=
0@3
}
.
The conflict assignment induce
s t
he
co
nflict clause
C
=
(
a
+
i
+
k
). Another conflict
induced clause in this case is (
b
c
). The induced conflict clause enables further
implications which improves the search and backtracking in the SAT solver engine,
and ensures that the same conflict does not occur again. During backtrack, conflict
clause allows us to backtrack on
k
(at time 3), thereby avoiding a chronological
backtrack on the variables assigned at time 5 and 4. This non-chronological backtrack
saves much time in the SAT solution process.
+
1.6
Chapter Summary
As we deepen our understanding of how cells operate and how genetic diseases
occur, we realize that many cell components are involved in cell function and that
a systems engineering approach is required. In this chapter, we described the key
issues in genomics and provided an introductory background to the genome and gene
regulatory network. Our work proposes to model the GRN as a Boolean network
(FSM), from which we can use logic synthesis techniques and Boolean Satisfiability
to tackle several genomics problems. We take advantage of improvements in modern
SAT solvers to provide efficient and powerful tools for research. The following
chapters present our methods and application to biological networks. In Chap. 2, we
present a method for inferring the gene predictor set [
27
], [
28
] from gene expression
data. Following that, in Chap. 3, we use the predictor set and gene expression data to
