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

doi:10.3969/j.issn.0372-2112.2017.05.021

电子学报 ›› 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. 吉林大学计算机科学与技术学院, 吉林长春 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-tong^1,3, LIU Bo-wen^1,3, ZHOU Jian-hua^2,3, ZHANG Li-ming^1,3

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)

摘要/Abstract

摘要：

基于模型诊断是人工智能领域内的一个重要研究方向，求解极小冲突集在基于模型诊断中有着重要应用.在对结合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)

中图分类号:

TP306

欧阳丹彤, 刘伯文, 周建华, 等. 结合问题特征利用SE-Tree反向深度求解冲突集的方法[J]. 电子学报, 2017, 45(5): 1175-1181.

OUYANG Dan-tong, LIU Bo-wen, ZHOU Jian-hua, et al. 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-1181.

参考文献

[1] Console L,Dressler O.Model-based diagnosis in the real world:lessons learned and challenges remaining[A].Proceedings of 16th International Joint Conference on Artificial Intelligence[C].Stockholm,Sweden,1999.1393-1400.
[2] De Kleer J.Local methods for localizing faults in electronic circuits[D].Cambridge,MA,MIT AI Memo 394,1976.
[3] Reiter R.A theory of diagnosis from first principles[J].Artificial Intelligence,1987,32(1):57-95.
[4] Jannach D,Schmitz T,Shchekotykhin K.Parallel model-based diagnosis on multi-core computers[J].Journal of Artificial Intelligence Research,2016,55:835-887.
[5] Zhao X,Ouyang D.Deriving all minimal hitting sets based on join relation[J].IEEE Transactions on Systems,Man,and Cybernetics:Systems,2015,45(7):1063-1076.
[6] 刘娟,欧阳丹彤,王艺源,张立明.结合特征学习的粒子群求解极小碰集方法[J].电子学报,2015,43(5):841-845. Liu Juan,Ouyang Dantong,et al.Computing minimal hitting sets with particle swarm optimization combined characteristics learning[J].Acta Electronica Sinica,2015,43(5):841-845.(in Chinese)
[7] Genesereth M R.The use of design descriptions in automated diagnosis[J].Artificial Intelligence,1984,24(1-3):411-436.
[8] Haenni R.A query driven anytime algorithm for argument-active and abduction[A].Proceedings of 17th National Conference on Artificial Intelligence[C].Texas,2000.337-342.
[9] 栾尚敏,戴国忠.利用结构信息的故障诊断方法[J].计算机学报,2005,28(5):801-808. Luang Shangmin,Dai Guozhong.An approachtodiagnosingasystemwithstructureinformation[J].Chinese JournalofComputers,2005,28(5):801-808.(in Chinese)
[10] 代树武,孙辉先.基于模型故障诊断中的冲突求解[J].控制理论与应用,2003,20(4):630-632. Dai Shuwu,Sun Huixian.Computing conflict setsfor model-based diagnosis[J].Control Theory & Applications,2003,20(4):630-632.(in Chinese)
[11] Stern R T,Kalech M,Feldman A,et al.Exploring the duality in conflict-directed model-based diagnosis[A]AAAI Conference on Artificial Intelligence[C].Canada:Toroto,2012.828-834.
[12] Amgoud L.Postulates for logic-based argumentation systems[J].International Journal of Approximate Reasoning,2014,55(9):2028-2048.
[13] Hou A.A theory of measurement in diagnosis from first principles[J].Artificial Intelligence,1994,65(2):281-328.
[14] Han B,Lee S J.Deriving minimal conflict sets by CS-Trees with mark set in diagnosis from first principles[J].IEEE Transactions on System,Man,and Cybernetics,1999,29(2):281-286.
[15] Smith A,Veneris A,Ali M F,et al.Fault diagnosis and logic debugging using Boolean satisfiability[J].IEEE Trans on CAD of Integrated Circuits and Systems,2005,24(10):1606-1621.
[16] 严晓浪,郑飞君,葛海通,杨军.结合二叉判决图和布尔可满足性的等价性验证算法[J].电子学报,2004,32(8):1233-1235. Yan Xiaolang,Zheng Feijun,Ge Haitong,Yang jun.Combining binary decision diagrams and Boolean satisfiability for equivalence cheking[J].Acta Electronica Sinica,2004,32(8):1233-1235.(in Chinese)
[17] Zhao X,Ouyang D.A method of combining SE tree to compute all minimal hitting sets[J].Progress in Natural Science,2006,16(2):169-174.
[18] 赵相福,欧阳丹彤.使用SAT求解器产生所有极小冲突部件集[J].电子学报,2009,37(4):804-810. Zhao Xiangfu,Ouyang Dantong.Deriving all minimal conflict sets using satisfiability algorithms[J].Acta Electronica Sinica,2009,37(4):804-810.(in Chinese)
[19] A.Biere.PicoSAT essentials[J].Journal on Satisfiability,Boolean Modeling and Computation,2008,4:75-97.

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

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

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 6

编辑推荐

Metrics

[1]	赵相福, 黄森, 童向荣, 欧阳丹彤, 张立明, 章星林. IBWIICC:结合局部独立覆盖检测策略增量求解极小碰集的算法[J]. 电子学报, 2022, 50(11): 2722-2729.
[2]	欧阳丹彤, 刘伯文, 刘梦, 张立明, 张永刚. 结合电路结构基于分块的诊断方法[J]. 电子学报, 2018, 46(7): 1571-1577.
[3]	刘梦, 欧阳丹彤, 刘伯文, 张立明, 张永刚. 结合问题特征的分组式诊断方法[J]. 电子学报, 2018, 46(3): 589-594.
[4]	潘理, 郑红, 刘显明, 杨勃. 基于Petri网局部性的极大冲突集枚举算法[J]. 电子学报, 2016, 44(8): 1858-1863.
[5]	徐勇, 毋国庆, 袁梦霆. 结合Craig插值分析的软件错误诊断方法[J]. 电子学报, 2016, 44(10): 2514-2521.
[6]	赵相福;欧阳丹彤;. 使用SAT求解器产生所有极小冲突部件集[J]. 电子学报, 2009, 37(4): 804-810.