@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{SRSM19,
  title={Ganak: A Scalable Probabilistic Exact Model Counter},
  author={
    Sharma, Shubham and Roy, Subhajit and Soos, Mate and Meel, Kuldeep S.
  },
  bib2html_pubtype={Refereed Conference},
  booktitle=IJCAI,
  month=aug,
  year={2019},
  bib2html_rescat={Counting},
  bib2html_dl_pdf={../Papers/ijcai19srsm.pdf},
  code={https://github.com/meelgroup/ganak},
  abstract={
    Given a Boolean formula F, the problem of model counting, also referred to
    as #SAT, seeks to compute the number of solutions of F. Model counting is a
    fundamental problem with a wide variety of applications ranging from
    planning, quantified information flow to probabilistic reasoning and the
    like. The modern #SAT solvers tend to be either based on static
    decomposition, dynamic decomposition, or a hybrid of the two. Despite
    dynamic decomposition based #SAT solvers sharing much of their architecture
    with SAT solvers, the core design and heuristics of dynamic
    decomposition-based #SAT solvers has remained constant for over a decade. In
    this paper, we revisit the architecture of the state-of-the-art dynamic
    decomposition-based #SAT tool, sharpSAT, and demonstrate that by introducing
    a new notion of probabilistic component caching and the usage of universal
    hashing for exact model counting along with the development of several new
    heuristics can lead to significant performance improvement over
    state-of-the-art model-counters. In particular, we develop GANAK, a new
    scalable probabilistic exact model counter that outperforms state-of-the-art
    exact and approximate model counters sharpSAT and ApproxMC3 respectively,
    both in terms of PAR-2 score and the number of instances solved.
    Furthermore, in our experiments, the model count returned by GANAK was equal
    to the exact model count for all the benchmarks. Finally, we observe that
    recently proposed preprocessing techniques for model counting benefit exact
    model counters while hurting the performance of approximate model counters.
  },
}