WAP: 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. 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, developing new methods over different paradigms remains to be an interesting research direction. In this paper, motivated by recent progress on modern SAT solver, we present a new method for computing MCSs based on SAT solving. Specifically, given a fault tree, we 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 an MCS from the cut set. The information of a new MCS is learned as a blocking clause for SAT solving, which helps to prune search space and ensures completeness of the results. We compare our method with a popular commercial FTA tool on practical fault trees. Preliminary results show that our method exhibits better performance on time and memory usage.