Deriving All Minimal Conflict Sets Using Satisfiability Algorithms
Dantong Ouyang · Dianzi xuebao · 2009
An important step in model-based diagnosis is to derive all minimal conflict sets.In this paper,we propose an approach for judging whether a component set is a conflict set using SAT solvers with some satisfiability algorithms.Firstly the system model and the obtained observations are described in conjunctive normal form.Then all the related clauses of the component set to be considered are extracted,which act as the input of SAT solvers.Hence all the conflict sets can be derived using CSISE-tree or other algorithms combing with a SAT solver.Heuristic strategies are introduced to best suit the input/output structural information of the system.Results show that all the minimal conflict sets can be effectively computed.Besides,the efficiency is greatly improved using heuristic strategies:about 21% and 48% for the average and highest rate respectively.