Determining Gene Function in Boolean Networks using SAT - Logic Synthesis for Genetic Diseases - page 39

the discrete model simplifies analysis. Furthermore, since the Boolean network is in-
herently a logic circuit, a vast number of techniques from the field of logic synthesis
can be applied to extract the BN.
One such logic synthesis technique is the Karnaugh Map (K-map) [ 10 ] which was
used in [ 4 ] to assign logic functions to genes and generate Boolean networks from a
priori gene pathway information. The K-map is an explicit method to represent and
to simplify a Boolean function. Pathway information is used to create partially filled
K-Maps which describe the update functions (or the next state functions) for each
of the genes in an incompletely specified manner. Minimization of the functions in
each K-map yields a family of Boolean networks. One issue with this approach is
that logical conflicts can arise between different update functions obtained in this
manner from the pathway information. The paper attempts to resolve these conflicts
by perturbing the pathway information, possibly leading to a vastly different net-
work. Another problem arises from the use of an explicit K-map based computation
approach.
One characteristic of assigning logic to the update function given a predictor
set, is that in a predictor set, the gene connections or “wiring” is fixed. Hence, the
problem is how to determine the logic function of each gene, to obtain the GRN.
Similar situations arise in digital design (an example is the wire planning problem
in which wires or communication channels are placed before logic synthesis [ 11 ]).
One method to approach this problem uses SPFDs (sets of pairs of functions to be
distinguished) [ 12 ] which expresses the functional flexibility of nodes in a Boolean
network. In [ 13 ], [ 14 ], SPFDs have been used to optimize Boolean networks. One
drawback is that SPFDs are usually implemented using Boolean Decision Diagrams
(BDDs), which do not scale well due to an exponential memory usage for some
common classes of logic functions.
Other logic synthesis techniques [ 15 ], [ 16 ], which assign logic from state transi-
tion diagrams, start with state information about the circuit, and assign logic which
optimally minimizes the number of gates needed to implement the logic. As men-
tioned, the predictor set (and hence the wiring) in our problem is fixed, and as such,
these logic synthesis methods cannot be used, since they may change the wiring to
minimize the logic.
This method we present uses a Boolean satisfiability (SAT) based method to assign
logic. Many logic synthesis algorithms are based on SAT, and there are several
efficient and well-developed SAT solvers [ 17 ], [ 18 ]. In the context of genomics,
SAT has been applied to the analysis of GRNs. In [ 19 ], a method is presented for
inferring GRN parameters by expressing GRN constraints in a SAT formula. In [ 20 ],
a model checking method (based on SAT) is presented to find all attractors in a
Boolean network. Boolean satisfiability is also used in [ 8 ] to infer the predictor set
of the GRN from attractors, and determine optimal drug selection for cancer therapy.
Our approach is fundamentally different in that we generate a family of BNs for a
predictor set given binary valued gene expression data, in an implicit and efficient
manner.