@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{ADM20,
  title={On the Sparsity of XORs in Approximate Model Counting},
  author={Agrawal, Durgesh and Bhavishya and Meel, Kuldeep S.},
  month=jul,
  booktitle=SAT,
  bib2html_pubtype={Refereed Conference},
  bib2html_dl_pdf={../Papers/sat20-adm.pdf},
  bib2html_rescat={Counting},
  year={2020},
  abstract={
    Given a Boolean formula F, the problem of model counting, also referred to
    as #SAT, is to compute the number of solutions of F.
    The hashing-based techniques for approximate counting have emerged as a
    dominant approach, promising achievement of both scalability and rigorous
    theoretical guarantees.
    The standard construction of strongly 2-universal hash functions employs
    dense XORs (i.e., involving half of the variables in expectation),
    which is widely known to cause degradation in the runtime performance of
    state of the art SAT solvers. Consequently,
    the past few years have witnessed an intense activity in the design of
    sparse XORs as hash functions. Such constructions
    have been proposed with beliefs to provide runtime performance improvement
    along with theoretical guarantees similar to that of dense XORs.
    The primary contribution of this paper is a rigorous theoretical and
    empirical analysis to understand the effect of the
    sparsity of XORs. In contradiction to prior beliefs of applicability of
    analysis for sparse hash functions to all the hashing-based
    techniques, we prove a contradictory result. We show that the best-known
    bounds obtained for sparse XORs are still too
    weak to yield theoretical guarantees for a large class of hashing- based
    techniques, including the state of the art approach ApproxMC3.
    We then turn to a rigorous empirical analysis of the performance benefits of
    sparse hash functions. To this end, we first design,
    to the best of our knowledge, the most efficient algorithm called
    SparseCount2 using sparse hash functions, which achieves at least up to two
    orders of magnitude performance improvement
    over its predecessor. Contradicting the current beliefs, we observe that
    SparseCount2 still falls short of ApproxMC3
    in runtime performance despite the usage of dense XORs in ApproxMC3. In
    conclusion, our work showcases that the question
    of whether it is possible to use short XORs to achieve scalability while
    providing strong theoretical guarantees is still wide open.
  },
}