A SAT-based algorithm for finding attractors in synchronous Boolean networks

Area of Science:

• Computational Biology
• Systems Biology
• Network Science

Background:

• Synchronous Boolean networks are used to model complex biological systems.
• Existing methods for finding attractors (stable states) in these networks have limitations in capacity or completeness.
• Boolean decision diagram (BDD) methods require excessive memory, while simulation-based methods are incomplete.

Purpose of the Study:

• To develop a more efficient and complete algorithm for identifying all attractors in synchronous Boolean networks.
• To overcome the limitations of existing Boolean decision diagram and simulation-based approaches.
• To enable the analysis of larger and more complex biological network models.

Main Methods:

• A novel algorithm employing SAT-based bounded model checking is presented.
• The algorithm's efficiency is assessed using seven real biological process network models.
• Performance is further evaluated on 150,000 randomly generated Boolean networks ranging in size from 100 to 7,000 nodes.

Main Results:

• The proposed SAT-based algorithm demonstrates superior performance compared to existing methods.
• The approach shows potential for handling models an order of magnitude larger than previously feasible.
• Successful identification of attractors in both biological and large-scale random networks was achieved.

Conclusions:

• The SAT-based bounded model checking algorithm offers a scalable and complete solution for attractor detection in synchronous Boolean networks.
• This advancement facilitates more comprehensive systems biology research by enabling the analysis of larger models.
• The method provides a robust tool for understanding the dynamics of complex biological regulatory networks.