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

作     者：赵相福 欧阳丹彤 

作者机构：吉林大学计算机科学与技术学院吉林长春130012 吉林大学符号计算与知识工程教育部重点实验室吉林长春130012 

出 版 物：《电子学报》 (Acta Electronica Sinica)

年 卷 期：2009年第37卷第4期

页      面：804-810页

核心收录：

学科分类：08[工学] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金重大项目(No.60496320 60496321) 国家自然科学基金(No.60773097 60873148) 新世纪优秀人才支持计划 吉林省科技发展计划(No.20060532 20080107) 欧盟项目(No.TH/AsiaLink/010(111084)) 吉林大学"985工程"研究生创新基金(No.20080115) 

主　　题：基于模型的诊断 冲突集 可满足性 SAT求解器 启发式 

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