• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Approximate Counting of Minimal Unsatisfiable Subsets.
Jaroslav Bendik, and Kuldeep S. Meel.
In Proceedings of International Conference on Computer-Aided Verification (CAV), July 2020.
Invited to FMSD issue dedicated to the best papers from CAV 2020
Given an unsatisfiable formula F in CNF, i.e. a set of clauses, the problem of Minimal Unsatisfiable Subset (MUS) seeks to identify the minimal subset of clauses N \subseteq F such that N is unsatisfiable. The emerging viewpoint of MUSes as the root causes of unsatisfiability has led MUSes to find applications in a wide variety of diagnostic approaches. Recent advances in finding and enumeration of MUSes have motivated researchers to discover applications that can benefit from rich information about the set of MUSes. One such extension is that of counting the number of MUSes, which has shown to describe the inconsistency metrics for general propositional knowledge bases. The current best approach for MUS counting is to employ a MUS enumeration algorithm, which often does not scale for the cases with a reasonably large number of MUSes. Motivated by the success of hashing-based techniques in the context of model counting, we design the first approximate counting procedure with (epsilon,delta) guarantees, called AMUSIC. Our approach avoids exhaustive MUS enumeration by combining the classical technique of universal hashing with advances in QBF solvers along with a novel usage of union and intersection of MUSes to achieve runtime efficiency. Our prototype implementation of AMUSIC is shown to scale to instances that were clearly beyond the reach of enumeration-based approaches.
@inproceedings{bm20,
title={Approximate Counting of Minimal Unsatisfiable Subsets},
author={Bendik, Jaroslav and Meel, Kuldeep S.},
month=jul,
booktitle=CAV,
year={2020},
bib2html_rescat={Counting},
bib2html_dl_pdf={../Papers/cav20-bm.pdf},
note={Invited to FMSD issue dedicated to the best papers from CAV 2020},
bib2html_pubtype={Refereed Conference,Award Winner},
abstract={
Given an unsatisfiable formula F in CNF, i.e. a set of clauses,
the problem of Minimal Unsatisfiable Subset (MUS) seeks to
identify the minimal subset of clauses N \subseteq F such that N is
unsatisfiable. The emerging viewpoint of MUSes as the root causes of
unsatisfiability has led MUSes to find applications in a wide variety of
diagnostic approaches. Recent advances in finding and
enumeration of MUSes have motivated researchers to discover applications
that can benefit from rich information about the set of MUSes.
One such extension is that of counting the number of MUSes, which has shown
to describe the inconsistency metrics for general
propositional knowledge bases. The current best approach for MUS counting is
to employ a MUS enumeration algorithm, which often does not scale for the
cases with a reasonably large number of MUSes.
Motivated by the success of hashing-based techniques in the context of model
counting, we design the first approximate counting procedure with
(epsilon,delta) guarantees, called AMUSIC. Our approach avoids exhaustive
MUS enumeration by combining the classical technique of universal hashing
with
advances in QBF solvers along with a novel usage of union and intersection
of MUSes to achieve runtime efficiency. Our prototype implementation of
AMUSIC is shown to scale to instances that were clearly beyond the reach of
enumeration-based approaches.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21