@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{WUAWMK20,
  title={A Study of Symmetry Breaking Predicates and Model Counting},
  author={
    Wang, Wenxi and Usman, Muhammad and Almaawi, Alyas and Wang, Kaiyuan and
    Meel, Kuldeep S. and Khurshid, Sarfraz
  },
  booktitle=TACAS,
  month=apr,
  year={2020},
  bib2html_rescat={Counting},
  bib2html_pubtype={Refereed Conference},
  bib2html_dl_pdf={../Papers/tacas20.pdf},
  abstract={
    Propositional model counting is a classic problem that has
    recently witnessed many technical advances and novel applications. While
    the basic model counting problem requires computing the number of all
    solutions to the given formula, in some important application scenarios,
    the desired count is not of all solutions, but instead, of all unique
    solutions
    up to isomorphism. In such a scenario, the user herself must try to
    either use the full count that the model counter returns to compute the
    count up to isomorphism, or ensure that the input formula to the model
    counter adequately captures the symmetry breaking predicates so it can
    directly report the count she desires.
    We study the use of CNF-level and domain-level symmetry breaking
    predicates in the context of the state-of-the-art in model counting,
    specifically
    the leading approximate model counter ApproxMC and the recently
    introduced exact model counter ProjMC. As benchmarks, we use
    a range of problems, including structurally complex specifications of
    software
    systems and constraint satisfaction problems. The results show that
    while it is sometimes feasible to compute the model counts up to isomorphism
    using the full counts that are computed by the model counters,
    doing so suffers from poor scalability. The addition of symmetry breaking
    predicates substantially assists model counters. Domain-specific predicates
    are particularly useful, and in many cases can provide full symmetry
    breaking to enable highly efficient model counting up to isomorphism.
    We hope our study motivates new research on designing model counters
    that directly account for symmetries to facilitate further applications of
    model counting.
  },
}