Counting Minimal Unsatisfiable Subsets

Abstract Given an unsatisfiable Boolean formula F in CNF, an unsatisfiable subset of clauses U of F is called Minimal Unsatisfiable Subset (MUS) if every proper subset of U is satisfiable. Since MUSes serve as explanations for the unsatisfiability of F , MUSes find applications in a wide variety of domains. The availability of efficient SAT solvers has aided the development of scalable techniques for finding and enumerating MUSes in the past two decades. Building on the recent developments in the design of scalable model counting techniques for SAT, Bendík and Meel initiated the study of MUS counting techniques. They succeeded in designing the first approximate MUS counter, $$\mathsf {AMUSIC}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>AMUSIC</mml:mi></mml:math> , that does not rely on exhaustive MUS enumeration. $$\mathsf {AMUSIC}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>AMUSIC</mml:mi></mml:math> , however, suffers from two shortcomings: the lack of exact estimates and limited scalability due to its reliance on 3-QBF solvers. In this work, we address the two shortcomings of $$\mathsf {AMUSIC}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>AMUSIC</mml:mi></mml:math> by designing the first exact MUS counter, $$\mathsf {CountMUST}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>CountMUST</mml:mi></mml:math> , that does not rely on exhaustive enumeration. $$\mathsf {CountMUST}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>CountMUST</mml:mi></mml:math> circumvents the need for 3-QBF solvers by reducing the problem of MUS counting to projected model counting. While projected model counting is #NP-hard, the past few years have witnessed the development of scalable projected model counters. An extensive empirical evaluation demonstrates that $$\mathsf {CountMUST}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>CountMUST</mml:mi></mml:math> successfully returns MUS count for 1500 instances while $$\mathsf {AMUSIC}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>AMUSIC</mml:mi></mml:math> and enumeration-based techniques could only handle up to 833 instances.