CSDL Home IEEE/ACM Transactions on Computational Biology and Bioinformatics 2011 vol.8 Issue No.05 - September/October

Issue No.05 - September/October (2011 vol.8)

pp: 1393-1399

Elena Dubrova , Royal Institute of Technology, Stockholm

Maxim Teslenko , Royal Institute of Technology, Stockholm

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TCBB.2010.20

ABSTRACT

This paper addresses the problem of finding attractors in synchronous Boolean networks. The existing Boolean decision diagram-based algorithms have limited capacity due to the excessive memory requirements of decision diagrams. The simulation-based algorithms can be applied to larger networks, however, they are incomplete. We present an algorithm, which uses a SAT-based bounded model checking to find all attractors in a Boolean network. The efficiency of the presented algorithm is evaluated by analyzing seven networks models of real biological processes, as well as 150,000 randomly generated Boolean networks of sizes between 100 and 7,000. The results show that our approach has a potential to handle an order of magnitude larger models than currently possible.

INDEX TERMS

Bounded model checking, SAT, Boolean network, attractor, gene regulatory network.

CITATION

Elena Dubrova, Maxim Teslenko, "A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks",

*IEEE/ACM Transactions on Computational Biology and Bioinformatics*, vol.8, no. 5, pp. 1393-1399, September/October 2011, doi:10.1109/TCBB.2010.20REFERENCES