@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@inproceedings{BM21,
  title={Counting Minimal Unsatisfiable Subsets},
  author={Bendik, Jaroslav and Meel, Kuldeep S.},
  booktitle=CAV,
  year={2021},
  month=jul,
  bib2html_dl_pdf={../Papers/cav21-bm.pdf},
  bib2html_rescat={Counting},
  bib2html_pubtype={Refereed Conference},
  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, Bendik and Meel initiated the study of MUS
    counting techniques. They succeeded in designing the first approximate MUS
    counter, AMUSIC, that does not rely on exhaustive MUS enumeration. AMUSIC,
    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 AMUSIC by designing the
    first exact MUS counter, CountMUST, that does not rely on exhaustive
    enumeration. CountMUST 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 CountMUST successfully returns MUS count for
    1500 instances while AMUSIC and enumeration-based techniques could only
    handle up to 833 instances.
  },
}