Incremental Information Interaction-Based Method for Enumerating MUSes

Enumerating minimal unsatisfiable subsets (MUS) is an important issue in theoretical computer science. Given an unsatisfiable Boolean formula, the number of its MUS is exponentially related to the formula’s scale. Contemporary methods aim to identify as many MUSes as possible within appropriate time limits. Dealing with the huge search space, choosing a suitable node to expand can markedly reduce the time consumption on shrink and grow operations, thereby the algorithm could obtain better performance. This paper introduces an incremental information interaction-based MUS solving method, denoted as MARCO-MSS4MUS, which utilizes the duality and complementary relationships among MUS, minimal correction sets (MCS), and maximal satisfiable subsets (MSS). Based on the framework of MARCO algorithm, the proposed method selects a more suitable node to expand via intersection and union information of previously identified MSSes during the search, i.e., the incremental MSS information is employed as a heuristic for node selection to accelerate the enumeration of MUS. This process also benefits in identifying more MSSes, in turn, the incremental MSS information help select a better node for next exploration, thereby achieving an interaction of incremental information. The paper presents two theorems and two corollaries regarding interactive incremental information, analyzing the feasibility of our MARCO-MSS4MUS algorithm theoretically. Experiments on standard MUS benchmark instances show the superiority of the proposed algorithm over state-of-the-art methods. Both the enumeration efficiency and the number of enumerated wins of the proposed method are significantly improved compared to existing methods.