ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2019, Vol. 56 ›› Issue (12): 2623-2631.doi: 10.7544/issn1000-1239.2019.20180852

Previous Articles     Next Articles

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

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

CLC Number: