使用SAT求解器产生所有极小冲突部件集

Deriving All Minimal Conflict Sets Using Satisfiability Algorithms

产生所有的极小冲突部件集为基于模型诊断中的一个重要步骤.本文将待诊断系统的行为模型及观测分别使用合取范式(CNF)形式的文件描述,从而提出将判定系统组件子集是否为冲突集的问题转化为:首先提取相关组件的CNF模型及观测,然后调用成熟的SAT求解器判定可满足性.随后,通过有效地结合CSISE-tree等方法来产生所有的极小冲突集.为进一步提高效率,给出了充分利用系统输入/输出结构信息的启发式策略.实验结果表明,使用结合SAT求解器及CSISE-tree等方法能够较快产生所有极小冲突集,并且启发式策略使得求解效率进一步提高(平均提高约21%,最高者甚至达到约48%).

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. Ftrstly 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 he 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.