Incremental Information Interaction-Based Algorithm 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 MUSes as many as possible within appropriate time limits. Dealing with the huge search space and choosing a suitable node to expand can markedly reduce the time consumption on shrink and grow operations, thereby the algorithm could obtain better performance. We introduce an incremental information interaction-based MUS solving algorithm, denoted as MARCO-MSS4MUS, which utilizes the duality and complementary relationships among MUS, minimal correction set (MCS), and maximal satisfiable subset (MSS). Based on the framework of MARCO algorithm, the proposed algorithm 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 helps select a better node for next exploration, thereby achieving an interaction of incremental information. Two theorems and two corollaries regarding interactive incremental information are proposed and the feasibility of our MARCO-MSS4MUS algorithm is theoretically analyzed. Experiments on standard MUS benchmark instances show the superiority of the proposed algorithm over state-of-the-art algorithms. Both the enumeration efficiency and the number of enumerated wins of the proposed algorithm are significantly improved compared with existing algorithms.