Deriving all minimal consistency-based diagnosis sets using SAT solvers

In this paper, a novel method is proposed for judging whether a component set is a consistency-based diagnostic set, using SAT solvers. Firstly, the model of the system to be diagnosed and all the observations are described with conjunctive normal forms (CNF). Then, all the related clauses in the CNF files to the components other than the considered ones are extracted, to be used for satisfiability checking by SAT solvers. Next, all the minimal consistency-based diagnostic sets are derived by the CSSE-tree or by other similar algorithms. We have implemented four related algorithms, by calling the gold medal SAT solver in SAT07 competition – RSAT. Experimental results show that all the minimal consistency-based diagnostic sets can be quickly computed. Especially our CSSE-tree has the best efficiency for the single- or double-fault diagnosis.