结合DOEC极小化策略的SAT求解极小碰集方法

• 作者: 刘思光 张立明 欧阳丹彤 王艺源 王荣全
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 基于模型诊断 极小碰集 可满足性问题 碰集极小化 集合覆盖
• 年，卷（期）: 2018,（6）
• 所属期刊栏目: 人工智能
• 页码范围: 1273-1281
• 页数: 9页
• 分类号: TP18
• 字数: 7654字
• 语种: 中文
• DOI: 10.7544/issn1000-1239.2018.20160809

摘要

在基于模型诊断中,诊断解通常是根据极小冲突集合簇进行相应的计算得到所有的极小碰集,所以提高极小碰集的求解效率是模型诊断的核心问题.因此提出结合基于元素覆盖集合度(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倍左右.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张立明	吉林大学计算机科学与技术学院	27	139	7.0	10.0
2	王荣全	吉林大学计算机科学与技术学院	2	2	1.0	1.0
3	王艺源	吉林大学计算机科学与技术学院	4	27	2.0	4.0