
结合问题特征利用SE-Tree反向深度求解冲突集的方法
A Method of Computing Minimal Conflict Sets Combining the Structure Property with the Anti-depth SE-Tree
基于模型诊断是人工智能领域内的一个重要研究方向,求解极小冲突集在基于模型诊断中有着重要应用.在对结合CSISE-Tree求解冲突集方法深入研究的基础上,根据冲突集求解特征重构了结合枚举树的计算冲突集的过程,提出基于深度优先反向搜索求解冲突集的方法.针对CSISE-Tree方法求解时占用内存空间与元件总数指数级相关的缺点,构建反向深度搜索方法减小求解时所占用内存空间;针对CSISE-Tree方法不能对部分非极小的冲突集进行剪枝的问题,给出对非冲突集和更多非极小的冲突集进行剪枝的方法,有效减少了求解时调用SAT(Boolean SATisfiability problem)求解器的次数;实验结果表明,与CSISE-Tree方法相比,本文提出的方法求解效率有明显的提升,并避免了求解时的内存爆炸问题.
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.
基于模型诊断 / 冲突集 / 布尔约束可满足 / 集合枚举树 {{custom_keyword}} /
model-based diagnosis / conflict set / Boolean SATisfiability problem (SAT) / set-enumeration tree(SE-Tree) {{custom_keyword}} /
[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.
国家自然科学基金 (No.61133011,No.61402196,No.61272208,No.61003101,No.61170092); 吉林省科技发展计划项目基金 (No.20140520067JH); 浙江省自然科学基金 (No.LY16F020004)
/
〈 |
|
〉 |