Abstract 1 Introduction 2 Connection to Ideals of Sets System 3 Proof of Lower Bound 4 Proof of Upper Bound 5 Conclusion and Open Problems References Appendix A Deferred proofs

CNFs and DNFs with Exactly k Solutions

L. Sunil Chandran ORCID Indian Institute of Science, Bengaluru, India Rishikesh Gajjala ORCID Indian Institute of Science, Bengaluru, India Kuldeep S. Meel ORCID Georgia Institute of Technology, Atlanta, GA, USA
University of Toronto, Canada
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⁢(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.

Keywords and phrases:
Model counting, #SAT, Set Systems, Combinatorics
Copyright and License:
[Uncaptioned image] © L. Sunil Chandran, Rishikesh Gajjala, and Kuldeep S. Meel; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Theory of computation → Logic
Funding:
This research was funded in part by the Natural Sciences and Engineering Research Council of Canada (NSERC), funding reference number RGPIN-2024-05956.
Editors:
Jeremias Berg and Jakob Nordström

1 Introduction

The (unweighted) model counting is a classical problem in which one has to find the number of satisfying assignments for a given boolean formula. Usually, Boolean formulae are considered in two forms – Conjunctive Normal Form (CNF) and Disjunctive Normal Form (DNF). In the former case, the formula is written as conjunctions (ANDs) of clauses. (Clauses are literals combined using ORs.) In the latter case the formula is written as disjunctions (ORs) of terms. (Terms are literals combined using ANDs). Note that a variable in a formula may appear either in positive form or in negated form. A monotone formula in DNF (or in CNF) consists of only variables in positive form.

The unweighted model counting problem was shown to be #P-complete for formulae in both CNF and DNF by Valiant [20]. The weighted model counting is a generalization of this problem. We are not providing a complete definition of this problem here since it is technical, but it can be found in [6]. Weighted model counting has been extensively studied [7, 10] due to its diverse applications across multiple domains. These applications include probabilistic reasoning [16], network reliability estimation [17], statistical physics, probabilistic databases [19], program synthesis, and system verification [8, 21]. The fundamental nature of weighted model counting has led to its emergence as a core computational problem in areas requiring reasoning under uncertainty, where the ability to compute weighted sums across large combinatorial spaces is essential.

A natural approach for solving the weighted model counting problem is to reduce it to the unweighted model counting problem and then to use the existing solvers for the latter [6]. This reduction approach has proven effective across various application domains as it leverages the significant advances in unweighted model counting algorithms. A key subroutine in this reduction involves finding DNFs or CNFs with exactly k satisfying assignments for a given positive integer k. The reduction becomes more efficient as the number of terms (or clauses) in the DNF or CNF decreases. While the number of terms is not the only factor of relevance, it raises a very natural question: What is the minimum number of terms (or clauses) required to construct a DNF (or CNF) formula with exactly k satisfying assignments?

This can be quantified using β⁢(k), which is defined as follows:

Definition 1.

The minimum number of terms or clauses needed to generate a DNF or CNF with exactly k satisfying assignments is defined to be β⁢(k).

It is known that β⁢(k)=O⁢(log⁡k) [6]. In this work, using an interesting connection to ideals of set systems, we give new lower and upper bounds on β⁢(k).

It is easy to see that many arbitrarily large numbers k exist for which β⁢(k)=1. For example, consider the DNF in which (x1) is the only term and x2,x3⁢⋯⁢xq+1 are the free variables, i.e., the variables which do not appear in the DNF (and hence their truth value does not affect the satisfiability of the formulae). Therefore, all k of the form 2q can be generated using a DNF with only 1 term, i.e., β⁢(k)=1. At the same time, there exists k for which we need at least Ω⁢(log⁡log⁡k) terms to generate a DNF with exactly k solutions (we prove this statement later). Thus, β⁢(k) does not increase or decrease monotonically with k. This motivates us to introduce a parameter called block count of k, which is more intimately associated with the number of terms needed to generate a DNF with exactly a given number of satisfying assignments.

Let 𝟏m denote 𝟏𝟏⁢⋯⁢m⁢ times and 𝟎q denote 𝟎𝟎⁢⋯⁢q⁢ times. Using this notation, the binary representation of 49, namely 110001 can be represented as 𝟏2⁢𝟎3⁢𝟏1.

Definition 2.

The block binary representation of any k∈ℕ, is defined to be the unique representation 𝟏qb⁢𝟎lb⁢⋯⁢𝟏q2⁢𝟎l2⁢𝟏q1⁢𝟎l1 where qi>0 and lj>0 for all i∈[b] and j∈[2,b]. Note that l1 can be 0. For k with such a representation, its block count, b⁢l⁢(k)=b.

The main result of our paper establishes a relationship between the block count of a number and the minimum number of terms needed to construct a DNF with exactly that many satisfying assignments.

Theorem 3 (Main Result).

For every k≥3,

log⁡(b⁢l⁢(k)+1)≤β⁢(k)≤min⁡{20⁢log⁡k⁢log⁡log⁡k,b⁢l⁢(k)+1}.

This represents the first o⁢(log⁡k) construction for this problem. We also conjecture that the value of β⁢(k) is polynomial in log⁡(b⁢l⁢(k)+1).

Conjecture 4.

There exists a sufficiently large constant C and a function f⁢(x), which is polynomial in x such that for every k∈ℕ, β⁢(k)≤C⋅f⁢(log⁡(b⁢l⁢(k))).

Organization

The rest of the paper is organized as follows. In Section 2, we establish a connection between the problem of finding minimum-sized DNFs with exactly k satisfying assignments and the theory of ideals of set systems. Section 3 provides the proof of our lower bound, while Section  4, which forms the technical core of the paper, presents the proof of upper bound. We finally conclude in Section 5.

2 Connection to Ideals of Sets System

We now show that a natural problem on the ideals of sets system (which is also of independent interest) is equivalent to finding small monotone DNFs (formulas consisting of only variables in positive form) with exactly a given number of satisfying assignments. We use this formulation to derive our upper bounds for β⁢(k).

2.1 Notation

ℕ denotes the set of natural numbers. We use log⁡k to denote log2⁡k. For a set S, |S| and 2S denote its cardinality and power set, respectively. The union of A and B is denoted as A∪B. The union of two disjoint sets A,B is denoted as A⊔B. The notation [a,b] represents {a,a+1⁢⋯⁢b} and [b] represents [1,b]. For every number i, we create distinct copies i0,i1,i2⁢⋯. The set [w]i represents {1i,2i⁢⋯⁢wi}. Note that the sets [w],[w]0,[w]1⁢⋯ are all different from each other as these sets are pairwise disjoint. Given a family of sets 𝒮={S1,S2⁢⋯⁢St} and a set X, we define 𝒮+X={S1∪X,S2∪X⁢⋯⁢St∪X}.

An anti-chain is a subset 𝒜 of a partially ordered set P such that any two distinct elements of 𝒜 are incomparable. An (order) ideal (also called semi-ideal, down-set, or monotone decreasing subset) of P is a subset I of P such that if t∈I and s≤t, then s∈I. Similarly, a dual order ideal (also called up-set or monotone increasing subset) is a subset I of P such that if t∈I and s≥t, then s∈I [18]. When P is finite, there is a one-to-one correspondence between anti-chains of P and order ideals: the anti-chain 𝒜 associated with the order ideal I is the set of maximal elements of I, while I={s∈P∣s≤t⁢ for some ⁢t∈𝒜}. Then the anti-chain 𝒜 is said to generate the ideal I=𝐈𝐃⁢(𝒜).

▶ Remark 5.

There may be some difference of opinion with the definition of ideal given above since, in some contexts, a slightly different definition is used for ideals. However, in this paper, we only study set systems, and with respect to set systems, most authors use the above definition for ideals. For example, see Bollabás [4].

2.2 Problem Definition

Definition 6.

The ideal generated by a family of sets, 𝒮={S1,S2⁢⋯⁢Sα}, is 𝐈𝐃⁢(𝒮)=2S1⁢⋃2S2⁢⋃⋯⁢2Sα.

Note that the minimal family of sets that generates a given ideal is an antichain.

Definition 7.

Given a natural number k, α⁢(k) is defined to be the minimum |𝒮| for which |𝐈𝐃⁢(𝒮)|=k.

Observe that for every natural number k, there is a family of sets 𝒮={∅,{1},{2}⁢⋯⁢{k−1}} such that |𝐈𝐃⁢(𝒮)|=k. Therefore, α⁢(k) exists for all k and moreover, α⁢(k)≤k. In this work, we establish more meaningful bounds on α⁢(k).

2.3 Combinatorial Background

Ideals and their symmetric counterpart filters are central concepts in the study of set systems. These concepts appear in some of the most fundamental theorems regarding set systems. For example, Bollobás and Thomason proved that every non-trivial monotone increasing/decreasing property of subsets of a set has a threshold function [5], in the probabilistic model where each element is chosen with probability p. Here, monotone decreasing property corresponds to ideals. This is one of the most significant results in the theory of random graphs (see chapter 6 of [4]).

Another well-known result on ideals and dual order ideals is Kleitman’s lemma [12], which triggered a long line of research on correlation-type inequalities, culminating in the Four Functions Theorem of Ahlswede and Daykin [1] (see chapter 6 of [3]). When studying extremal problems on set systems, it is often sufficient to prove the extremality restricted to set systems that are ideals or dual-order ideals. For example, see Kleitman’s proof establishing a tight bound for the cardinality of maximal l-intersecting families [13] (see chapter 13 of [4]).

In chapter 17 of [4], Bollabás discusses theorems of the form (m,k)→(r,s) regarding traces. Such a theorem means if the universe X=[k] and a family ℱ consists of m subsets of X, then there exists an s-element subset S of X such that when we take the intersection of S with the members of ℱ, we get at least r distinct subsets. Alon [2] and Frankl [11] independently proved that to establish any theorem of the form (m,k)→(r,s), it is sufficient to prove the corresponding statement when ℱ is restricted to an ideal [11].

Ideals are also studied under the name abstract simplicial complex or abstract complex. This represents a combinatorial description of the geometric notion of a simplicial complex [15]. In the context of matroids and greedoids, these are also referred to as independence systems [14].

Several questions closely related to our work have been studied in the literature. For instance, Duffus, Howard, and Leader investigated the maximum cardinality of an anti-chain that can be present in a given ideal [9]. The problem we discuss in this paper – finding the minimum cardinality α⁢(k) of the anti-chain that can generate an ideal of a given size k – has been examined by both computer scientists and combinatorialists due to its applications in model counting.

2.4 Connection between Ideals and Monotone DNFs

The model counting problem for monotone DNF formulae has an interesting connection to the ideals of set systems. In fact, these problems are essentially equivalent. Let x1,x2,…,xm be the set of positive literals used in the monotone DNF formulae we consider. An assignment assigns a truth value to each of these m variables; if the formula evaluates to TRUE under this assignment, then the assignment is called a satisfying assignment.

Take the universe U=[m]={1,…,m}. Given any subset S of U, we can associate to S a term TS=⋀i∈Sxi. Conversely, given a term T={xi1∧xi2∧…∧xit} of a monotone DNF formula, we can associate the subset ST={i1,i2,…,it} to T. Also, to a family ℱ={S1,S2,…,St} of subsets of U, we can associate a monotone DNF formula fℱ=T⁢(S1)∨T⁢(S2)∨…∨T⁢(St). Conversely, to a monotone DNF formula f=T1∨T2∨…∨Tℓ, we can associate a family of subsets of U, namely ℱf={ST1,ST2,…,STℓ}.

Thus, there is a one-to-one correspondence between monotone DNF formulae using variables x1,x2,…,xm and families of subsets of U.

Let ℱ be a family of subsets. Then let ℱ¯={S¯:S∈ℱ}, where S¯=U∖S is the complement of S. We can show that the set of satisfying assignments of a monotone DNF formula f has a one-to-one correspondence with the ideal generated by the family ℱf¯. This is because for f to be satisfied, at least one term of f must be satisfied. If term Ti is satisfied, then all literals appearing in Ti must be set to TRUE. So, the set of literals that are set to FALSE must correspond to a set of indices S′ such that S′⊆STi¯. In other words, S′∈𝐈𝐃⁢(ℱf¯).

The converse is also true: For S′∈𝐈𝐃⁢(ℱf¯), the assignment where each variable xi with i∈S′ is set to FALSE and the remaining variables set to TRUE will be a satisfying assignment for f. This is because there will be a superset of S′ in ℱf¯, and the term in f that corresponds to the complement of this superset would evaluate to TRUE. Since every satisfying assignment can be bijectively mapped to the set of variables that are set to FALSE, the set of satisfying assignments of f are bijectively mapped to the ideal of ℱf¯. From this discussion, we have:

Theorem 8.

Let k be a positive integer. If ℱ is a family of subsets with |𝐈𝐃⁢(ℱ)|=k, then there exists a monotone DNF formula f=fℱf¯ with exactly k satisfying assignments. In particular, a monotone DNF formula with the smallest number of terms and exactly k satisfying assignments will have α⁢(k) terms.

Corollary 9.

For k≥1, α⁢(k)≥β⁢(k).

▶ Remark 10.

A similar statement can be made about monotone CNF formulae. The difference is that k would represent the number of non-satisfying assignments, and a subset in the ideal would correspond to the variables assigned TRUE.

3 Proof of Lower Bound

We first state the inclusion-exclusion principle

Theorem 11.

For finite sets V1,V2⁢⋯⁢Vq

|⋃i=1qVi|=∑∅≠J⊆{1,2⁢⋯,q}(−1)|J|+1⁢|⋂j∈JVj|.

For a formulae ℱ, let S⁢o⁢l⁢(ℱ) denote the set of satisfying assignments for ℱ.

Observation 12.

For a DNF formula ℱ=T1∨T2⁢⋯∨Tq, we have

|S⁢o⁢l⁢(ℱ)|=∑∅≠J⊆{1,2⁢⋯,q}(−1)|J|+1⁢|S⁢o⁢l⁢(⋀j∈JTj)|.
Proof.

For the DNF formula ℱ=T1∨T2⁢⋯∨Tq, it is easy to see that

S⁢o⁢l⁢(ℱ)=⋃i=1qS⁢o⁢l⁢(Ti).

Therefore, from Theorem 11

|⋃i=1qS⁢o⁢l⁢(Ti)|=∑∅≠J⊆{1,2⁢⋯,q}(−1)|J|+1⁢|⋂j∈JS⁢o⁢l⁢(Tj)|

Observe that S⁢o⁢l⁢(Ti)∩S⁢o⁢l⁢(Tj)=S⁢o⁢l⁢(Ti∧Tj). Therefore,

∑∅≠J⊆{1,2⁢⋯,q}(−1)|J|+1⁢|⋂j∈JS⁢o⁢l⁢(Tj)|=∑∅≠J⊆{1,2⁢⋯,q}(−1)|J|+1⁢|S⁢o⁢l⁢(⋀j∈JTj)|

◀

Observation 13.

For any non-empty set J⊆{1,2⁢⋯,q}, the value of |S⁢o⁢l⁢(⋀j∈JTj)| is either 0 or of the form 2α for some α∈ℕ∪{0}.

Proof.

Consider a literal y. We have the following cases

  • ■

    If the literal y appears positively in Ti and negatively in Tj for some i,j∈J, then ⋀j∈JTj has no solution.

  • ■

    If the literal y appears positively for at least one Ti for i∈J and never appears negatively for any Tj for j∈J, then y must be true in all satisfying assignments.

  • ■

    Similarly, if the literal y appears negatively for at least one Ti for i∈J and never appears positively for any Tj for j∈J, then y must be false in all satisfying assignments.

  • ■

    If the literal y does not appear in any Tj for j∈J, then it can take the true or false value in an assignment.

It is now easy to see that if there are α such literals which never appeared in any Tj for j∈J, there will be 2α many satisfying assignments. ◀

Observation 14.

Let t∈ℕ and xi,yi∈{0}∪ℕ for all i∈[t]. If k=∑i∈[t](−1)xi⁢2yi≥1, then b⁢l⁢(k)≤t.

Proof.

We prove this by induction on t. When t=1, x1 must be even since k≥1. Therefore, k is of the form 2y1 and hence b⁢l⁢(k)=1=t.

Let t>1 and m=k−mini∈[t](−1)xi2yi. For i∈[t], if there exists an xi which is odd, then mini∈[t](−1)xi2yi<0 and hence m≥1. On the other hand, if for all i∈[t], xi is even, then m can be written as the sum of positive integers. Therefore, m≥1. Therefore, by the induction assumption b⁢l⁢(m)≤t−1.

Observe that when (−1)xi⁢2yi is added to the binary representation of m, 1 is either added or subtracted at the (yi+1)th bit of m. Suppose the (yi+1)th bit of m be 0 (respectively 1). Then adding (respectively subtracting) 1 at the (yi+1)th position changes the number of blocks by at most 1. On the other hand, when the (yi+1)th bit of m is 1 (respectively 0), adding (respectively subtracting) 1 at the (yi+1)th position flips all contiguous 1s (respectively 0s) at and before (yi+1)th position and the first preceding 0 (respectively 1). Therefore, the number of blocks change by at most 1.

Therefore, as k=m+(−1)xt⁢2yt, b⁢l⁢(k)≤b⁢l⁢(m)+1≤t. ◀

Lemma 15.

For every k∈ℕ, log⁡(b⁢l⁢(k)+1)≤β⁢(k).

Proof.

Towards a contradiction, let there exist some k∈ℕ such that log⁡(b⁢l⁢(k)+1)>β⁢(k). Let ℱ=T1∨T2⁢⋯∨Tβ⁢(k) be a DNF such that it has exactly k solutions. From Observation 12,

|S⁢o⁢l⁢(ℱ)|=∑∅≠J⊆{1,2⁢⋯,β⁢(k)}(−1)|J|+1⁢|S⁢o⁢l⁢(⋀j∈JTj)|

From Observation 13, it is easy to see that |S⁢o⁢l⁢(ℱ)| can be written as the sum or difference of 2β⁢(k) or less terms that are powers of 2. Therefore, from Observation 14, b⁢l⁢(k)≤2β⁢(k)−1<b⁢l⁢(k)+1−1=b⁢l⁢(k). This is a contradiction. ◀ From Corollary 9, it is also easy to see the following corollary now.

Corollary 16.

For every k∈ℕ, log⁡(b⁢l⁢(k)+1)≤α⁢(k).

4 Proof of Upper Bound

We first establish a framework for analyzing the size of ideals generated by families of sets. Our approach leverages the inclusion-exclusion principle and introduces two key operations – splitting and lifting – that will be central to our construction.

4.1 Technical Preliminaries

A key insight for our analysis is understanding how the inclusion-exclusion principle applies to unions of power sets. This is captured in the following observation:

Observation 17.

For finite sets V1,V2⁢⋯⁢Vq

|⋃i=1q2Vi|=∑j=1q(−1)j+1⁢(∑1≤i1<⋯<ij≤q2|Vi1∩⋯∩Vij|).
Proof.

From the inclusion-exclusion principle,

|⋃i=1q2Vi|=∑j=1q(−1)j+1⁢(∑1≤i1<⋯<ij≤q|2Vi1∩⋯∩2Vij|)
=∑j=1q(−1)j+1⁢(∑1≤i1<⋯<ij≤q|2Vi1∩⋯∩Vij|)=∑j=1q(−1)j+1⁢(∑1≤i1<⋯<ij≤q2|Vi1∩⋯∩Vij|)

◀

4.2 Fundamental Operations: Splitting and Lifting

We now introduce two fundamental operations that will serve as building blocks for our upper-bound construction. These operations allow us to construct ideals with specific cardinalities efficiently.

Lemma 18 (Splitting lemma).

For m,k∈ℕ, α⁢(m+k)≤α⁢(m)+α⁢(k+1).

Proof.

Let 𝒮,𝒯 be family of sets such that S∩T=∅ for all S∈𝒮 and T∈𝒯, where

|𝒮|=α⁢(m)&|𝐈𝐃⁢(𝒮)|=m
|𝒯|=α⁢(k+1)&|𝐈𝐃⁢(𝒯)|=k+1

Observe that, by construction 𝐈𝐃⁢(𝒮)∩𝐈𝐃⁢(𝒯)={∅}. Therefore,

|𝐈𝐃⁢(𝒮∪𝒯)|=|𝐈𝐃⁢(𝒮)|+|𝐈𝐃⁢(𝒯)|−1=m+k

It now follows that,

α⁢(m+k)≤|𝒮∪𝒯|=|𝒮|+|𝒯|=α⁢(m)+α⁢(k+1)

◀

The splitting lemma essentially tells us that to construct an ideal of size m+k, we can combine ideals of sizes m and k+1 that share only the empty set. This allows us to decompose the problem of constructing larger ideals into constructing smaller ones.

Our second fundamental operation is the lifting lemma, which provides an efficient way to construct ideals whose cardinality is a power of 2 multiplied by a given number:

Lemma 19 (Lifting lemma).

For every t,k∈ℕ, α⁢(2t⋅k)≤α⁢(k).

Proof.

Let 𝒮={S1,S2⁢⋯⁢Sα⁢(k)} be a family of sets such that |𝐈𝐃⁢(𝒮)|=k. Let the set X={x1,x2⁢⋯⁢xt} be such that X∩Si=∅ for all Si∈𝒮. We define Si′=Si⊔X for all i∈[α⁢(k)] and 𝒮′={S1′,S2′⁢⋯⁢Sα⁢(k)′}. By Observation 17,

|𝐈𝐃⁢(𝒮′)|=|⋃i=1α⁢(k)2Si′|=∑j=1α⁢(k)(−1)j+1⁢(∑1≤i1<⋯<ij≤α⁢(k)2|Si1′∩⋯∩Sij′|)

By construction,

=∑j=1α⁢(k)(−1)j+1⁢(∑1≤i1<⋯<ij≤α⁢(k)2|(Si1∩⋯∩Sij)⊔X|)
=2|X|⁢∑j=1α⁢(k)(−1)j+1⁢(∑1≤i1<⋯<ij≤α⁢(k)2|Si1∩⋯∩Sij|)

By Observation 17,

2|X|⁢|⋃i=1α⁢(k)2Si|=2t⁢|𝐈𝐃⁢(𝒮)|=2t⋅k

Therefore, α⁢(2t⋅k)≤|𝒮′|=|𝒮|=α⁢(k) ◀

The lifting lemma provides a powerful tool: it shows that we can construct an ideal of size 2t⋅k using the same number of generators as an ideal of size k. Intuitively, this is achieved by adding t new elements to each generator set in a way that preserves the relative structure of the original ideal.

4.3 Simple Upper Bound Based on Block Count

Using the operations we’ve developed, we can now establish a simple relationship between α⁢(k) and the block count of k:

Lemma 20.

For every k∈ℕ, α⁢(k)≤b⁢l⁢(k)+1.

Proof.

We prove this by induction on the block count of k. We first give a construction for the base case, that is, for any k with b⁢l⁢(k)=1, say k=𝟏q1⁢𝟎l1, where q1≥1 and l1≥0. Consider the sets S1=[q1+l1−1]1 and S2=[q1−1]2⊔[l1]1. Note that S1⁢⋂S2=[l1]1. We now observe that,

|𝐈𝐃⁢({S1,S2})|=2|S1|+2|S2|−2|S1⁢⋂S2|=2q1+l1−2l1=𝟏q1⁢𝟎l1

Thus for k, with b⁢l⁢(k)=1, α⁢(k)≤2. We now consider any number k with b⁢l⁢(k)=b≥2, say 1qb⁢0lb⁢⋯⁢1q2⁢0l2⁢1q1⁢0l1, where qi>0 and lj>0 for all i∈[b] and j∈[2,b]. From the Lifting lemma,

α⁢(k)=α⁢(1qb⁢0lb⁢⋯⁢1q2⁢0l2⁢1q1⁢0l1)≤α⁢(1qb⁢0lb⁢⋯⁢1q2⁢0l2⁢1q1)=α⁢(1qb⁢0lb⁢⋯⁢1q2⁢0l2+q1+1q1)

From the Splitting lemma,

≤α⁢(1qb⁢0lb⁢⋯⁢1q2⁢0l2+q1)+α⁢(1q1+1)=α⁢(1qb⁢0lb⁢⋯⁢1q2⁢0l2+q1)+α⁢(2q1)

From the induction assumption,

≤b+α⁢(2q1)=b+1=b⁢l⁢(k)+1

◀

This lemma establishes that α⁢(k) grows no faster than the block count of k plus one. While this already gives us a non-trivial upper bound, we will develop tighter bounds in the next section.

4.4 Tighter Upper Bound Construction

We now present our main technical result, which establishes a much tighter bound on α⁢(k). The key insight is to construct specialized sets for numbers of a particular form and then extend these constructions to all natural numbers.

Theorem 21.

For m of the form 23⁢q2+β where β<2q2, α⁢(m)≤(q+1)⁢⌈log⁡q⌉+4⁢q+6.

The proof of this theorem is technical and will be presented in Section 4.5. First, we’ll show how this theorem helps us establish our main result, Theorem 3.

Observation 22.

For every k∈ℕ, there exists a q such that k=23⁢q2+γ⋅2q2+β<23⁢(q+1)2 where γ=⌊k−23⁢q22q2⌋ and 0≤β<2q2.

Proof.

For every number k, there exists a q such that 23⁢q2≤k<23⁢(q+1)2. By dividing k−23⁢q2 by 2q2, it follows that γ=⌊k−23⁢q22q2⌋ is the quotient and 0≤β<2q2 is the remainder. ◀

This observation shows that any natural number can be decomposed into the form required by Theorem 21, plus an additional term. We now show how to handle this additional term:

Lemma 23.

α⁢(23⁢q2+γ⋅2q2+β)≤α⁢(23⁢q2+β)+α⁢(γ)+1

Proof.

From the Splitting lemma,

α⁢(23⁢q2+γ⋅2q2+β)≤α⁢(23⁢q2+β)+α⁢(γ⋅2q2+1)
≤α⁢(23⁢q2+β)+α⁢(γ⋅2q2)+α⁢(2)=α⁢(23⁢q2+β)+α⁢(γ⋅2q2)+1

From the Lifting lemma,

=α⁢(23⁢q2+β)+α⁢(γ)+1

◀

With these pieces in place, we are now ready to prove our main result, which provides an O⁢(log⁡k⁢log⁡log⁡k) upper bound on α⁢(k).

Proof of Theorem 3.

From Observation 22, for every k, there exists a q such that k=23⁢q2+γ⋅2q2+β<23⁢(q+1)2 where γ=⌊k−23⁢q22q2⌋ and 0≤β<2q2.

When 3≤k<20, it is obvious that α⁢(k)≤k<20⁢log⁡k⁢log⁡log⁡k. So, we can assume that 20≤k and therefore q≥1.

Observation 24.

If log⁡3≤log⁡k≤30000, then ⌈0.5⁢log⁡k+1⌉<20⁢log⁡k⁢log⁡log⁡k.

From our simple upper bound in Lemma 20 along with Observation 24, we get that for all q<100,

α⁢(k)≤⌈0.5⁢log⁡k⌉+1<20⁢log⁡k⁢log⁡log⁡k

We now inductively prove Theorem 3 for q≥100, inducting on q.

α⁢(k)=α⁢(23⁢q2+γ⋅2q2+β)

When γ=0, by Theorem 21, α⁢(k)≤20⁢log⁡k⁢log⁡log⁡k. For γ>0, from Lemma 23,

≤α⁢(23⁢q2+β)+α⁢(γ)+1

From Theorem 21,

≤(q+1)⁢⌈log⁡q⌉+4⁢q+7+α⁢(γ)

When γ≤2 and log⁡k>30000, as α⁢(1)=α⁢(2)=1, α⁢(k)≤20⁢log⁡k⁢log⁡log⁡k. Therefore, for γ≥3, by induction assumption,

α⁢(k)≤(q+1)⁢⌈log⁡q⌉+4⁢q+7+20⁢log⁡γ⁢log⁡log⁡γ

As log⁡γ≤log⁡k−q2≤3⁢(q+1)2−q2≤2.1⁢q2 for q≥100,

≤(q+1)⁢⌈log⁡q⌉+4⁢q+7+20⁢2.1⁢q⁢log⁡log⁡k

As (q+1)⁢⌈log⁡q⌉+4⁢q+7≤2⁢q⁢log⁡q for q≥100,

≤2⁢q⁢log⁡q+20⁢2.1⁢q⁢log⁡log⁡k≤q⁢log⁡log⁡k+20⁢2.1⁢q⁢log⁡log⁡k
=(20⁢2.1+1)⁢q⁢log⁡log⁡k≤20⁢3⁢q⁢log⁡log⁡k≤20⁢log⁡k⁢log⁡log⁡k

◀

4.5 Proof of Theorem 21

We now present the most technical part of our proof: constructing an ideal with specific properties for numbers of the form 23⁢q2+β where β<2q2. The key idea is to carefully design a collection of sets based on the binary representation of β.

Let m=23⁢q2+β where β<2q2. For i,j∈[0,q−1], we define Fi⁢j in the following way:

  • ■

    If the (j⁢q+i+1)th least significant bit of β is 1, then fix Fi⁢j=∅.
    Let ℱ0 be the family of all such sets.

  • ■

    If the (j⁢q+i+1)th least significant bit of β is 0, then fix Fi⁢j=[i]j⁢q+i.
    Let ℱ1 be the family of all such sets.

We note that the least significant bit of β is indexed to be the 1st bit. On the other hand the indices i,j start from 0. From this construction, several important properties immediately follow:

▶ Remark 25.

For all i,j∈[0,q−1], Fi⁢j∩[q2]=∅.

▶ Remark 26.

For any Fi⁢j,Fi′⁢j′∈ℱ1, Fi⁢j⁢⋂Fi′⁢j′≠∅ if and only if i=i′ and j=j′.

▶ Remark 27.

β+∑Fi⁢j∈ℱ12j⁢q+|Fi⁢j|=β+∑Fi⁢j∈ℱ12j⁢q+i=𝟏q2=2q2−1

▶ Remark 28.

∑Fi⁢j∈ℱ02j⁢q+|Fi⁢j|=∑Fi⁢j∈ℱ02j⁢q

These observations lead to the following key relationship:

Corollary 29.

2q2−∑i,j∈[0,q−1]2j⁢q+|Fi⁢j|=β+1−∑Fi⁢j∈ℱ02j⁢q

Using these Fi⁢j sets, we construct two families of sets that will form the basis of our ideal. For all i,j∈[0,q−1], let Si′=[q2],Tj′=[j⁢q] and let

Si=(⋃j=0q−1Fi⁢j)⁢⨆Si′&Tj=(⋃i=0q−1Fi⁢j)⁢⨆Tj′

We define 𝒮={S0,⋯⁢Sq−1},𝒮′={S0′,⋯⁢Sq−1′},𝒯={T0,⋯⁢Tq−1} and 𝒯′={T0′,⋯⁢Tq−1′}

Our strategy is to compute the cardinality of the ideal generated by 𝒮∪𝒯. We want to show that α⁢(|𝐈𝐃⁢(𝒮∪𝒯)|)≤2⁢q, and since q=O⁢(log⁡k), this would give us the desired upper bound if |𝐈𝐃⁢(𝒮∪𝒯)|=β=m−23⁢q2. However, this equality doesn’t hold exactly, but we’ll show that the difference has a small α-value.

Computing |𝐈𝐃⁢(𝒮∪𝒯)| directly is complex, so we first relate it to |𝐈𝐃⁢(𝒮′∪𝒯′)|, which equals 2q2 because all sets in 𝒮′ and 𝒯′ are subsets of [q2] and every Si′=[q2].

Observation 30.

Si∩Tj=[j⁢q]⁢⨆Fi⁢j

Proof.

By Remark 25 and Remark 26,

Si∩Tj=((⋃j′=0q−1Fi⁢j)⊔[q2])∩((⋃i′=0q−1Fi⁢j)⊔[j⁢q])=[j⁢q]⁢⨆Fi⁢j

◀

Observation 31.

For p<i, 2Ti∩2Tp=2[p⁢q]=2Ti′∩2Tp′ and 2Si∩2Sp=2[q2]=2Si′∩2Sp′.

Proof.

By Remark 25 and Remark 26,

2Ti∩2Tp=2Ti∩Tp=2Ti′∩Tp′=2[p⁢q]=2Ti′∩2Tp′
2Si∩2Sp=2Si∩Sp=2Si′∩Sp′=2[q2]=2Si′∩2Sp′

◀

These observations allow us to relate terms in the inclusion-exclusion expansions of |𝐈𝐃⁢(𝒮∪𝒯)| and |𝐈𝐃⁢(𝒮′∪𝒯′)|. We define:

(A1,A2⁢⋯⁢A2⁢q)=(2S0,2S1⁢⋯⁢2Sq−1,2T0,2T1⁢⋯⁢2Tq−1)
(A1′,A2′⁢⋯⁢A2⁢q′)=(2S0′,2S1′⁢⋯⁢2Sq−1′,2T0′,2T1′⁢⋯⁢2Tq−1′)

We note that the indices of A and A′ start at 1 while indices of S,S′,T,T′ start at 0.

Observation 32.

For any ℓ≥3, let I={i1,i2⁢⋯⁢iℓ} such that 1≤i1<⋯<iℓ≤2⁢q

|⋂j∈IAj|=|⋂j∈IAj′|.
Proof.

As ℓ≥3, by pigeon hole principle, there exists two sets Aix and Aiy such that either Aix,Aiy∈{2S0,2S1⁢⋯⁢2Sq−1} or Aix,Aiy∈{2T0,2T1⁢⋯⁢2Tq−1}. From Observation 31, Aix∩Aiy⊂2[q2]. It follows that ⋂j∈IAj⊂2[q2]. Therefore,

|⋂j∈IAj|=|⋂j∈I(Aj⁢⋂2[q2])|=|⋂j∈IAj′|

◀

This allows us to compute the difference between the two ideals’ cardinalities:

Observation 33.
|𝐈𝐃⁢(𝒮∪𝒯)|−|𝐈𝐃⁢(𝒮′∪𝒯′)|
=(∑i=0q−1|2Si|−∑i=0q−1|2Si′|)+(∑j=0q−1|2Tj|−∑j=0q−1|2Tj′|)−(∑i,j∈[0,q−1](|2Si⁢⋂Tj|)−∑i,j∈[0,q−1](|2Si′⁢⋂Tj′|))

Through a series of algebraic manipulations (Proof in Section A.2), we derive the exact cardinality of our constructed ideal:

Lemma 34.

|𝐈𝐃⁢(𝒮∪𝒯)|=∑i=0q−1|2Si|+∑j=0q−1|2Tj|−∑i,j∈[0,q−1]2j⁢q⁢(2|Fi⁢j|)+(q−1)⁢(∑j=0q−12j⁢q−2q2)

This leads to a bound on the α-value of our constructed ideal (as |𝒮∪𝒯|=2⁢q):

Corollary 35.

α⁢(∑i=0q−1|2Si|+∑j=0q−1|2Tj|−∑i,j∈[0,q−1]2j⁢q⁢(2|Fi⁢j|)+(q−1)⁢(∑j=0q−12j⁢q−2q2))=α⁢(|𝐈𝐃⁢(𝒮∪𝒯)|)≤2⁢q

Our goal is to show that α⁢(m−|𝐈𝐃⁢(𝒮∪𝒯)|)=O⁢(q⁢log⁡q), which would imply α⁢(m)=O⁢(q⁢log⁡q)=O⁢(log⁡k⁢log⁡log⁡k) by the splitting lemma and Corollary 35. However, the expression for |𝐈𝐃⁢(𝒮∪𝒯)| contains inconvenient terms like ∑i=0q−1|2Si|. We first eliminate these terms:

Observation 36.

α⁢(23⁢q2−1−∑i=0q−1|2Si|−∑j=0q−1|2Tj|+2q2)≤2⁢q+3

Proof.

From Observation 14, 23⁢q2−1−∑i=0q−1|2Si|−∑j=0q−1|2Tj|+2q2 has at most 2⁢q+2 blocks. Therefore, from our earlier results on block counts and α values, α⁢(23⁢q2−1−∑i=0q−1|2Si|−∑j=0q−1|2Tj|+2q2)≤2⁢q+3 ◀

For clarity, we define two auxiliary values: t1=23⁢q2−1+2q2−1−∑i,j∈[0,q−1]2j⁢q⁢(2|Fi⁢j|)+(q−1)⁢(∑j=0q−12j⁢q−2q2)

t2=23⁢q2−1+∑Fi⁢j∈ℱ02j⁢q−(q−1)⁢(∑j=0q−12j⁢q−2q2)

Here, t1 is the sum of |𝐈𝐃⁢(𝒮∪𝒯)| and the expression from Observation 36. We now show that t2=m−t1:

Observation 37.

m=t1+t2

Proof.

By definition, t1+t2=23⁢q2+2q2−1−∑i,j∈[0,q−1]2j⁢q+|Fi⁢j|+∑Fi⁢j∈ℱ02j⁢q

From Corollary 29, =23⁢q2+β=m ◀

Observation 38.

α⁢(t1)≤4⁢q+3

Proof.

This follows from the splitting lemma along with Corollary 35 and Observation 36. ◀

By the splitting lemma and Observation 37, it is now sufficient to prove that α⁢(t2+1) is small. We’ll show that t2 can be written in a special form that allows us to bound its α-value efficiently:

Observation 39.

There exists −1≤aj≤q−1 for j∈[0,q−1] and aq=−(q−1), for which t2=23⁢q2−1−∑j=0qaj⁢2j⁢q.

Proof.

t2=23⁢q2−1+∑Fi⁢j∈ℱ02j⁢q−(q−1)⁢(∑j=0q−12j⁢q−2q2)

For a given j, let 0≤bj≤q be the number of Fi⁢j∈ℱ0 =23⁢q2−1+(q−1)⁢2q2−∑j=0q−1(q−1−bj)⁢2j⁢q

Therefore, for some −1≤aj≤q−1 for j∈[0,q−1] and aq=−(q−1) =23⁢q2−1−∑j=0qaj⁢2j⁢q ◀

Finally, we show that numbers with this special structure have a small α-value:

Lemma 40.

For any |aj|≤q−1 for j∈[0,q], α⁢(23⁢q2−1−∑j=0qaj⁢2j⁢q+1)≤(q+1)⁢⌈log⁡q⌉+3.

Proof.

The binary representation of |aj| has at most ⌈log⁡q⌉ non-zero bits. Therefore, |aj|⁢2j⁢q has at most ⌈log⁡q⌉ non-zero bits in its binary representation. This means ∑j=0qaj⁢2j⁢q can be written as the sum or difference of (q+1)⁢⌈log⁡q⌉ powers of 2. From our earlier results on block counts, 23⁢q2−1−∑j=0qaj⁢2j⁢q+1 has at most (q+1)⁢⌈log⁡q⌉+2 blocks. Therefore, α⁢(23⁢q2−1−∑j=0qaj⁢2j⁢q+1)≤(q+1)⁢⌈log⁡q⌉+3 ◀

Corollary 41.

α⁢(t2+1)≤(q+1)⁢⌈log⁡q⌉+3

Combining all these results, Theorem 21 follows from the splitting lemma along with Corollary 41, Observation 38, and Observation 37.

5 Conclusion and Open Problems

We have established that for every k≥3, there exists a DNF or CNF with exactly k satisfying assignments using at most O⁢(log⁡k⁢log⁡log⁡k) terms or clauses. Our construction provides the first o⁢(log⁡k) upper bound for this problem, significantly improving previous bounds [6]. The constructed DNFs also have the desirable property of being monotone, which simplifies their structure and analysis. On the other hand, we also give a lower bound showing that there exist infinitely many k∈ℕ requiring at least Ω⁢(log⁡log⁡k) terms or clauses. However, there remains a gap between our upper and lower bounds that presents an interesting avenue for future research.

We conjecture that the value of β⁢(k) is polynomial in log⁡(b⁢l⁢(k)+1), which would provide a more precise characterization of the relationship between the number of terms needed and the block structure of the number of solutions. Resolving this conjecture would further deepen our understanding of the structural properties of boolean formulas with a specific number of satisfying assignments.

The connection we established between this problem and the theory of ideals in set systems may also lead to further applications in other areas of combinatorics and computational complexity theory. In particular, the construction techniques we developed might be useful in addressing related questions about the expressiveness and succinctness of different representations of boolean functions.

References

  • [1] Rudolf Ahlswede and David E. Daykin. An inequality for the weights of two families of sets, their unions and intersections. Zeitschrift für Wahrscheinlichkeitstheorie und Verwandte Gebiete, 43:183–185, 1978.
  • [2] Noga Alon. On the density of sets of vectors. Discrete Mathematics, 46(2):199–202, 1983. doi:10.1016/0012-365X(83)90253-4.
  • [3] Noga Alon and Joel H. Spencer. The Probabilistic Method, chapter 6, pages 81–92. John Wiley & Sons, Ltd, 2000.
  • [4] Béla Bollobás. Combinatorics: Set Systems, Hypergraphs, Families of Vectors, and Combinatorial Probability. Cambridge University Press, USA, 1986.
  • [5] Béla Bollobás and Andrew G. Thomason. Threshold functions. Combinatorica, 7:35–38, 1987. doi:10.1007/BF02579198.
  • [6] Supratik Chakraborty, Dror Fried, Kuldeep S. Meel, and Moshe Y. Vardi. From weighted to unweighted model counting. In Qiang Yang and Michael J. Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 689–695. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/103.
  • [7] Adnan Darwiche and Pierre Marquis. A knowledge compilation map. J. Artif. Intell. Res., 17:229–264, 2002. doi:10.1613/jair.989.
  • [8] Carmel Domshlak and Jörg Hoffmann. Probabilistic planning via heuristic forward search and weighted model counting. J. Artif. Intell. Res., 30:565–620, 2007. doi:10.1613/jair.2289.
  • [9] Dwight Duffus, David Howard, and Imre Leader. The width of downsets. European Journal of Combinatorics, 79:46–59, 2019. doi:10.1016/j.ejc.2018.11.005.
  • [10] Jörg Flum and Martin Grohe. The parameterized complexity of counting problems. SIAM J. Comput., 33(4):892–922, 2004. doi:10.1137/S0097539703427203.
  • [11] Peter Frankl. On the trace of finite sets. J. Comb. Theory, Ser. A, 34:41–45, 1983. doi:10.1016/0097-3165(83)90038-9.
  • [12] Daniel J. Kleitman. Families of non-disjoint subsets. Journal of Combinatorial Theory, 1(1):153–155, 1966.
  • [13] Daniel J. Kleitman. On a combinatorial conjecture of erdös. Journal of Combinatorial Theory, 1(2):209–214, 1966.
  • [14] Bernhard Körte, Rainer Schräder, and László Lovász. Greedoids. Springer, January 1991.
  • [15] John M. Lee. Introduction to topological manifolds. Springer, January 2011.
  • [16] Dan Roth. On the hardness of approximate reasoning. Artif. Intell., 82(1-2):273–302, 1996. doi:10.1016/0004-3702(94)00092-1.
  • [17] Tian Sang, Fahiem Bacchus, Paul Beame, Henry A. Kautz, and Toniann Pitassi. Combining component caching and clause learning for effective model counting. In SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings, 2004. URL: http://www.satisfiability.org/SAT04/programme/21.pdf.
  • [18] Richard P. Stanley. Enumerative Combinatorics, volume 1. Cambridge University Press, USA, 2nd edition, 2011. pg. 282.
  • [19] Dan Suciu, Dan Olteanu, Christopher Ré, and Christoph Koch. Probabilistic databases. Springer Nature, 2022.
  • [20] Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM J. Comput., 8(3):410–421, 1979. doi:10.1137/0208032.
  • [21] Yexiang Xue, Arthur Choi, and Adnan Darwiche. Basing decisions on sentences in decision diagrams. In Jörg Hoffmann and Bart Selman, editors, Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, July 22-26, 2012, Toronto, Ontario, Canada, pages 842–849. AAAI Press, 2012. doi:10.1609/aaai.v26i1.8221.

Appendix A Deferred proofs

A.1 Proof of Observation 24

We claim that for every integer 3≤k≤230000,

⌈12⁢log2⁡k+1⌉< 20⁢log2⁡k⁢log2⁡(log2⁡k).
Proof.

Put x:=log2⁡k. Then x∈[log2⁡3, 30000]. The inequality ⌈y⌉<y+1 gives

⌈12⁢x+1⌉<12⁢x+2,

so it suffices to prove

f⁢(x):=12⁢x+2−20⁢x⁢log2⁡x<0for ⁢x∈[log2⁡3, 30000].

It is easy to see that

f′⁢(x)=12−10⁢log2⁡xx−20⁢log2⁡ex,f′′⁢(x)=5⁢log2⁡xx3/2> 0(x>1).

Hence f is convex on the entire interval. We can also compute that

f⁢(log2⁡3)≈−13.8< 0,f⁢(30000)≈−3.66×104< 0.

As both the end points of the convex function are negative, we know that the function is also negative everywhere between them. So, f⁢(x)<0 for all x∈[log2⁡3,30000]. Substituting x=log2⁡k yields the claimed inequality. ◀

A.2 Proof of Lemma 34

Proof.

Observe that

∑i=0i=q−1|2Si′|=q⋅2q2,∑j=0j=q−1|2Tj′|=∑j=0j=q−12j⁢k

Moreover, since all sets in 𝒮′ and 𝒯′ are subsets of [q2]

|𝐈𝐃⁢(𝒮′∪𝒯′)|=2q2
∑i,j∈[0,q−1](|2Si′⁢⋂Tj′|)=∑i,j∈[0,q−1](|2[j⁢k]|)=q⋅∑i=0i=q−12i⁢k

Substituting these values in Observation 33, we get |𝐈𝐃⁢(𝒮∪𝒯)|

=∑i=0i=q−1|2Si|+∑j=0j=q−1|2Tj|−∑i,j∈[0,q−1](|2Si⁢⋂Tj|)−q⋅2q2−∑i=0i=q−12i⁢k+q⋅∑i=0i=q−12i⁢k+2q2
=∑i=0i=q−1|2Si|+∑j=0j=q−1|2Tj|−∑i,j∈[0,q−1](|2Si⁢⋂Tj|)+(q−1)⁢(∑j=0j=q−12j⁢k−2q2)

From Observation 30,

=∑i=0i=q−1|2Si|+∑j=0j=q−1|2Tj|−∑i,j∈[0,q−1]2j⁢k⁢(2|Fi⁢j|)+(q−1)⁢(∑j=0j=q−12j⁢k−2q2).

◀