中文摘要：

环是布尔网络状态转换过程中的稳定态,在模式检测、基因调控网络和可达性分析等领域都有重要的意义。计算布尔网络状态转换中的所有环是一个NP完全问题。该文基于全解布尔满足性判定（SAT）算法,设计了一种求解所有小于等于指定步长环的算法。算法基于布尔网络的状态转换函数和状态环属性生成合取范式形式（CNF）的问题集,通过融合冲突子句学习（CDCL）、非时序回退、阻塞子句和变量分类等技术,降低算法的计算复杂度。实验结果表明,该算法能够高效地计算指定步长的环。对于无法计算所有环的复杂网络,指定步长计算环的方式将更有应用价值。

英文摘要：

A cycle which is a steady state in Boolean network state transition is important in modeling checking, genetic regulatory networks and reachability analysis. Obtaining all the cycles in Boolean network state transition is a NP complete problem. In this paper, we proposes an algorithm for solving all the cycles which have less than or equal to the assigned step length based on all-solution Boolean satisfiability （SAT） algorithm. By extending the state transition function of a Boolean network and the property of cycles, this algorithm creates a problem set in conjunctive normal form （CNF） and incorporates techniques such as conflict-driven clause learning （CDCL）, non-chronological backtracking, blocking clause and variable classification to decrease computational complexity. Experiment result shows that this algorithm is efficient for solving the cycles. For large scale complex network that is hard to get all the cycles, this algorithm delivers more practical value.