基于不可满足原因的最小纠正集求解

• 作者: 张敏 张越岭 李建文 胡潇洒 蒲戈光
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 可满足性 最小纠正集 软件验证
• 年，卷（期）: 2018,（6）
• 所属期刊栏目: 软件工程
• 页码范围: 1067-1074
• 页数: 8页
• 分类号: TP311
• 字数: 8065字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2018.06.015

摘要

布尔公式的最小纠正集MCS是子句的集合.对于一个不可满足公式,移除MCS后,所得到的新公式可满足.任一MCS中的子句保留在公式中,所得到的新公式不可满足.通过求解MCS并调整约束集合,能够求解最小不可满足核心、MaxSAT问题和最大(小)可满足解问题;还能够应用于故障定位、模型检查配置优化等实际问题中.提出了一种基于不可满足原因的MCS求解算法,实现了相应的CUC工具.通过与目前最好的MCS求解工具LBX进行比较,得到了CUC性能优于LBX的结论.CUC比LBX平均多解出5％(65个)的公式.对于CUC和LBX均可解出的公式,CUC的平均求解时间比LBX快2.5倍.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张敏	华东师范大学计算机科学与软件工程学院	34	171	7.0	12.0
2	李建文	华东师范大学计算机科学与软件工程学院	3	13	2.0	3.0
3	蒲戈光	华东师范大学计算机科学与软件工程学院	7	27	3.0	5.0
4	胡潇洒	华东师范大学计算机科学与软件工程学院	1	0	0.0	0.0
5	张越岭	华东师范大学计算机科学与软件工程学院	1	0	0.0	0.0