ATPG for Cancer Therapy - Logic Synthesis for Genetic Diseases - page 75

In [ 5 ], the authors proposed modeling cancer as faults in the signaling network and
applied fault analysis for drug intervention to control the GRN. Cancer is a disease
that arises from fault(s) in the network, leading to loss of cell cycle control and
uncontrolled cell proliferation. Therapy involves both identification of the fault and
a suitable drug combination to target the fault. To test our method, we focused on the
growth factor (GF) signaling pathways, which are often associated with proliferation
of cancer. The GRN is modeled using Boolean logic gates and all possible single
faults are enumerated. All drug combinations are also modeled, to determine the
effectiveness of different drug combinations towards each fault.
The method proposed in [ 5 ] is an ATPG technique in principle. Our approach
is similar to [ 5 ] in that it uses the BN and models cancer as faults in the network.
However, the differences are several. Instead of explicit enumeration of the BN,
we use an extensible, implicit SAT-based ATPG approach to efficiently model and
identify faults, and perform drug selection. Further, unlike [ 5 ], we include weighted
clauses for outputs and drugs in the SAT formulation. Using this, the algorithm
can implicitly and efficiently determine the drug combination which is maximally
effective. Finally, our approach can handle multiple faults easily. The runtimes of
our approach are typically much less than a second per set of faults.
In the past, ATPG has been extensively studied in research and industry. One such
ATPG technique is the SAT-based ATPG [ 7 ], [ 8 ], [ 9 ] which translates the testing
condition into a SAT instance that retains the circuit structure. A test for the fault can
then be found by invoking a SAT solver. In the context of cancer therapy, we extend
the SAT based approach to handle drugs and multiple faults.
SAT-based approaches have been applied to the analysis of GRNs and Boolean
networks. In [ 2 ], [ 10 ], SAT-based approaches are presented to infer gene predictors
and determine gene function from gene expression data using a BN model. Another
SAT-based approach for GRN inference is presented in [ 11 ]. Assuming an asyn-
chronous logical description of the GRN, [ 11 ] expresses GRN constraints into a
Boolean formula, from which they infer parameters of the GRN. While in [ 12 ], an
algorithm is presented to find all attractors in a Boolean network based on a SAT-
based bounded model checking. This algorithm uses a SAT-solver to identify paths of
a particular length in the state-transition graph of a Boolean network. In these previ-
ous works, SAT has been used to infer the GRN. This fundamentally differs from our
work which uses SAT to simulate the faulty GRN and control the GRN using drugs.
Control of Boolean networks has been studied from a theoretical standpoint in
[ 13 ] and using a model checking algorithm in [ 14 ]. In these papers, a BN with control
nodes is given, and the control strategy denotes a sequence of control signals that
deterministically drive the BN from a given initial state, to a desired final state, in t
time steps. Conceptually, our SAT-based ATPG approach is similar to these methods
of Boolean network control, in that we construct a SAT formula to check whether
a selection of drugs can drive the system to a desired state. However we differ in a
few key areas. First, our approach considers the BN under a stuck-at fault model, in
that one or more of the genes can be faulty. This model allows us to apply ATPG
techniques to identify faulty genes in the BN which can lead to undesired GRN
behavior. And secondly, our approach assigns weights to the drugs and the outputs in