-
题名针对MUS求解问题的加强剪枝策略
- 1
-
-
作者
蒋璐宇
欧阳丹彤
董博文
张立明
-
机构
吉林大学计算机科学与技术学院
吉林大学软件学院
符号计算与知识工程教育部重点实验室(吉林大学)
-
出处
《软件学报》
EI
CSCD
北大核心
2024年第4期1964-1979,共16页
-
基金
国家自然科学基金(62076108,61872159,61972360)。
-
文摘
极小不可满足子集(minimal unsatisfiable subsets,MUS)的求解是布尔可满足性问题中的一个重要子问题.对于一个给定的不可满足问题,其MUS的求解能够反映出问题中导致其不可满足的关键原因.然而,MUS的求解是一项极其耗时的任务,不同的剪枝过程将直接影响到搜索空间的大小、算法的迭代次数,从而影响算法的求解效率.提出一种针对MUS求解的加强剪枝策略ABC(accelerating by critical MSS),依据MSS、MCS、MUS这3者之间的对偶性和碰集关系特点,提出cMSS和subMUS概念,并总结出4条性质,即每个MUS必是subMUS的超集,进而在避免对MCS的碰集进行求解的情况下有效利用MUS和MCS互为碰集的特征,有效避免求解碰集时的时间开销.当subMUS不可满足时,则subMUS是唯一的MUS,算法将提前结束执行;当subMUS可满足时,则剪枝掉此节点,进而有效避免对求解空间中的冗余空间进行搜索.同时,通过理论证明ABC策略的有效性,并将其应用于目前最高效的单一化模型算法MARCO和双模型算法MARCO-MAM,在标准测试用例下的实验结果表明,该策略可以有效地对搜索空间进行进一步剪枝,从而提高MUS的枚举效率.
-
关键词
极小不可满足子集
极大可满足子集
mus枚举
幂集探索
不可行分析
-
Keywords
minimal unsatisfiable subset(mus)
maximal satisfiable subset(MSS)
mus enumeration
power set exploration
infeasibility analysis
-
分类号
TP18
[自动化与计算机技术—控制理论与控制工程]
-