@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{BDSRM21,
  title={
    Symmetric Component Caching for Model Counting on Combinatorial Instances
  },
  author={
    Timothy van Bremen and Vincent Derkinderen and Shubham Sharma and Subhajit
    Roy and Kuldeep S. Meel
  },
  booktitle=AAAI,
  month=feb,
  year={2021},
  bib2html_rescat={Counting},
  bib2html_pubtype={Refereed Conference},
  bib2html_dl_pdf={../Papers/aaai21-bdsrm.pdf},
  abstract={
    Given a propositional formula $\psi$, the model counting problem, also
    referred to as #SAT, seeks to compute the number of satisfying assignments
    (or models) of $\psi$. Modern search-based model counting algorithms are
    built on conflict-driven clause learning, combined with the caching of
    certain subformulas (called components) encountered during the search
    process. Despite significant progress in these algorithms over the years,
    state-of-the-art model counters often struggle to handle large but
    structured instances that typically arise in combinatorial settings.
    Motivated by the observation that these counters do not exploit the inherent
    symmetries exhibited in such instances, we revisit the component caching
    architecture employed in current counters and introduce a novel caching
    scheme that focuses on identifying symmetric components. We first prove the
    soundness of our approach, and then integrate it into the state-of-the-art
    model counter GANAK. Our extensive experiments on hard combinatorial
    instances demonstrate that the resulting counter, SymGANAK, leads to
    improvements over GANAK both in terms of PAR-2 score and the number of
    instances solved.
  },
}