@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{LMY21,
  title={The Power of Literal Equivalence in Model Counting},
  author={Yong Lai and Kuldeep S. Meel and Roland Yap},
  booktitle=AAAI,
  month=feb,
  year={2021},
  bib2html_rescat={Counting},
  bib2html_pubtype={Refereed Conference},
  bib2html_dl_pdf={../Papers/aaai21-lmy.pdf},
  abstract={
    The past two decades have seen the significant improvements of the
    scalability of practical model counters, which have been quite influential
    in many applications from artificial intelligence to formal verification.
    While most of exact counters fall into two categories, search-based and
    compilation-based, Huang and Darwiche's remarkable observation ties these
    two categories: the trace of a search-based exact model counter corresponds
    to a Decision-DNNF formula. Taking advantage of literal equivalences, this
    paper designs an efficient model counting technique such that its trace is a
    generalization of Decision-DNNF formula. We first propose a generalization
    of Decision-DNNF, called CCDD, to capture literal equivalences, then show
    that CCDD supports model counting in linear time, and finally design a model
    counter, called ExactMC, whose trace corresponds to CCDD. We perform an
    extensive experimental evaluation over a comprehensive set of benchmarks and
    conduct performance comparison of ExactMC vis-a-vis the state of the art
    counters, c2d, miniC2D, D4, ADDMC, and Ganak. Our empirical evaluation
    demonstrates ExactMC can solve 885 instances while the prior state of the
    art could solve only 843 instances, representing a significant improvement
    of 42 instances.
  },
}