Biomedical Engineering Reference
In-Depth Information
formulate the clauses
c
i
for gene
i
, smaller clauses are formed from all pairs of
combinations of its predictors
v
i
1
···
j
. In each of these clauses of pairs of variables,
both predictor variables are complemented.
c
1
=
(
v
1
+
v
2
)
c
2
=
(
v
1
+
v
2
)
(
v
1
+
v
3
)
(
v
1
+
v
4
)
(
v
2
+
v
3
)
(
v
2
+
v
4
)
(
v
3
+
v
4
)
·
·
·
·
·
c
3
=
(
v
1
+
v
2
)
·
(
v
1
+
v
3
)
·
(
v
2
+
v
3
)
Any selection of two or more predictors for gene
i
will result in the clauses of
c
i
becoming unsatisfiable. The
c
i
clause ensures that at least one predictor will be
chosen for gene
i
, and
c
i
forces the selection of exactly one predictor for gene
i
.
The conjunction of all
c
i
clauses forms the constraint
S
2
(Eq.
2.2
), which forces
SAT to choose only one predictor per gene.
c
1
·
c
2
·
c
3
S
2
=
(2.2)
3. The last constraint (
S
3
) requires that each gene must be used as a predictor for at
least one other gene in the predictor set. A gene that is not used in any predictor
does not perform any regulation function and could be removed from the GRN.
S
3
ensures that this does not occur. To ensure that gene
g
i
is used in at least one
predictor, we form clauses
c
i
which include all predictors that use gene
g
i
as
input. To specify that gene
g
i
must be used, we also include a single variable
clause (
x
i
)to
c
i
. For gene
g
1
,
g
2
, and
g
3
, we create the following clauses
c
1
,
c
2
,
and
c
1
3 respectively:
c
1
=
v
1
+
v
2
+
v
1
+
v
2
+
v
4
+
v
1
+
v
3
)
(
x
1
)
·
(
x
1
+
c
2
=
v
2
+
v
1
+
v
3
+
v
4
+
v
2
+
v
3
)
(
x
2
)
·
(
x
2
+
c
3
=
v
1
+
v
2
+
v
2
+
v
3
+
v
4
+
v
1
+
v
2
+
v
3
)
(
x
3
)
·
(
x
3
+
To satisfy these clauses,
x
i
and at least one other predictor variable in the second
clause of
c
i
must be selected.
S
3
is a conjunction of all the
c
3
clauses (Eq.
2.3
).
S
3
=
c
1
·
c
2
·
c
3
(2.3)
The final SAT formula
S
as a conjunction of the
S
i
formulas (Eq.
2.4
).
S
=
S
1
·
S
2
·
S
3
(2.4)
