ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2019, Vol. 56 ›› Issue (12): 2623-2631.doi: 10.7544/issn1000-1239.2019.20180852

• 人工智能 • 上一篇    下一篇

基于双模型的MUS求解方法

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

  1. 1(吉林大学软件学院 长春 130012);2(吉林大学计算机科学与技术学院 长春 130012);3(符号计算与知识工程教育部重点实验室(吉林大学) 长春 130012) (ouyangdantong@163.com)
  • 出版日期: 2019-12-01
  • 基金资助: 
    国家自然科学基金项目(61872159,61672261,61502199)

MUS Enumeration Based on Double-Model

Ouyang Dantong1,2,3, Gao Han1,3, Tian Naiyu2,3, Liu Meng2,3, Zhang Liming1,2,3   

  1. 1(College of Software, Jilin University, Changchun 130012);2(College of Computer Science and Technology, Jilin University, Changchun 130012);3(Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University), Ministry of Education, Changchun 130012)
  • Online: 2019-12-01

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

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

Abstract: The MUS (minimal unsatisfiable subset) for solving unsatisfiable problems is an important research direction in the field of artificial intelligence. The MARCO-M method is currently the most efficient way of solving MUS. It uses a single way to enumerate MUS, called maximal-model, without further effective pruning. For the shortcoming of MARCO-M, MARCO-MAM method is proposed which uses maximal-middle model to enumerate MUS. It emphasizes the characteristic that the complexity of solving satisfiable problem is less than the one of solving unsatisfiable problem, that is, solving an MSS is easier than solving an MUS. There are two solutions when using middle-model to improve the efficiency of MUS enumeration, if an MSS(maximal satisfiable subset) is found, the unexplored space of MUS can be pruned by blocking down the MSS. Else, an MUS is found that the times of the unsatisfiable iteration will be reduced. The double-model selects seeds from the top and middle of the hasse diagram, respectively, rather than a single top-down. The maximal model does not effectively use other excellent techniques to reduce the solution space when enumerating MUS. The experimental results show that the MARCO-MAM method is more efficient than the MARCO-M method, especially in large-scale problems or large search spaces.

Key words: propositional satisfiability problem(SAT), minimal unsatisfiable subset(MUS), maximal satisfiable subset(MSS), power set exploration, double model

中图分类号: