电子学报 ›› 2017, Vol. 45 ›› Issue (5): 1175-1181.DOI: 10.3969/j.issn.0372-2112.2017.05.021

• 学术论文 • 上一篇    下一篇

结合问题特征利用SE-Tree反向深度求解冲突集的方法

欧阳丹彤1,3, 刘伯文1,3, 周建华2,3, 张立明1,3   

  1. 1. 吉林大学计算机科学与技术学院, 吉林长春 130012;
    2. 吉林大学软件学院, 吉林长春 130012;
    3. 符号计算与知识工程教育部重点实验室(吉林大学), 吉林长春 130012
  • 收稿日期:2015-12-30 修回日期:2016-06-20 出版日期:2017-05-25
    • 通讯作者:
    • 张立明
    • 作者简介:
    • 欧阳丹彤 女,1968年生于吉林长春,博士、吉林大学教授、博士生导师,主要研究方向为基于模型的诊断、自动推理和模型检测.E-mail:ouyangdantong@163.com;刘伯文 男,1993年出生吉林延边,吉林大学硕士研究生,研究方向为基于模型诊断、SAT问题.E-mail:1591365445@qq.com
    • 基金资助:
    • 国家自然科学基金 (No.61133011,No.61402196,No.61272208,No.61003101,No.61170092); 吉林省科技发展计划项目基金 (No.20140520067JH); 浙江省自然科学基金 (No.LY16F020004)

A Method of Computing Minimal Conflict Sets Combining the Structure Property with the Anti-depth SE-Tree

OUYANG Dan-tong1,3, LIU Bo-wen1,3, ZHOU Jian-hua2,3, ZHANG Li-ming1,3   

  1. 1. College of Computer Science and Technology, Jilin University, Changchun, Jilin 130012, China;
    2. CollegeofSoftware, Jilin University, Changchun, Jilin 130012, China;
    3. Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University), Ministry of Education, Changchun, Jilin 130012, China
  • Received:2015-12-30 Revised:2016-06-20 Online:2017-05-25 Published:2017-05-25
    • Supported by:
    • National Natural Science Foundation of China (No.61133011, No.61402196, No.61272208, No.61003101, No.61170092); Science and Technology Development Project Fund of Jilin Province (No.20140520067JH); National Natural Science Foundation of Zhejiang Province,  China (No.LY16F020004)

摘要:

基于模型诊断是人工智能领域内的一个重要研究方向,求解极小冲突集在基于模型诊断中有着重要应用.在对结合CSISE-Tree求解冲突集方法深入研究的基础上,根据冲突集求解特征重构了结合枚举树的计算冲突集的过程,提出基于深度优先反向搜索求解冲突集的方法.针对CSISE-Tree方法求解时占用内存空间与元件总数指数级相关的缺点,构建反向深度搜索方法减小求解时所占用内存空间;针对CSISE-Tree方法不能对部分非极小的冲突集进行剪枝的问题,给出对非冲突集和更多非极小的冲突集进行剪枝的方法,有效减少了求解时调用SAT(Boolean SATisfiability problem)求解器的次数;实验结果表明,与CSISE-Tree方法相比,本文提出的方法求解效率有明显的提升,并避免了求解时的内存爆炸问题.

关键词: 基于模型诊断, 冲突集, 布尔约束可满足, 集合枚举树

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.

Key words: model-based diagnosis, conflict set, Boolean SATisfiability problem (SAT), set-enumeration tree(SE-Tree)

中图分类号: