欧阳丹彤^1,2,3,高菡^1,3,田乃予^2,3,刘梦^2,3,张立明^1,2,3

¹(吉林大学软件学院 长春 130012);²(吉林大学计算机科学与技术学院 长春 130012);³(符号计算与知识工程教育部重点实验室(吉林大学) 长春 130012) (ouyangdantong@163.com)

出版日期: 2019-12-01


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

MUS Enumeration Based on Double-Model

Ouyang Dantong^1,2,3, Gao Han^1,3, Tian Naiyu^2,3, Liu Meng^2,3, Zhang Liming^1,2,3

¹(College of Software, Jilin University, Changchun 130012);²(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: 2019-12-01

摘要/Abstract

摘要： 求解不可满足问题的极小不可满足子集(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方法效率较高,尤其在大规模问题或较大搜索空间时效率提高更为明显.

参考文献

相关文章 2

[1]	张水发 丁 欢 张文生. 双模型背景建模与目标检测研究[J]. , 2011, 48(11): 1983-1990.
[2]	赖 永 欧阳丹彤 蔡敦波 吕 帅. 基于扩展规则的模型计数与智能规划方法[J]. , 2009, 46(3): 459-469.

PDF全文下载地址:

https://crad.ict.ac.cn/CN/article/downloadArticleFile.do?attachType=PDF&id=4064