基于SAT求解器的故障树最小割集求解算法

摘要

Fault tree analysis is widely used in the safety analysis of safety crisis areas such as nuclear industry,aerospace engineering,traffic control,etc.It is the key step to solve the minimal cut sets of fault tree in fault tree analysis.The conventional algorithms solving the minimal cut sets of large-scale fault tree are mainly based on the binary decision diagram.Their main drawback is that the time and space consumption of the algorithm relies heavily on a good order of variables.In order to reduce the storage resources and speed up the process,we propose a new algorithm based on Boolean satisfiability problem to solve the minimal cut sets in fault tree analysis.Firstly,we convert this problem into a Boolean satisfiability problem.Secondly,the SAT solver is used to solve the minimal satisfiability of the Boolean formula,namely the minimal cut sets of the fault tree,through the iteration of above processes.Experimental results show that compared with conventional algorithms,this new algorithm is not only more accurate but also more efficient for solving the minimal cut sets in fault tree analysis.%故障树分析广泛应用于核工业、航空航天和交通控制等安全攸关领域的安全性分析.求解故障树的最小割集是故障树分析的关键步骤.目前,对于大规模故障树的最小割集的求解方法主要是将故障树转化为二元决策图之后求解,其主要缺点在于算法在时间和空间上的消耗严重依赖良好的变量顺序.为了减少存储资源并加快求解速度,提出了一种基于可满足性问题的故障树最小割集求解算法.首先,将求解故障树最小割集问题转化为求解布尔可满足性问题.然后,利用可满足性问题求解器,通过迭代分析求得最小可满足解集合,即为对应故障树的最小割集.实验表明,本文算法求得的最小割集准确、有效并且在空间和时间上的消耗均要优于传统的基于二元决策图的故障树最小割集求解算法.