BNS is a software tool for computing attractors in Boolean Networks with Synchronous update.
Synchronous Boolean networks  are used for the modeling of genetic regulatory networks.
BNS implements the algorithm presented in 
which is based on a SAT-based bounded model checking.
BNS uses much less space compared to BooleNet or other BDD-based approaches for computing attractors.
It can handle several orders of magnitude larger networks.
BNS reads in a Boolean network description represented in a .cnet format similar to the
Berkeley Logic Interchange Format (BLIF) format commonly used in synthesis
and verification tools and prints out the set of network's attractors.
NEWS: BNS has been extended to the new version, 1.3 (February 2017). This version enables two additional options:
The first option can drastically reduce runtime. It is usefull when unrestricted search is unfeasible. The introduction of this option was motivated by a new application we found for BNS, see . The second option does not impact the result, but might increase or reduce total runtime, depending on the Boolean network.
- Restricting search to attractors of a given length only, and
- Setting initial unfolding of the transition relation to a specified number of levels instead the default one.
BNS1.3 pre-compiled executables are available for the following platforms:
Save the binary for you platform as a file. For Linux and Mac, you will need to make the downloaded file executable by using the command chmode +x bns. For Mac, you might also need to make an exception to open files downloaded from the Web.
NOTE: If antivirus programs on your computer prevents you from downloading executables directly from the Web, then you can download the source code package given below. It contains the same pre-compiled executables.
A package with the source code of BNS1.3 with dependencies is available here. Apart from the source code, the package contains pre-compiled executables for Linus, Mac and Windows and examples of Boolean networks.
User manual for BNS.
TEST INPUT FILES
You can use the following benchmarks to test BNS:
You can also test BNS on randomly generated graphs. Statistical features of randomly generated Boolean
networks on the critical line are believed to capture the dynamics of genetic regulatory networks
of living organisms . The following simple program
will generate you an n-node random Boolean network on the critical line in the .cnet format.
 Boolean Dynamics with Random Couplings, M. Aldana, S. Coopersmith, L. P. Kadanoff, 2002, http://arXiv.org/abs/nlin/0204062.
 "A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks", E. Dubrova, M. Teslenko, IEEE/ACM Transactions on Computational Biology and Bioinformatics, vol. 8, no. 5, 2011, pp. 1393-1399.
 "From Genes to Flower Patterns and Evolution: Dynamic Models of Gene Regulatory Networks",
A. Chaos, M. Aldana, C. Espinosa-Soto, B. G. P. de Leon, A. G. Arroyo, E. R. Alvarez-Buylla,
Journal of Plant Growth Regulation, vol. 25, n. 4, 2006, pp. 278-289.
 "A Method for the Generation of Standardized Qualitative Dynamical Systems of Regulatory Networks", L. Mendoza and I. Xenarios, Journal of Theoretical Biology and Medical Modeling, 2006, vol. 3, no. 13.
 "A Methodology for the Structural and Functional Analysis of Signaling and Regulatory Networks", S. Klamt, J. Saez-Rodriguez, J. A. Lindquist, L. Simeoni, E. D. Gilles, JBMC Bioinformatics, 2006, vol. 7, no. 56.
 "Dynamical Analysis of a Generic Boolean Model for the Control of the Mammalian Cell Cycle", A. Faure, A. Naldi, C. Chaouiya, D. Thieffry, Bioinformatics, 2006, vol. 22, no. 14, pp. e124-e131.
 "Boolean Network Model Predicts Cell Cycle Sequence of Fission Yeast", M. I. Davidich, S. Bornholdt, PLoS ONE. 2008 Feb 27, 3(2):e1672.
 "The Yeast Cell-Cycle Network is Robustly Designed", Fangting Li, Tao Long, Ying Lu, Qi Ouyang, Chao Tang, PNAS April 6, 2004, vol. 101 no. 14, 4781-4786.
 "The Topology of the Regulatory Interactions Predicts the Expression Pattern of the Segment Polarity Genes in Drosophila Melanogaster", R. Albert and H. G. Othmer, Journal of Theoretical Biology, 2003, vol. 223, no. 1, pp. 1-18.
 A SAT-Based Algorithm for Finding Short Cycles in Shift Register Based Stream Ciphers, E. Dubrova, M. Teslenko, Cryptology ePrint Archive, Report 2016/1068, Nov. 2016, https://eprint.iacr.org/2016/1068.pdf.
Department of Electronics, Computer and Software
School of Information and Communication Technology