SAT-based Computation Of Minimal Cut Sets

Fault tree analysis(FTA)is a prominent reliability analysis method widely used in safety-critical industries.Computing minimal cut sets(MCSs),i.e.,finding all the smallest combination of basic events that result in the top level event,plays a fundamental role in FTA.Computation of MCSs is heterogeneous in themselves because of the huge scale and complex structure of the industrial fault trees,which makes this issue a hot topic both in academia and industry.Classical methods have been proposed based on manipulation of Boolean expressions of fault trees and Binary Decision Diagrams.However,given the inherent intractability of computing MCSs,there are still some limitations to these methods.Therefore,motivated by recent progress on modern SAT solver,we present a new method for computing MCSs based on SAT solving.The content of this paper is divided into three parts.The details are as follows.Firstly,we propose a basic algorithm of SAT-based computation of MCSs –SATMCS.SATMCS searches MCSs of the fault tree by continuous iteration likely Davis-Putnam-Loveland-Logeman(DPLL).By means of a heuristic strategy,SATMCS can avoid traversing the entire search space of the fault tree and improve the efficiency.The main innovations of SATMCS include the following.(a)Tseitin coding the fault tree not only improves the coding efficiency,but also keeps the structural features of the fault tree which contributes to the construction of a heuristic search strategy.(b)The algorithm of MCSs extraction based on the cover of cut sets,extracts all the MCSs by computing a lot of approximate MCSs in continuous iteration.(c)Based on the multiple priority independent heuristic assignment strategy,SATMCS can make use of structural features of the fault tree to search MCSs more instructively.Secondly,by analyzing the performance of SATMCS,we clarify that the bottleneck of SATMCS depends on the approximation of the MCS obtained in each iteration.In order to completely solve this problem,SATMCS is optimized – SATMCS-Pro.SATMCS-Pro still keeps a similar SATMCS searchbased MCSs computing process and the fundamental change is the MCSs extraction algorithm.Specifically,given a fault tree,SATMCS-Pro iteratively search for a cut set based on the DPLL framework.By exploiting local failure propagation paths in the fault tree,we provide efficient algorithms for extracting a MCS from the cut set.The information about a new MCS is learned as a blocking clause for SAT solving,which helps to prune search space and ensures completeness of the results.SATMCS-Pro's innovations include the following.(a)An incremental determination process of the cut set is proposed to improve the efficiency of finding a cut set.(b)An algorithm of MCSs extraction based on local propagation graph is proposed to compute MCSs accurately and efficiently.(c)SATMCS-Pro can increasingly learn the information about the conflict clauses generated in DPLL and the block clauses of MCSs,which speeds up the pruning search space;(d)We capture the distribution rule of MCSs.In addition,SATMCS-Pro adopts jump-chronological backtracking strategy to improve the information sharing between two iterations and optimize the search.Finally,we have implemented a tool for computing all MCSs of a fault tree – NUAAFTA that can be powered by SATMCS or SATMCS-Pro.We assess the performance of SATMCS-Pro in this paper through four classes of experiments.From the experiments,we can conclude that SATMCS-Pro possesses excellent ability to compute all MCSs.Preliminary results show that our method exhibits comparable with commercial software on time and memory usage,and even better than some commercial software.