Biomedical Engineering Reference
In-Depth Information
3.3
Our Approach
3.3.1
SAT-based Formulation for Gene Function Assignment
In our approach, the problem of gene function assignment is transformed into an
instance of Boolean satisfiability, such that each satisfying solution is an assignment
of gene functions in accordance to the input predictor set and gene expression states.
The SAT formulation is done in two distinct steps—(1) circuit construction from the
predictor set and (2) constraining the solution space using the gene expression states.
3.3.1.1
Circuit Construction from the Predictor Set
The first step is to construct a SAT-based circuit that implicitly represents all possible
BNs, based on prior knowledge of the predictor set. From the predictor set, we can
determine the
wiring
of the genes. A predictor states which genes regulate the target
gene, or in circuit terms, which genes are wired to the input of a target gene.
To assign the function for a gene
x
i
, our approach implicitly enumerates all pos-
sible functions {
g
i
1
,
g
i
2
,
...
} and then implicitly selects one function as a solution.
Thus in our circuit construction, for each gene, all possible functions are enumerated,
and a multiplexor (MUX) is added to select exactly one output from all the functions.
Since the size of the predictor of gene
i
is small, the number of possible functions
for gene
i
is tractable. The inputs to the MUX are the outputs of the functions, and
a select signal
s
i
controls which function to select as the output for gene
i
. As such,
the MUX selection determines which function is assigned to the gene.
The circuit is then converted into a CNF formula. Each function (including the
MUX) has a CNF formula associated with it. The formula is true if and only if the
variables representing the gate's inputs and outputs take on values consistent with
its truth table.
One method to write the corresponding CNF of a Boolean formula is using im-
plications and Boolean transformation
s
. The basic transformation of an implication
a
b
). The impl
ic
ation states that if
a
is true
(1), t
h
en
b
is also true (1). We can examine the clause (
a
→
b
into CNF is the single clause (
a
+
+
b
) and see that if
a
=
1,
then
a
0. As such, for the clause to be satisfied (evaluate to 1),
b
must be set to 1.
For example, consider a 2-input OR gate (
g
i
) with
x
and
y
as inputs and
z
as
output. For an OR gate, the output is 1 if and only if one of the inputs are 1. As such,
we have the following two implications:
=
z
→
x
+
y
(3.1)
+
→
x
y
z
(3.2)
