• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

Computer Engineering & Science

Previous Articles     Next Articles

Computing minimal cut sets of fault tree using SAT solver

LUO Wei-lin,WEI Ou,HUANG Ming-yu   

  1. (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)
  • Received:2016-12-10 Revised:2017-02-13 Online:2017-04-25 Published:2017-04-25

Abstract:

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.

Key words: fault tree analysis, safety analysis, minimal cut set, Boolean satisfiability problem