MUS Enumeration Based on Double-Model

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.