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