CNFs and DNFs with Exactly $k$ Solutions
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915984903766016 |
|---|---|
| author | Chandran, L. Sunil Gajjala, Rishikesh Meel, Kuldeep S. |
| author_facet | Chandran, L. Sunil Gajjala, Rishikesh Meel, Kuldeep S. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_07268 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | CNFs and DNFs with Exactly $k$ Solutions Chandran, L. Sunil Gajjala, Rishikesh Meel, Kuldeep S. Discrete Mathematics Data Structures and Algorithms Logic in Computer Science Combinatorics Logic 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. |
| title | CNFs and DNFs with Exactly $k$ Solutions |
| topic | Discrete Mathematics Data Structures and Algorithms Logic in Computer Science Combinatorics Logic |
| url | https://arxiv.org/abs/2506.07268 |