Fault detection and therapeutic intervention in gene regulatory networks using SAT solvers

Random somatic mutations disrupt homeostasis of the cell resulting in various undesirable phenotypes including proliferation. One of the most important questions in systems medicine research is the therapeutic intervention design, which requires the knowledge of these mutations. A single or multiple mutations can occur in the diseases like cancer. These mutations have been successfully modeled as stuck-at faults in the Boolean network model of the underlying regulatory system. Identification of these fault types for multiple stuck-at faults is a non-trivial problem and requires some system theoretic introspection. This manuscript addresses the dual problem of the fault identification and the therapeutic intervention. Both the problems are mapped to the Boolean satisfiability (SAT) problem. The underlying problems are solved using a fast SAT solver. The synthetic and biological examples elucidate the effectiveness of the mapping.