@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{CGM25,
  title={CNFs and DNFs with Exactly k Solutions},
  author={Chandran, L. Sunil and Gajjala, Rishikesh and Meel, Kuldeep S.},
  booktitle=SAT,
  pages={9:1--9:15},
  year={2025},
  month=aug,
  bib2html_rescat={Counting},
  bib2html_pubtype={Refereed Conference},
  bib2html_dl_pdf=
    {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.9},
  abstract={
    Model counting is a fundamental problem that consists of determining the
    number of satisfying assignments for a given Boolean formula. The weighted
    variant, which computes the weighted sum of satisfying assignments, has
    extensive applications in probabilistic reasoning, network reliability,
    statistical physics, and formal verification. A common approach for solving
    weighted model counting is to reduce it to unweighted model counting, which
    raises an important question: What is the minimum number of terms (or
    clauses) required to construct a DNF (or CNF) formula with exactly k
    satisfying assignments? In this paper, we establish both upper and lower
    bounds on this question. We prove that for any natural number k, one can
    construct a monotone DNF formula with exactly k satisfying assignments using
    at most O(sqrt{log k}log log k) terms. This construction represents the
    first
    o(log k) upper bound for this problem. We complement this result by showing
    that there exist infinitely many values of k for which any DNF or CNF
    representation requires at least Omega(log log k) terms or clauses. These
    results have significant implications for the efficiency of model counting
    algorithms based on formula transformations.
  },
}
