基于双模型的MUS求解方法

MUS Enumeration Based on Double-Model

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

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.