首页 | 本学科首页   官方微博 | 高级检索  
     

结合问题特征利用SE-Tree反向深度求解冲突集的方法
引用本文:欧阳丹彤,刘伯文,周建华,张立明. 结合问题特征利用SE-Tree反向深度求解冲突集的方法[J]. 电子学报, 2017, 45(5): 1175. DOI: 10.3969/j.issn.0372-2112.2017.05.021
作者姓名:欧阳丹彤  刘伯文  周建华  张立明
作者单位:1. 吉林大学计算机科学与技术学院,吉林长春 130012;符号计算与知识工程教育部重点实验室(吉林大学),吉林长春 130012;2. 吉林大学软件学院,吉林长春 130012;符号计算与知识工程教育部重点实验室(吉林大学),吉林长春 130012
基金项目:国家自然科学基金,吉林省科技发展计划项目基金,浙江省自然科学基金
摘    要:基于模型诊断是人工智能领域内的一个重要研究方向,求解极小冲突集在基于模型诊断中有着重要应用.在对结合CSISE-Tree求解冲突集方法深入研究的基础上,根据冲突集求解特征重构了结合枚举树的计算冲突集的过程,提出基于深度优先反向搜索求解冲突集的方法.针对CSISE-Tree方法求解时占用内存空间与元件总数指数级相关的缺点,构建反向深度搜索方法减小求解时所占用内存空间;针对CSISE-Tree方法不能对部分非极小的冲突集进行剪枝的问题,给出对非冲突集和更多非极小的冲突集进行剪枝的方法,有效减少了求解时调用SAT(Boolean SATisfiability problem)求解器的次数;实验结果表明,与CSISE-Tree方法相比,本文提出的方法求解效率有明显的提升,并避免了求解时的内存爆炸问题.

关 键 词:基于模型诊断  冲突集  布尔约束可满足  集合枚举树
收稿时间:2015-12-30

A Method of Computing Minimal Conflict Sets Combining the Structure Property with the Anti-depth SE-Tree
OUYANG Dan-tong,LIU Bo-wen,ZHOU Jian-hua,ZHANG Li-ming. A Method of Computing Minimal Conflict Sets Combining the Structure Property with the Anti-depth SE-Tree[J]. Acta Electronica Sinica, 2017, 45(5): 1175. DOI: 10.3969/j.issn.0372-2112.2017.05.021
Authors:OUYANG Dan-tong  LIU Bo-wen  ZHOU Jian-hua  ZHANG Li-ming
Abstract:Model-based diagnosis is an important problem in the field of artificial intelligence.In model-based diagnosis,how to get the minimal conflict sets is a well-known problem with extensive applications.In this paper,according to the characteristics of the conflict sets,we use the enumeration tree to reconstruct the process of solving conflict sets and then design a reverse depth algorithm based on the previous algorithm CSISE-Tree.Firstly,this proposed reverse depth search algorithm can reduce as many memory spaces as possible when obtaining some conflict sets,while CSISE-Tree have to expend some unnecessary memory spaces in this case,where the consume of memory spaces exponentially grows with the number of circuit elements.Secondly,compared with CSISE-Tree,our algorithm can effectively cut down the number of calling the SAT(Boolean SATisfiability problem) solver by pruning some non-minimal conflict sets and non-conflict sets.The experimental results show that our algorithm performs better than its competitor CSISE-Tree in terms of run time in most instances.More importantly,our algorithm avoids the memory explosion when solving some large instances.
Keywords:model-based diagnosis  conflict set  Boolean SATisfiability problem (SAT)  set-enumeration tree(SE-Tree)
本文献已被 万方数据 等数据库收录!
点击此处可从《电子学报》浏览原始摘要信息
点击此处可从《电子学报》下载免费的PDF全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号