CNFs and DNFs with Exactly $k$ Solutions
For researchers in model counting and Boolean function representation, this provides tight bounds on the size of DNF/CNF formulas with exactly k solutions, with implications for algorithm efficiency.
The paper establishes that any natural number k can be represented by a monotone DNF with O(√(log k) log log k) terms, the first sub-logarithmic upper bound, and shows a matching lower bound of Ω(log log k) for infinitely many k, impacting the efficiency of model counting via formula transformations.
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: {\em 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 $Ω(\log\log k)$ terms or clauses. These results have significant implications for the efficiency of model counting algorithms based on formula transformations.