| 使用SAT求解器产生所有极小冲突部件集 |
| |
| 引用本文： | 赵相福,欧阳丹彤. 使用SAT求解器产生所有极小冲突部件集[J]. 电子学报, 2009, 37(4): 804-810 |
| |
| 作者姓名： | 赵相福 欧阳丹彤 |
| |
| 作者单位： | 吉林大学计算机科学与技术学院,吉林,长春,130012;吉林大学符号计算与知识工程教育部重点实验室,吉林,长春,130012 |
| |
| 基金项目： | 国家自然科学基金重大项目，国家自然科学基金，教育部新世纪优秀人才支持计划，吉林省科技发展计划，欧盟项目，吉林大学面向21世纪教育振兴行动计划（985计划） |
| |
| 摘 要： | 产生所有的极小冲突部件集为基于模型诊断中的一个重要步骤.本文将待诊断系统的行为模型及观测分别使用合取范式(CNF)形式的文件描述,从而提出将判定系统组件子集是否为冲突集的问题转化为:首先提取相关组件的CNF模型及观测,然后调用成熟的SAT求解器判定可满足性.随后,通过有效地结合CSISE-tree等方法来产生所有的极小冲突集.为进一步提高效率,给出了充分利用系统输入/输出结构信息的启发式策略.实验结果表明,使用结合SAT求解器及CSISE-tree等方法能够较快产生所有极小冲突集,并且启发式策略使得求解效率进一步提高(平均提高约21%,最高者甚至达到约48%).
|
| 关 键 词： | 基于模型的诊断 冲突集 可满足性 SAT求解器 启发式 |
| 收稿时间： | 2008-04-10 |
Deriving All Minimal Conflict Sets Using Satisfiability Algorithms |
| |
| ZHAO Xiang-fu,OUYANG Dan-tong. Deriving All Minimal Conflict Sets Using Satisfiability Algorithms[J]. Acta Electronica Sinica, 2009, 37(4): 804-810 |
| |
| Authors: | ZHAO Xiang-fu OUYANG Dan-tong |
| |
| Affiliation: | 1.School of Computer Science and Technology;Jilin University;Changchun;Jilin 130012;China;2.Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education;China |
| |
| Abstract: | 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 a... |
| |
| Keywords: | model-based diagnosis conflict set satisfiability SAT solvers heuristic |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《电子学报》浏览原始摘要信息 |
|
点击此处可从《电子学报》下载全文 |
