• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
CNFs and DNFs with Exactly k Solutions.
L. Sunil Chandran, Rishikesh Gajjala and Kuldeep S. Meel.
In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 9:1–9:15, August 2025.
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(sqrtlog klog 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.
@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.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21