CNFs and DNFs with Exactly $k$ Solutions

TL;DR

This paper investigates the minimal size of DNF and CNF formulas with exactly k solutions, providing new bounds that impact the efficiency of model counting algorithms.

Contribution

It establishes the first sub-logarithmic upper bounds and matching lower bounds on the size of formulas with exactly k solutions.

Findings

Constructed monotone DNF formulas with O(√(log k) log log k) terms

Proved that infinitely many k require at least Ω(log log k) terms or clauses

Results influence the complexity of model counting via formula transformations

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: {\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 $\Omega(\log\log k)$ terms or clauses. These results have significant implications for the efficiency of model counting algorithms based on formula transformations.