Repairing Boolean regulatory networks using Maximum Satisfiability

Abstract

Models of biological regulatory networks are increasingly used to formally describe and understand complex biological processes. Such models are often repaired whenever new observations become available, because the model cannot generate behaviours consistent with the new observations, or because the behaviours are contradictory. This process of model repair is often manual and therefore prone to errors. In this work, we describe biological regulatory networks using the Boolean logical formalism, where nodes are represented by Boolean variables denoting biological components and edges denote regulatory interactions between components. The evolution of each variable is defined by a Boolean logical function depending on the values of the regulators of the component. Here, we propose to repair the model by changing inconsistent functions, with four types of atomic repairs which can be further combined. The goal is to find the cardinality minimal set of repairs allowing the model to satisfy all available observations. The proposed method is implemented using Maximum Satisfiability (MaxSAT) and is tested using data from Escherichia coli and Candida albicans organisms. The system finds optimal solutions to ensure consistency for all observations.

Downloads

• Program to generate the CNF encoding based on a network written in ASP (jar+code)
• Program to transform the CNF result into a human readable file (jar+code)
• Both programs require the use of java
• Instances in ASP: Escherichia coli [1]
• Sample of encoded instances: Escherichia coli
• MaxSAT Solver: Open WBO

Example of usage

To run the MaxSAT solver on a CNF file:

To use the program you should pass it an influence graph (in the ASP format), an experimental profiles (in the ASP format), the default function and the repair operation. For example:

It is possible to run the program allowing the use of different repair operations:

• Repair e - removes edges
• Repair i - negates the regulators of a function
• Repair n - negates a function
• Repair g - changes AND to OR and NOT to the identity function.

Note: All the combinations of repairs are allowed, and they need to be written in alphabetical order.

In order to convert the result of the solver into a human readable file:

Contacts

If you have any comments or questions, please .

Notes

[1] The data was originally obtained from Repair and Prediction (under Inconsistency) in Large Biological Networks with Answer Set Programming paper.