(吉林大学计算机科学与技术学院 长春 130012) (符号计算与知识工程教育部重点实验室(吉林大学) 长春 130012) (wangrongquanjlu@163.com)
出版日期: 2018-06-01基金资助:国家自然科学基金项目(61672261,61502199,61402196,61373052)；浙江省自然科学基金项目(LY16F020004)Solving Minimal Hitting Sets Method with SAT Based on DOEC Minimization
Wang Rongquan,Ouyang Dantong,Wang Yiyuan,Liu Siguang, Zhang Liming(College of Computer Science and Technology, Jilin University, Changchun 130012) (Key Laboratory of Symbolic Computation and Knowledge Engineering (Jilin University), Ministry of Education, Changchun 130012)
Online: 2018-06-01摘要/Abstract
摘要： 在基于模型诊断中，诊断解通常是根据极小冲突集合簇进行相应的计算得到所有的极小碰集，所以提高极小碰集的求解效率是模型诊断的核心问题.因此提出结合基于元素覆盖集合度(degree of element coverage, DOEC)极小化策略的SAT求解极小碰集的方法SAT-MHS(satisfiability problem-minimal hitting sets).首先，方法SAT-MHS将碰集求解问题转换成SAT问题,即把所有的冲突集合以子句形式表示成SAT的输入CNF进行迭代求解.其次,提出比现有的基于子超集检测极小化策略(sub-superset detecting minimization, SSDM)更为高效的DOEC极小化策略进行极小化处理.由实验数据可见，与SSDM极小化策略相比，其优点是缩减了求解空间和迭代求解次数，尤其当求解规模较大问题时，其极小化效率越高.主要是因为其极小化不会随着待求解问题规模的增加而增加，而是只与冲突集合簇的大小相关，因此时间复杂度较低.实验结果表明，对于一些较大的实例，与目前效率最好的Boolean方法相比，SAT-MHS方法高效且易于实现，求解速度能提高10~20倍，DOEC极小化策略对比传统SSDM极小化策略能达到40倍左右.
参考文献
相关文章 13
| [1] | 欧阳丹彤, 高菡, 徐旖旎, 张立明. 结合故障逻辑关系的极小冲突集求解方法[J]. 计算机研究与发展, 2020, 57(7): 1472-1480. |
| [2] | 田乃予,欧阳丹彤,刘梦,张立明. 基于子集一致性检测的诊断解极小性判定方法[J]. 计算机研究与发展, 2019, 56(7): 1396-1407. |
| [3] | 欧阳丹彤,陈晓艳,叶靖,邓召勇,张立明. 基于极小碰集求解算法的测试向量集约简[J]. 计算机研究与发展, 2019, 56(11): 2448-2457. |
| [4] | 欧阳丹彤,智华云,刘伯文,张立明,张永刚. 基于伪故障度生成枚举树的极小诊断求解方法[J]. 计算机研究与发展, 2018, 55(4): 782-790. |
| [5] | 邓召勇,欧阳丹彤,耿雪娜,刘杰. 基于动态极大元素覆盖值的极小碰集求解算法[J]. 计算机研究与发展, 2018, 55(4): 791-801. |
| [6] | 徐旖旎,欧阳丹彤,刘梦,张立明,张永刚. 结合故障输出结构特征的极小冲突求解算法[J]. 计算机研究与发展, 2018, 55(11): 2386-2394. |
| [7] | 刘思光,欧阳丹彤,王艺源,贾凤雨,张立明. 结合SE-Tree结构特征的极小碰集求解算法[J]. 计算机研究与发展, 2016, 53(11): 2556-2566. |
| [8] | 王艺源,欧阳丹彤,张立明,张永刚. 利用CSP求解极小碰集的方法[J]. 计算机研究与发展, 2015, 52(3): 588-595. |
| [9] | 张立明 欧阳丹彤 曾海林. 基于动态极大度的极小碰集求解方法[J]. , 2011, 48(2): 209-215. |
| [10] | 张立明 欧阳丹彤 白洪涛. 基于半扩展规则的定理证明方法[J]. , 2010, 47(9): 1522-1529. |
| [11] | 孙吉贵 李 莹 朱兴军 吕 帅. 一种新的基于扩展规则的定理证明算法[J]. , 2009, 46(1): 9-14. |
| [12] | 潘 锐 朱大铭 马绍汉. 一般设施定位问题计算复杂度和近似算法研究[J]. , 2007, 44(5): 790-797. |
| [13] | 蔡志平 殷建平 刘湘辉 刘 芳 吕绍和. 链路约束的分布式网络监测模型[J]. , 2006, 43(4): 601-606. |
PDF全文下载地址:
https://crad.ict.ac.cn/CN/article/downloadArticleFile.do?attachType=PDF&id=3711
