|
|
- 2015
基于满足性判定的布尔网络环求解算法
|
Abstract:
环是布尔网络状态转换过程中的稳定态,在模式检测、基因调控网络和可达性分析等领域都有重要的意义。计算布尔网络状态转换中的所有环是一个NP完全问题。该文基于全解布尔满足性判定(SAT)算法,设计了一种求解所有小于等于指定步长环的算法。算法基于布尔网络的状态转换函数和状态环属性生成合取范式形式(CNF)的问题集,通过融合冲突子句学习(CDCL)、非时序回退、阻塞子句和变量分类等技术,降低算法的计算复杂度。实验结果表明,该算法能够高效地计算指定步长的环。对于无法计算所有环的复杂网络,指定步长计算环的方式将更有应用价值。
| [1] | MCMILLAN K L. Applying SAT methods in unbounded symbolic model checking[C]//14th International Conference on Computer Aided Verification. Denmark: Springer, 2002. |
| [2] | CHAUHAN P, CLARKE E M, KROENING D. Using SAT based image computation for reachability analysis[M]. The Netherlands: Springer, 2003. |
| [3] | GUO W, YANG G, WU W, et al. A parallel attractor finding algorithm based on Boolean satisfiability for genetic regulatory networks[EB/OL]. [2014-01-03] http://journals. plos.org/plosone/article?id=10.1371/journal.pone.0094258. |
| [4] | ZHAO Q. A remark on "scalar equations for synchronous boolean networks with biological applications" by C. Farrow, J. Heidel, J. Maloney, and J. Rogers[J]. IEEE Transactions on Neural Networks, 2005, 16(6): 1715-1716. |
| [5] | T AKUTSU, S KOSUB, A A MELKMAN, et al. Finding a periodic attractor of a Boolean network[J]. Transactions on Computational Biology and Bioinformatics, 2012, 9(5): 1410-1421. |
| [6] | DUBROVA E, TESLENKO M. A SAT-based algorithm for finding attractors in synchronous Boolean networks[J]. Transactions on Computational Biology and Bioinformatics (TCBB), 2011, 8(5): 1393-1399. |
| [7] | ZHENG De-sheng, YANG Guo-wu, LI Xiao-yu, et al. An efficient algorithm for computing attractors of synchronous and asynchronous Boolean networks[EB/OL]. [2014-01-01] http://journals.plos.org/plosone/article?id=10.1371/journal.pone.0060593. |
| [8] | BRAUER J, KING A, KRIENER J. Existential quantification as incremental SAT[C]//23rd International Conference on Computer Aided Verification. Snowbird UT, USA: Springer, 2011. |
| [9] | LIMA J F. Boolean satisfiability solvers: Techniques, implementations and analysis[J]. Electrónica e Telecomunica？？es S. A., 2013, 5(2): 218-225. |
| [10] | GRUMBERG O, SCHUSTER A, YADGAR A. Memory efficient all-solutions SAT solver and its application for reachability analysis[C]//5th international confrence on Formal Methods in Computer-Aided Design. Texas, USA: Springer, 2004. |
| [11] | YU Y, SUBRAMANYAN P, TSISKARIDZE N, MALIK S. All-SAT using minimal blocking clauses[C]//27th International Conference on VLSI Design and 13th International Conference on Embedded Systems. Mumbai, India: IEEE, 2014. |
| [12] | EEN N, SORENSSON N. Minisat 2.2.0[CP/DK]. [2014-02-02]. http://minisat.se/downloads/minisat-2.2.0.tar.gz. |
