基于双模型的MUS求解方法

论文摘要

求解不可满足问题的极小不可满足子集（minimal unsatisfiable subset, MUS）是人工智能领域的重要研究方向.MARCO-M方法是目前采用单一极大化模型求解MUS效率最高的方法,但此方法未对求解空间进行进一步有效剪枝.针对MARCO-M方法的不足,结合可满足问题求解复杂度低于不可满足问题的特征,提出基于双模型即极大-中间化模型的MARCO-MAM方法求解MUS.此方法对中间模型求解若得到极大可满足子集（maximal satisfiable subset, MSS）,则利用可满足问题对应求解空间对不可满足问题的求解空间进行剪枝,即利用MSS对应的空间来对MUS搜索空间进行剪枝,进而通过缩减未探索空间来提高MUS求解效率;如果中间模型进行求解得到MUS时,则减少了MARCO-M方法中MUS的不可满足迭代求解次数.此方法避免了MARCO-M方法单一极大化模型求解MUS时未有效利用其他优化技术对求解空间进行剪枝的问题.实验结果表明:与MARCO-M方法相比MARCO-MAM方法效率较高,尤其在大规模问题或较大搜索空间时效率提高更为明显.

论文目录

• 1 预备知识
•   1.1 SAT问题
•   1.2 MUS和MCS
• 2 MARCO-M方法
• 3 MARCO-MAM方法
• 4 实验结果
• 5 结束语

文章来源

类型: 期刊论文

作者: 欧阳丹彤,高菡,田乃予,刘梦,张立明

关键词: 命题可满足问题,极小不可满足子集,极大可满足子集,幂集探索,双模型

来源: 计算机研究与发展 2019年12期

年度: 2019

分类: 信息科技

专业: 自动化技术

单位: 吉林大学软件学院,吉林大学计算机科学与技术学院,符号计算与知识工程教育部重点实验室(吉林大学)

基金: 国家自然科学基金项目(61872159,61672261,61502199)~~

分类号: TP18

页码: 2623-2631

总页数: 9

文件大小: 822K

下载量: 38