Application of MaxSATbased ATPG to optimal cancer therapy design
 1.7k Downloads
 2 Citations
Abstract
Background
Cancer and other gene related diseases are usually caused by a failure in the signaling pathway between genes and cells. These failures can occur in different areas of the gene regulatory network, but can be abstracted as faults in the regulatory function. For effective cancer treatment, it is imperative to identify faults and select appropriate drugs to treat the faults. In this paper, we present an extensible MaxSAT based automatic test pattern generation (ATPG) algorithm for cancer therapy. This ATPG algorithm is based on Boolean Satisfiability (SAT) and utilizes the stuckat fault model for representing signaling faults. A weighted partial MaxSAT formulation is used to enable efficient selection of the most effective drug.
Results
Several usage cases are presented for fault identification and drug selection. These cases include the identification of testable faults, optimal drug selection for single/multiple known faults, and optimal drug selection for overall fault coverage. Experimental results on growth factor (GF) signaling pathways demonstrate that our algorithm is flexible, and can yield an exact solution for each feature in much less than 1 second.
Keywords
Gene Regulatory Network Boolean Network Conjunctive Normal Form Sequential Circuit Automatic Test Pattern GenerationBackground
In all organisms, cell function is supported by the interaction of genes and protein products, forming an interconnected network called the gene regulatory network (GRN) [1]. The interaction or communication between genes and cells is highly complex and multivariate. Cancer and generelated diseases are often the result of a failure in the signaling, leading to incorrect gene regulation and its associated functions.
The modeling of the gene interactions is thus highly important for understanding the mechanism and therapy of cancer. Because genes are observed to have a switchlike expression (active or inactive), the Boolean network model [2] has become popular for representing the GRN. In the Boolean network, the genes and biochemical pathways are represented as logic functions, much like logic gates in an integrated circuit (IC). This network can be extended to include signaling failures and defects in the GRN, which are represented as faulty lines in the circuit [3]. The issue of faults in circuits is well understood in electronic testing. For example, in chip manufacturing, circuits are typically tested to check that the IC is defect free before vendoring. Manufacturing defects manifest themselves as logical faults modeled as lines (wires) stuckat '1' or '0'. Using this stuckat fault model, automatic test pattern generation (ATPG) algorithms determine a set of tests (bit vectors on the inputs of the circuit) to test for stuckat faults in the circuit.
In this paper, we use the stuckat fault model for the GRN [3] and employ ATPG techniques to determine a drug vector (set of drugs) to rectify the fault. The ATPG algorithm is developed as a Boolean satisfiability (SAT) based method, where the Boolean network is transformed into a conjunctive normal form (CNF) expression and solved for satisfiability to find the drug vector. In therapy, the goal is to treat the cancer (represented by one or more faults) using drugs with the least negative impact on the patient, ideally by prescribing the fewest number of drugs necessary to avoid unnecessary sideeffects and cost. The SAT method is further extended by assigning weights to the circuit outputs and drug vectors, and solved with a weighted partial MaxSAT to find the optimal set of drugs to fix or rectify the fault.
The key contributions of this paper are:

In contrast to previous approaches [3] which performs an explicit search, we develop an implicit SATbased ATPG approach to model and identify detectable faults (single and multiple) in a Boolean network.

By assigning weights to model output and drug vectors, we use a weighted partial MaxSAT formulation to determine the optimum selection of drugs to rectify a specific fault.

Our approach can be trivially extended to handle multiple faults.

We utilize the above techniques for drug therapy to select the minimum set of drugs to provide the best coverage across all single/multiple faults.
The remainder of this paper is organized as follows. The next section discusses previous work in this area. In the following section, we introduce faultmodeling and Boolean satisfiability and describe our approach for drug therapy. We then present experimental results obtained from applying our methods to a biological example and discuss applications of our algorithm towards sequential circuits. Lastly, we draw some concluding remarks about our SATbased ATPG method.
Previous work
In the actual GRN, the gene expression or protein concentration is continuous. However, in this paper, the Boolean network (BN) [2] is chosen as preferred network for modeling the GRN. There are several reasons for this choice. First, it has been observed that many genes exhibit a switchlike ON/OFF activity in terms of their expression [4]. Second, a discrete model like the BN is relatively simple and easy to analyze and simulate. And lastly, there are many logic synthesis and test algorithms already developed in circuit design and testing that can be applied to the Boolean network.
In [3], 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 arise 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. This paper 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 were also simulated to determine the effectiveness of drug combinations towards each fault.
The method proposed in [3] is an ATPG technique in principle. Our approach is similar to [3] 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 SATbased ATPG approach to efficiently model and identify faults, and perform drug selection. Further, unlike [3], 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 SATbased ATPG [5, 6, 7] 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.
SATbased approaches have been applied to the analysis of GRNs and Boolean networks. Assuming an asynchronous logical description of the GRN, [8] presents an approach for expressing GRN constraints into a Boolean formula, from which they infer parameters of the GRN. While in [9], an algorithm is presented to find all attractors in a Boolean network based on a SATbased bounded model checking. This algorithm uses a SATsolver to identify paths of a particular length in the statetransition graph of a Boolean network. In these previous 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 [10] and using a model checking algorithm in [11]. 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 SATbased 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 stuckat 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 weighs the drugs and outputs in the ATPG formulation, allowing for different control strategies depending on desired specifications (i.e. selection with fewest drugs or fewest side effects). Unlike [10, 11], our method can also determine the best drug selection on a BN where the faulty gene location is unknown.
Method
In this section, we present our SATbased ATPG method. Before the method is described in detail, we first provide definitions for fault modeling and Boolean Satisfiability.
Fault terminology
A manifestation of a defect at the abstracted function level is called a fault.
In an IC, the difference between a defect and a fault can be explained as imperfections in the hardware and function, respectively. While in genomics, examples of biological defects can include mutations in the gene activation site, malformation of the protein folding, and problems in the gene product transport. Likewise, an example of a biological fault is a modification of the logical function representing a gene, producing the incorrect output. A stuckat fault is modeled by assigning a fixed (0 or 1) value to a signal line (input or output of a logic gate) in the circuit.
An untestable fault is a fault which no test can detect. Untestable faults appear in two situations.

Faults that are redundant, whose presence does not change the output behavior of the circuit.

Faults that change the output behavior of the circuit, but no test (drug vector in the context of cancer therapy) can be generated to propagate or rectify the fault.
Stuckat fault modeling
In the Boolean network model for a GRN, the activity of genes is modeled as a Boolean circuit. We assume the circuit is modeled as an interconnection of Boolean gates. A stuckat fault is assumed to only affect interconnections (wires or nets) between gates. Each net can have one of two types of faults: stuckat1 or stuckat0 (sa1 and sa0, respectively). Thus, a net with a stuckat0 fault will always have a logic value 0, irrespective of the correct logic output of the gate (gene) driving the net.
Note that drugs are modeled the same as stuckat faults, wherein a drug that inhibits a gene is modeled as a sa0 "fault", while a drug that activates a gene is modeled as sa1 "fault". The gates for drug injection are inserted at the nets of the genes that they target.
Boolean satisfiability
Several ATPG algorithms [5, 6, 7], including the method proposed in this paper are based on Boolean Satisfiability (SAT) and utilize the stuckat fault model. We begin with an overview of SAT, followed by a SATbased formulation of the ATPG problem.
A literal or a literal function is a binary variable x or its negation $\stackrel{\u0304}{x}$.
A clause is a disjunction (logical OR) containing literals (example: $\left(x+\u0233+\stackrel{\u0304}{z}\right)$).
A Conjunctive Normal Form (CNF) expression S consists of a conjunction (AND) of m clauses c_{1} ... c_{ m }. Each clause c_{ i } consists of disjunction (OR) of k_{ i } literals. A CNF S is satisfied if it evaluates to 1. Satisfying S is equivalent to satisfying all c_{ i } ∈ S
Given a Boolean formula S (on a set of binary variables X) expressed in CNF, the objective of SAT is to identify an assignment of the binary variables in X that satisfies S, if such an assignment exists.
For example, consider the formula $S\left(a,b,c\right)=\left(a+\stackrel{\u0304}{b}\right)\cdot \left(a+b+c\right)$. This formula consists of 3 variables, 2 clauses, and 4 literals. This particular formula is satisfiable, and a satisfying assignment is (a,b,c) = (0,0,1) or $\u0101\stackrel{\u0304}{b}c$. There are several extensions to the SAT problem. One such extension of interest is AllSAT. For a SAT formula, there may exist many satisfying assignments. The objective of AllSAT is to find all satisfying assignments. Another useful extension is Weighted partial MaxSAT (WPMS) which aims to satisfy a partial set of clauses. In WPMS, each clause in the CNF is identified as a hard clause or soft clause. Each soft clause is associated with a weight. The problem then is to identify an assignment that satisfies all hard clauses while maximizing the total weight of the satisfied soft clauses.
SATbased formulation for stuckat fault model
In the SAT based ATPG method, we first generate a formula in CNF to represent tests for the fault. To do so, the circuit from the stuckat fault model must be converted to a CNF. Every gate (g_{ i }) of the circuit has CNF formula (G_{ i }) associated with it, which represent the function performed by the gate. The formula is true iff the variables representing the gate's inputs and outputs take on values consistent with its truth table.
When all the sa0 and sa1 variables are set to false (0), the CNF formula S describes the good (faultfree) circuit behavior. The faulty circuit is a copy of the faultfree circuit, with faults (sa0 or sa1 variables) injected at the gates to be affected by faults.
The value of f, the side input to gate g_{3}, determines whether the stuckat 1 fault is activated or now. To activate the fault, f is set true by adding a clause (f) to the CNF, thus S = G 1 · G_{2} · G_{3} · (f). Likewise, to deactivate the fault, f is set false by adding the clause $\left(\stackrel{\u0304}{f}\right)$ to the CNF, thus $S={G}_{\mathsf{\text{1}}}\cdot {G}_{\mathsf{\text{2}}}\cdot {G}_{\mathsf{\text{3}}}\cdot \left(\stackrel{\u0304}{f}\right)$. With our CNF formula for the circuit, we now describe several usage cases employing this CNF in SAT.
Implementation of fault and drug simulation
Case 1: Single stuckat fault identification
In this method, we find all single stuckat faults which are nonredundant, as well as the faulty outputs that they generate. To proceed with this method, we first simulate the original circuit to determine the correct faultfree output. The circuit is simulated using our SAT formulation in the faultfree and drugfree model for a specified primary input value, and the resulting primary output value for the true response is saved as Z^{0}.
Here ${Z}_{i}^{0}$ is the variable corresponding to the i^{ th } output bit.
We now form a new CNF S^{1} = S · C^{1} · C^{2}. The resulting AllSAT on S^{1} is a list of all nonredundant single stuckat faults and their faulty output. These faults are flagged for drug simulation using any of the next three cases.
The results from this case can also be used immediately in several ways. For example, this method classifies for each single stuckat fault whether it is redundant or nonredundant. That is, any fault which is redundant does not produce an incorrect output, and can be ignored from a therapy standpoint. In a second example, the faulty output from the stuckat model can be compared to a previously measured output from expression data, in order to identify which genes are potentially faulty. This information can be used to target genes for potential drug development, avoiding genes that are untestable.
Case 2: Fault rectification with fewest drugs
In the presence of a particular fault, the problem is determining whether a selection of drugs can rectify the circuit, i.e. change the faulty output to the correct output. If this is not possible, we want to obtain the "best" or "closest" output to the correct output, by using drugs. To do this, we guide the WPMS solver by assigning weights to the output states. For example, in the GF network used in our experiments, the faultfree output Z^{0} is assigned the highest weight (80) and remaining output states are assigned decreasing weights (70, 60, 50, etc.) based on increasing Hamming distance (1, 2, 3, etc.) from the faultfree output. We assume that faulty states that have a larger Hammingdistance have a more pronounced cancer proliferative effect.
Additionally, the selection of drugs to achieve the best output should use the least number of drugs to minimize the sideeffects on the patient. To incorporate this in the WPMS solver, each drug that is not selected is given a weight of 1. The GF network example has 6 drugs, thus if no drugs are selected, then the cumulative drug weight is 6. Likewise, if all drugs are selected, the drug weight is 0.
Note that the output and drug weights are assigned in such a way as to avoid the situation where a lessdesirable output (with few drugs) is chosen over a higher weight output with more drugs. We assume that from a clinical standpoint, the priority is to first produce the best possible output, and secondarily to use the fewest drugs required for that output.
All faulty circuits with nonredundant faults from Case 1 are augmented with the output and drug weights and simulated using WPMS. The WPMS solver will implicitly and deterministically find the assignment of drugs that achieves the best possible output and with the fewest drugs. The output values, selected drugs, and highest weight of the fault+drug circuits are recorded and compared with the drugfree circuits. An immediate result from this method is that a fault where the fault+drug circuit which obtains its best output with zero drugs is in fact an untestable fault, wherein no drug combination can improve the output.
In general, several stuckat faults can be simultaneously present in the circuit. A circuit with n lines can have 3^{ n }  1 possible stuck line combinations. This is because each line can be in one of the three states: sa1, sa0, or faultfree. All combinations (except one which has all lines in their faultfree state) are counted as faulty. In our implementation, multiple stuckat faults can easily be modeled for rectification, by setting one or more lines to their faulty state.
Case 3: Fault rectification with minimal drug cost
In the previous case, all drugs are equal in terms of their weight. However, there may be a situation where we would want to differentiate the drugs based on some cost function based on characteristics such as price, number of sideeffects, or ease of availability. For example, two drugs with few sideeffects may be more desirable than one drug with many sideeffects, if both drug selections produce the same output. As such, in the presence of a particular faulty circuit and desired output, the problem is determining a selection of drugs with lowest total cost.
Each drug that is not selected is given a weight proportional to its cost. In our example, we use the number of sideeffects as the drug's cost. All faulty circuits with detectable faults from Case 2 are modified with the new drug weights. In addition, the output of the circuit is fixed to the best output as determined in Case 2. These circuits are then solved using WPMS to obtain the selected drugs with lowest cost.
Case 4: Determining therapy with fewest drugs and best coverage
From Case 2, we identify the drug selection that best rectifies a certain fault. However, in drug therapy, the fault location may be unknown. In this situation, a drug selection that rectifies all faults (or as many faults as possible) with the fewest drugs, is desirable.
For each faulty circuit (with a single fault), we find all combinations of 1, 2, and 3 drugs that yield the best output from Case 2. This is done by performing a WPMS AllSAT to find all satisfying drug selections with drug weight greater than or equal to d  3, where d is the total number of drugs. Each drug selection (or vector) is analyzed to see how many testable faults are rectified or covered by it. The drug vector with the highest coverage and fewest drugs is recorded as a best candidate for therapy.
Results
Model implementation
We evaluate the WPMSbased ATPG methods on the GRN that models growth factor (GF) pathways [3]. In multicellular organisms, cell growth and replication is tightly controlled by the cell cycle control. This system receives signals from other cells which are used to decide whether the cell should grow. A failure in these signals can lead to unwanted or unregulated cell growth, leading to cancer. These signaling pathways are well studied, and several drugs have been developed to target different pathways for cancer therapy.
In the results, stuckat faults are referred by the net numbers that are affected (i.e. net 7 sa0, means that the signal corresponding to net 7 is stuckat 0). The network has 5 primary input (PI) signals and 7 primary output (PO) signals. The PIs will be defined as a 5bit binary vector X = [EGF,HBEGF,IGF,NRG1,PTEN], while the POs will be defined as a 7bit binary vector Z = [FOS  JUN,SP 1,SRF  ELK 1,SRF  ELK 4,BCL 2,BCL 2L 1,CCND 1]. In all tests, the PIs are fixed to X = 00001 as this input leads to the nonproliferative output in the faultfree case.
For this network, six drugs are available, defined as a 6bit vector. Each bit corresponds to a drug, such that a value of 1 on the i^{ th } bit indicates that drug i is selected, and a value of 0 indicates that drug i is not selected. The drug vector is D = [lapatinib,AG 825,AG 1024,U 0126,LY 249002,Temsirolimus].
All the methods (Case 1 through 4) were implemented using an opensource weighted partial MaxSAT solver called Maxsatz [12, 13]. Our procedure consists of scripts which take the initial CNF, selects desired fault variables, sets output and drug weights, and solves the CNF using Maxsatz. The satisfying assignments are then parsed for the output and drug vectors, and reported in the results. In all examples listed in this section, the WPMS runtime was significantly less than 1 second per CNF.
Simulation results
Case 1: Single stuckat fault identification
Drug selection for single stuckat faults
Net  sa  Faulty PO  Best PO  Drug Vector  Score 

1  1  1111111  0000000  010000  85 
2  1  1111111  0000000  100000  85 
3  1  1111111  0000000  001000  85 
4  1  1111111  0000000  010000  85 
5  1  1111111  0000000  000110  84 
6  1  0000111  0000000  000110  84 
7  1  0000111  0000111  000000  56 
8  1  1111111  0000000  000010  85 
9  1  0000111  0000000  000010  85 
10  1  0000111  0000111  000000  56 
11  1  0000111  0000111  000000  56 
12  1  0000111  0000111  000000  56 
16  1  0111110  0000000  000100  85 
17  1  0111110  0000000  000100  85 
18  1  0111110  0111110  000000  36 
19  0  0000001  0000001  000000  76 
20  0  0000110  0000000  000001  85 
21  1  0000110  0000000  000001  85 
22  1  0000110  0000000  000001  85 
23  1  0000110  0000110  000000  66 
24  0  0000110  0000110  000000  66 
From this table, we observe that nets 13, 14, and 15 are not listed. The presence of a fault (sa0 or sa1) on these nets does not generate an incorrect PO, and as such, these are redundant faults. From a therapy standpoint, the genes corresponding to these faults can be ignored.
Case 2: Fault rectification with fewest drugs
From the results in Case 1, all nonredundant faults are simulated with drugs. The outputs are first weighted where the faultfree output Z^{0} = 0000000 has a maximum weight of 80 as it represents a nonproliferative output. All remaining output vectors are given weights of 80  10h, where h is their Hamming distance from the faultfree output. The drugs are also given weights where the nonselection of a drug has a weight of 1. With six drugs, the maximum score is therefore 80 + 6 = 86.
Table 1 shows for each nonredundant stuckat fault, the best output (Column 4), the drug vector to achieve such output (Column 5), and the weight score (Column 6). We observe that for many faults, there exists a drug vector that can completely rectify the fault, and produce a faultfree circuit. Additionally, the corresponding reported drug vector is minimal in the number of drugs used, which is desirable in therapy usage. We also determine that faults on nets 7, 1015, 18, 19, 23, and 24 are untestable, as no combination of drugs can produce a change in the output. This can be explained as there are no drugs on the fanout of these genes to rectify the fault.
Drug selection for multiple stuckat faults
Net  sa  Faulty PO  Best PO  Drug Vector  Score 

1,21  1,1  1111111  0000000  010001  84 
4,9  1,1  1111111  0000000  000001  85 
5,19  1,0  1111111  0000001  000110  74 
6,8  1,1  1111111  0000000  000110  84 
7,20  1,1  0000111  0000111  000000  56 
8,21  1,0  0000111  0000000  000010  85 
13,16  1,1  1111110  0000000  000100  85 
1,3,6  1,0,1  1111111  0000000  000110  84 
2,14,20  1,1,0  1111111  0000000  100001  84 
4,7,17  1,1,1  1111111  0000111  010100  54 
4,12,23  1,1,1  1111111  0000111  010000  55 
8,9,11  1,1,1  0000111  0000111  000000  56 
8,9,21  1,1,0  0000111  0000000  000010  85 
12,18,20  0,0,0  0000110  0000000  000001  85 
15,17,21  0,0,1  0000110  0000000  000001  85 
Case 3: Fault rectification with minimal drug cost
When selecting drugs, there may be multiple drug combinations that may rectify a fault, but where each drug has a different associated cost. We first assign weights to drugs, according to their cost. For this paper, we use the number of sideeffects as the drug's cost. Drugs AG825, lapatinib, Temsirolimus are assigned weights of 10, 15, and 35, respectively, which correspond to their approximate number of sideeffects [14, 15]. However, drugs AG1024, U0126, and LY294002 have yet to under go clinical trial and the number of sideeffects is unknown. As such, these drugs are assigned a weight 20, which is an average of the 3 previous weights.
In this GF example, Case 3 simulation provides the same results as in Case 2. This is due to a lack of drugs that share paths in the circuit. In fact, for almost every nonredundant fault, the best output state can only be achieved through one drug vector.
Case 4: Determining therapy with fewest drugs and best coverage
Drug selection count and fault coverage
Drug Vector  Count  Coverage  Drug Vector  Count  Coverage 

000001  3  23%  000111  13  100% 
000010  2  15%  001011  6  46% 
000100  2  15%  001101  6  46% 
001000  1  8%  001110  10  77% 
010000  2  15%  010011  7  54% 
100000  3  23%  010101  7  54% 
000011  5  38%  010110  10  77% 
000101  3  23%  011001  6  46% 
000110  10  77%  011010  5  38% 
001001  4  31%  011100  5  38% 
001010  3  23%  100011  8  62% 
001100  3  23%  100101  8  62% 
010001  5  38%  100110  10  77% 
010010  4  31%  101001  7  54% 
010100  4  31%  101010  6  46% 
011000  3  23%  101100  6  46% 
100001  6  46%  110001  6  46% 
100010  5  38%  110010  5  38% 
100100  5  38%  110100  5  38% 
101000  4  31%  111000  4  31% 
110000  3  23% 
From these results, we observe that with only 1 drug selected, the best coverage is only 23% of faults using lapatinib (d_{1}) or Temsirolimus (d_{6}). When allowing for 2 drugs, coverage increases to 77% using the drug combination of U0126 (d_{4}) and LY294002 (d_{5}). Finally, we achieve 100% coverage of all testable faults when using the 3 drug combination of U0126 (d_{4}), LY294002 (d_{5}), and Temsirolimus (d_{6}). When the single stuckat fault location is unknown, these selected drug combinations will be the most effective for therapy and for preventing the proliferation of cancer.
Discussion
One consideration for the sequential ATPG is the initialization of state in the first time frame. Ideally a known state should be used, such as one obtained from a previous microarray expression measurement. An alternative is to use an attractor state. In the longterm behavior, the dynamics of the BN transition to the attractors (attractor cycles), thus using an attractor state is a reasonable starting state for therapy.
The complexity of applying SATbased ATPG to sequential circuits depends on the length of timeframe expansion. For a circuit with k variables in its SAT formulation, each frame increases the number of variables by k. The SAT search space is then 2^{ km } for an expanded circuit with m frames. The number of frames for expansion can be bounded. If a subsequence of states has the same first and last state, then the sequence can be stopped. For a BN, the number of frames m can be bounded by the sum of the number of stesps it takes to reach an attractor cycle and the maximum length of the attractor cycles for all combinations of drugs under consideration. In the worst case, the number of frames required would equal to the number of possible states, which is 2^{n+d}for a BN with n target genes and d drugs.
Conclusions
In this paper, we have presented an efficient and extensible SATbased ATPG methodology for cancer therapy. We approach this problem by representing the BN and cancer as a logic circuit stuckat fault model. This circuit, along with the testing conditions, is converted into a CNF. The CNF is then augmented with output and drug vectors weights and solved using a weighted partial MaxSAT solver for four different usage cases: (1) single stuckat fault identification, (2) fault rectification with fewest drugs, (3) fault rectification with minimum drug cost, and (4) determining therapy with fewest drugs and best coverage. We demonstrate these methods on the growth factor signaling pathway, and have presented results that are applicable to cancer therapy. While the GF network example in this paper is a combinational network, our algorithm can easily be extended to address sequential networks, like those found in transcriptional GRNs, by simply unrolling the sequential circuit in time and applying the same methods. Furthermore, all nets, inputs, outputs, and drugs can be assigned weights, which can be made variable, allowing the user to finetune the network or design therapies for any number of test situations.
Notes
Acknowledgements
Based on “Efficient cancer therapy using Boolean networks and MaxSATbased ATPG”, by PeyChang K Lin and Sunil P Khatri which appeared in Genomic Signal Processing and Statistics (GENSIPS), 2011 IEEE International Workshop on. © 2011 IEEE [18].
This article has been published as part of BMC Genomics Volume 13 Supplement 6, 2012: Selected articles from the IEEE International Workshop on Genomic Signal Processing and Statistics (GENSIPS) 2011. The full contents of the supplement are available online at http://www.biomedcentral.com/bmcgenomics/supplements/13/S6.
References
 1.Guelzim N, et al: Topological and causal structure of the yeast transcriptional regulatory network. Nature Genetics. 2002, 31: 6063. 10.1038/ng873.CrossRefPubMedGoogle Scholar
 2.Kauffman SA: Metabolic stability and epigenesis in randomly constructed genetic nets. Journal of Theoretical Biology. 1969, 22 (3): 437467. 10.1016/00225193(69)900150.CrossRefPubMedGoogle Scholar
 3.Layek R, Datta A, Bittner M, Dougherty E: Cancer therapy design based on pathway logic. Bioinformatics. 2011, 27 (4): 548555. 10.1093/bioinformatics/btq703.CrossRefPubMedGoogle Scholar
 4.Jacob F, Monod J: Genetic regulatory mechanisms in the synthesis of proteins. Journal of Molecular Biology. 1961, 3 (3): 318356. 10.1016/S00222836(61)800727.CrossRefPubMedGoogle Scholar
 5.Larrabee T: Efficient Generation of Test Patterns Using Boolean Difference. Proc of the Intl Test Conf. 1989, 795801.CrossRefGoogle Scholar
 6.Stephan P, Brayton R, SangiovanniVincentelli A: Combinational Test Generation Using Satisfiability. ComputerAided Design of Integrated Circuits and Systems, IEEE Transactions on. 1996, 15 (9): 11671176. 10.1109/43.536723.CrossRefGoogle Scholar
 7.Saluja N, Gulati K, Khatri S: SATbased ATPG using multilevel compatible don'tcares. ACM Trans Des Autom Electron Syst. 2008, 13: 24:124:18.CrossRefGoogle Scholar
 8.Corbin F, Bordeaux L, Hamadi Y, Fanchon E, Trilling L: A SATbased approach to decipher Gene Regulatory Networks. 2007, [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.71.1999]Google Scholar
 9.Dubrova E, Teslenko M: A SATBased Algorithm for Finding Attractors in Synchronous Boolean Networks. IEEE/ACM Trans Comput Biol Bioinform. 2011, 8 (5): 13931399.CrossRefPubMedGoogle Scholar
 10.Akutsu T, Hayashida M, Ching W, Ng M: Control of Boolean networks: Hardness results and algorithms for tree structured networks. Journal of Theoretical Biology. 2007, 244 (4): 670679. 10.1016/j.jtbi.2006.09.023.CrossRefPubMedGoogle Scholar
 11.Langmead C, Jha S: Symbolic approaches for finding control strategies in Boolean Networks. Journal of Bioinformatics and Computational Biology. 2009, 7: 323338. 10.1142/S0219720009004084.CrossRefPubMedGoogle Scholar
 12.
 13.Li C, Manya F, Mohamedou N, Planes J: Exploiting Cycle Structures in MaxSAT. Theory and Applications of Satisfiability Testing  SAT 2009, Volume 5584 of Lecture Notes in Computer Science. Edited by: Kullmann O. 2009, Springer Berlin/Heidelberg, 467480.Google Scholar
 14.Santa Cruz Biotechnology, Inc. [http://www.scbt.com/]
 15.PubMed Health Home. [http://www.ncbi.nlm.nih.gov/pubmedhealth/]
 16.Faryabi B, Chamberland JF, Vahedi G, Datta A, Dougherty E: Optimal Intervention in Asynchronous Genetic Regulatory Networks. IEEE Journal of Selected Topics in Signal Processing. 2008, 2 (3): 412423.CrossRefGoogle Scholar
 17.Abramovici M, Breuer MA, Friedman AD: Digital Systems Testing and Testable Design. 1990, Computer Science PressGoogle Scholar
 18.Lin PK, Khatri SP: Efficient cancer therapy using Boolean networks and MaxSATbased ATPG. Genomic Signal Processing and Statistics (GENSIPS), 2011 IEEE International Workshop on: 46 December 2011. 2011, 8790. 10.1109/GENSiPS.2011.6169450.CrossRefGoogle Scholar
Copyright information
This article is published under license to BioMed Central Ltd. This is an open access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/2.0), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.