Model Counting meets $F_{0}$ Estimation

The complexity-theoretic study of model counting was initiated by Valiant who showed that this problem, in general, is #P-complete  (Valiant, 1979). This motivated researchers to investigate approximate model counting and in particular achieving $(\varepsilon,\delta)$-approximation schemes. The complexity of approximate model counting depends on its representation. When the model $\varphi$ is represented as a CNF formula $\varphi$, designing an efficient $(\varepsilon,\delta)$-approximation is NP-hard (Stockmeyer, 1983). In contrast, when it is represented as a DNF formula, model counting admits FPRAS (fully polynomial-time approximation scheme) (Karp and Luby, 1983; Karp et al., 1989). We will use #CNF to refer to the case when $\varphi$ is a CNF formula while #DNF to refer to the case when $\varphi$ is a DNF formula.

For #CNF, Stockmeyer (Stockmeyer, 1983) provided a hashing-based randomized procedure that can compute ($\varepsilon,\delta)$-approximation within time polynomial in $|\varphi|,\varepsilon,\delta$, given access to an NP oracle. Building on Stockmeyer’s approach and motivated by the unprecedented breakthroughs in the design of SAT solvers, researchers have proposed a series of algorithmic improvements that have allowed the hashing-based techniques for approximate model counting to scale to formulas involving hundreds of thousands of variables (Gomes et al., 2007b; Chakraborty et al., 2013b; Ermon et al., 2013; Ivrii et al., 2015; Chistikov et al., 2015; Chakraborty et al., 2016; Achlioptas and Theodoropoulos, 2017; Soos and Meel, 2019; Soos et al., 2020). The practical implementations substitute NP oracle with SAT solvers. In the context of model counting, we are primarily interested in time complexity and therefore, the number of NP queries is of key importance. The emphasis on the number of NP calls also stems from practice as the practical implementation of model counting algorithms have shown to spend over 99% of their time in the underlying SAT calls (Soos and Meel, 2019).

Karp and Luby (Karp and Luby, 1983) proposed the first FPRAS scheme for #DNF, which was subsequently improved in the follow-up works (Karp et al., 1989; Dagum et al., 2000). Chakraborty, Meel, and Vardi (Chakraborty et al., 2016) demonstrated that the hashing-based framework can be extended to #DNF, hereby providing a unified framework for both #CNF and #DNF. Meel, Shrotri, and Vardi (Meel et al., 2017, 2018, 2019) subsequently improved the complexity of the hashing-based approach for #DNF and observed that hashing-based techniques achieve better scalability than that of Monte Carlo techniques.

Estimating $(\varepsilon,\delta)$-approximation of the $k^{\rm th}$ frequency moments ($F_{k}$) is a central problem in the data streaming model (Alon et al., 1999). In particular, considerable work has been done in designing algorithms for estimating the $0^{th}$ frequency moment ($F_{0}$), the number of distinct elements in the stream. While designing streaming algorithms, the primary resource concerns are two-fold: space complexity and processing time per element. For an algorithm to be considered efficient, these should be ${\rm poly}(\log N,1/\epsilon)$ where $N$ is the size of the universe ¹¹1We ignore $O(\log{1\over\delta})$ factor in this discussion.

The first algorithm for computing $F_{0}$ with a constant factor approximation was proposed by Flajolet and Martin, who assumed the existence of hash functions with ideal properties resulting in an algorithm with undesirable space complexity (Flajolet and Martin, 1985). In their seminal work, Alon, Matias, and Szegedy designed an $O(\log N)$ space algorithm for $F_{0}$ with a constant approximation ratio that employs 2-universal hash functions (Alon et al., 1999). Subsequent investigations into hashing-based schemes by Gibbons and Tirthapura (Gibbons and Tirthapura, 2001) and Bar-Yossef, Kumar, and Sivakumar (Bar-Yossef et al., 2002) provided $(\varepsilon,\delta)$-approximation algorithms with space and time complexity $\log N\cdot{\rm poly}({1\over\varepsilon})$. Subsequently, Bar-Yossef et al. proposed three algorithms with improved space and time complexity (Bar-Yossef et al., [n. d.]). While the three algorithms employ hash functions, they differ conceptually in the usage of relevant random variables for the estimation of $F_{0}$. This line of work resulted in the development of an algorithm with optimal space complexity ${O}(\log N+{1\over\varepsilon^{2}})$ and $O(\log N)$ update time (Kane et al., 2010).

The above-mentioned works are in the setting where each data item $a_{i}$ is an element of the universe. Subsequently, there has been a series of results of estimating $F_{0}$ in rich scenarios with particular focus to handle the cases $a_{i}\subseteq[N]$ such as a list or a multidimensional range (Bar-Yossef et al., 2002; Pavan and Tirthapura, 2007; Tirthapura and Woodruff, 2012; Sun and Poon, 2009).

As mentioned above, the algorithmic developments for model counting and $F_{0}$ estimation have largely relied on the usage of hashing-based techniques and yet these developments have, surprisingly, been separate, and rarely has a work from one community been cited by the other. In this context, we wonder whether it is possible to bridge this gap and if such an exercise would contribute to new algorithms for model counting as well as for $F_{0}$ estimation? The main conceptual contribution of this work is an affirmative answer to the above question. First, we point out that the two well-known algorithms; Stockmeyer’s #CNF algorithm  (Stockmeyer, 1983) that is further refined by Chakraborty et. al.  (Chakraborty et al., 2016) and Gibbons and Tirthapura’s $F_{0}$ estimation algorithm (Gibbons and Tirthapura, 2001), are essentially the same.

The core idea of the hashing-based technique of Stockmeyer’s and Chakraborty et al’s scheme is to use pairwise independent hash functions to partition the solution space (satisfying assignments of a CNF formula) into roughly equal and small cells, wherein a cell is small if the number of solutions is less than a pre-computed threshold, denoted by $\mathsf{Thresh}$. Then a good estimate for the number of solutions is the number of solutions in an arbitrary cell $\times$ number of cells. To partition the solution space, pairwise independent hash functions are used. To determine the appropriate number of cells, the solution space is iteratively partitioned as follows. At the $m^{th}$ iteration, a hash function with range $\{0,1\}^{m}$ is considered resulting in cells $h^{-1}(y)$ for each $y\in\{0,1\}^{m}$. An NP oracle can be employed to check whether a particular cell (for example $h^{-1}(0^{m})$) is small by enumerating solutions one by one until we have either obtained $\mathsf{Thresh}$+1 number of solutions or we have exhaustively enumerated all the solutions. If the the cell $h^{-1}(0^{m})$ is small, then the algorithm outputs $t\times 2^{m}$ as an estimate where $t$ is the number of solutions in the cell $h^{-1}(0^{m})$. If the cell $h^{-1}(0^{m})$ is not small, then the algorithm moves on to the next iteration where a hash function with range $\{0,1\}^{m+1}$ is considered.

We now describe Gibbons and Tirthapura’s algorithm for $F_{0}$ estimation which we call the $\mathsf{Bucketing}$ algorithm. We will assume the universe $[N]=\{0,1\}^{n}$. The algorithm maintains a bucket of size $\mathsf{Thresh}$ and starts by picking a hash function $h:\{0,1\}^{n}\rightarrow\{0,1\}^{n}$. It iterates over sampling levels. At level $m$, when a data item $x$ comes, if $h(x)$ starts with $0^{m}$, then $x$ is added to the bucket. If the bucket overflows, then the sampling level is increased to $m+1$ and all elements $x$ in the bucket other than the ones with $h(x)=0^{m+1}$ are deleted. At the end of the stream, the value $t\times 2^{m}$ is output as the estimate where $t$ is the number of elements in the bucket and $m$ is the sampling level.

These two algorithms are conceptually the same. In the $\mathsf{Bucketing}$ algorithm, at the sampling level $m$, it looks at only the first $m$ bits of the hashed value; this is equivalent to considering a hash function with range $\{0,1\}^{m}$. Thus the bucket is nothing but all the elements in the stream that belong to the cell $h^{-1}(0^{m})$. The final estimate is the number of elements in the bucket times the number of cells, identical to Chakraborty et. al’s algorithm. In both algorithms, to obtain an $(\varepsilon,\delta)$ approximation, the $\mathsf{Thresh}$ value is chosen as $O({1\over\varepsilon^{2}})$ and the median of $O(\log{1\over\delta})$ independent estimations is output.

Motivated by the conceptual identity between the two algorithms, we further explore the connections between algorithms for model counting and $F_{0}$ estimation.

1. (1)

   We formalize a recipe to transform streaming algorithms for $F_{0}$ estimation to those for model counting. Such a transformation yields new $(\varepsilon,\delta)$-approximate algorithms for model counting, which are different from currently known algorithms. Recent studies in the fields of automated reasoning have highlighted the need for diverse approaches (Xu et al., 2008), and similar studies in the context of #DNF provided strong evidence to the power of diversity of approaches (Meel et al., 2018). In this context, these newly obtained algorithms open up several new interesting directions of research ranging from the development of MaxSAT solvers with native XOR support to open problems in designing FPRAS schemes.

2. (2)

   Given the central importance of #DNF (and its weighted variant) due to a recent surge of interest in scalable techniques for provenance in probabilistic databases (Senellart, 2018, 2019), a natural question is whether one can design efficient techniques in the distributed setting. In this work, we initiate the study of distributed #DNF. We then show that the transformation recipe from $F_{0}$ estimation to model counting allows us to view the problem of the design of distributed #DNF algorithms through the lens of distributed functional monitoring that is well studied in the data streaming literature.

3. (3)

   Building upon the connection between model counting and $F_{0}$ estimation, we design new algorithms to estimate $F_{0}$ over structured set streams where each element of the stream is a (succinct representation of a) subset of the universe. Thus, the stream is $S_{1},S_{2},\cdots$ where each $S_{i}\subseteq[N]$ and the goal is to estimate the $F_{0}$ of the stream, i.e. size of $\cup_{i}S_{i}$. In this scenario, a traditional $F_{0}$ streaming algorithm that processes each element of the set incurs high per-item processing time-complexity and is inefficient. Thus the goal is to design algorithms whose per-item time (time to process each $S_{i}$) is poly-logarithmic in the size of the universe. Structured set streams that are considered in the literature include 1-dimensional and multidimensional ranges (Pavan and Tirthapura, 2007; Tirthapura and Woodruff, 2012). Several interesting problems such as max-dominance norm (Cormode and Muthukrishnan, 2003), counting triangles in graphs (Bar-Yossef et al., 2002), and distinct summation problem (Considine et al., 2004) can be reduced to computing $F_{0}$ over such ranges.

   We observe that several structured sets can be represented as small DNF formulae and thus $F_{0}$ counting over these structured set data streams can be viewed as a special case of #DNF. Using the hashing-based techniques for #DNF, we obtain a general recipe for a rich class of structured sets that include multidimensional ranges, multidimensional arithmetic progressions, and affine spaces. Prior work on single and multidimensional ranges ²²2Please refer to Remark 1 in Section 5 for a discussion on the earlier work on multidimensional ranges (Tirthapura and Woodruff, 2012). had to rely on involved analysis for each of the specific instances, while our work provides a general recipe for both analysis and implementation.

We present notations and preliminaries in Section 2. We then present the transformation of $F_{0}$ estimation to model counting in Section 3. We then focus on distributed #DNF in Section 4. We then present the transformation of model counting algorithms to structured set streaming algorithms in Section 5. We conclude in Section 6 with a discussion of future research directions.

We would like to emphasize that the primary objective of this work is to provide a unifying framework for $F_{0}$ estimation and model counting. Therefore, when designing new algorithms based on the transformation recipes, we intentionally focus on conceptually cleaner algorithms and leave potential improvements in time and space complexity for future work.

Observe that for each of the algorithms, the final computation of $F_{0}$ estimation depends on the sketch $\mathcal{S}$. Therefore, as long as for two streams $\mathbf{a}$ and $\hat{\mathbf{a}}$, if their corresponding sketches, say $\mathcal{S}$ and $\hat{\mathcal{S}}$ respectively, are equivalent, the three schemes presented above would return the same estimates. The recipe for a transformation of streaming algorithms to model counting algorithms is based on the following insight:

1. (1)

   Capture the relationship $\mathcal{P}(\mathcal{S},H,\mathbf{a}_{u})$ between the sketch $\mathcal{S}$, set of hash functions $H$, and set $\mathbf{a}_{u}$ at the end of stream. Recall that $\mathbf{a}_{u}$ is the set of all distinct elements of the stream $\mathbf{a}$.

2. (2)

   The formula $\varphi$ is viewed as symbolic representation of the unique set $\mathbf{a}_{u}$ represented by the stream $\mathbf{a}$ such that $\mathsf{Sol}(\varphi)=\mathbf{a}_{u}$.

3. (3)

   Given a formula $\varphi$ and set of hash functions $H$, design an algorithm to construct sketch $\mathcal{S}$ such that $\mathcal{P}(\mathcal{S},H,\mathsf{Sol}(\varphi))$ holds. And now, we can estimate $|\mathsf{Sol}(\varphi)|$ from $\mathcal{S}$.

In the rest of this section, we will apply the above recipe to the three types of $F_{0}$ estimation algorithms, and derive corresponding model counting algorithms. In particular, we show how applying the above recipe to the $\mathsf{Bucketing}$ algorithm leads us to reproduce the state of the art hashing-based model counting algorithm, $\mathsf{ApproxMC}$, proposed by Chakraborty et al (Chakraborty et al., 2016). Applying the above recipe to $\mathsf{Minimum}$ and $\mathsf{Estimation}$ allows us to obtain fundamentally different schemes. In particular, we observe while model counting algorithms based on $\mathsf{Bucketing}$ and $\mathsf{Minimum}$ provide FPRAS’s when $\varphi$ is DNF, such is not the case for the algorithm derived based on $\mathsf{Estimation}$.

The $\mathsf{Bucketing}$ algorithm chooses a set $H$ of pairwise independent hash functions and maintains a sketch $\mathcal{S}$ that we will describe. Here we use $\mathcal{H}_{\mathsf{Toeplitz}}$ as our choice of pairwise independent hash functions. The sketch $\mathcal{S}$ is an array where, each $\mathcal{S}[i]$ of the form $\langle c_{i},m_{i}\rangle$. We say that the relation $\mathcal{P}_{1}(\mathcal{S},H,\mathbf{a}_{u})$ holds if

1. (1)

   $|\mathbf{a}_{u}\cap\{x~{}|~{}H[i]_{m_{i}-1}(x)=0^{m_{i}-1}\}|\geq\frac{96}{\varepsilon^{2}}$

2. (2)

   $c_{i}=|\mathbf{a}_{u}\cap\{x~{}|~{}H[i]_{m_{i}}(x)=0^{m_{i}}\}|<\frac{96}{\varepsilon^{2}}$

The following lemma due to Bar-Yossef et al. (Bar-Yossef et al., [n. d.]) and Gibbons and Tirthapura (Gibbons and Tirthapura, 2001) captures the relationship among the sketch $\mathcal{S}$, the relation $\mathcal{P}_{1}$ and the number of distinct elements of a multiset.

To design an algorithm for model counting, based on the bucketing strategy, we turn to the subroutine introduced by Chakraborty, Meel, and Vardi: $\mathsf{BoundedSAT}$, whose properties are formalized as follows:

Equipped with Proposition 2, we now turn to designing an algorithm for model counting based on the Bucketing strategy. The algorithm follows in similar fashion to its streaming counterpart where $m_{i}$ is iteratively incremented until the number of solutions of the formula ($\varphi\wedge H[i]_{m_{i}}(x)=0^{m_{i}})$ is less than $\mathsf{Thresh}$. Interestingly, an approximate model counting algorithm, called $\mathsf{ApproxMC}$, based on bucketing strategy was discovered independently by Chakraborty et. al. (Chakraborty et al., 2013b) in 2013. We reproduce an adaptation $\mathsf{ApproxMC}$ in Algorithm 5 to showcase how $\mathsf{ApproxMC}$ can be viewed as transformation of the $\mathsf{Bucketing}$ algorithm. In the spirit of $\mathsf{Bucketing}$, $\mathsf{ApproxMC}$ seeks to construct a sketch $\mathcal{S}$ of size $t\in\mathcal{O}(\log(1/\delta))$. To this end, for every iteration of the loop, we continue to increment the value of the loop until the conditions specified by the relation $\mathcal{P}_{1}(\mathcal{S},H,\mathsf{Sol}(\varphi))$ are met. For every iteration $i$, the estimate of the model count is $c_{i}\times 2^{m_{i}}$. Finally, the estimate of the model count is simply the median of the estimation of all the iterations. Since in the context of model counting, we are concerned with time complexity, wherein both $\mathcal{H}_{\mathsf{Toeplitz}}$ and $\mathcal{H}_{\mathsf{xor}}$ lead to same time complexity. Furthermore, Chakraborty et al. (Chakraborty et al., 2013a) observed no difference in empirical runtime behavior due to $\mathcal{H}_{\mathsf{Toeplitz}}$ and $\mathcal{H}_{\mathsf{xor}}$.

The following theorem establishes the correctness of $\mathsf{ApproxMC}$, and the proof follows from Lemma 1 and Proposition 2.

For a given multiset $\mathbf{a}$ ( eg: a data stream or solutions to a model), we now specify the property $\mathcal{P}_{2}(\mathcal{S},H,\mathbf{a}_{u})$. The sketch $\mathcal{S}$ is an array of sets indexed by members of $H$ that holds lexicographically $p$ minimum elements of $H[i](\mathbf{a}_{u})$ where $p$ is $\min(\frac{96}{\varepsilon^{2}},|\mathbf{a}_{u}|)$. $\mathcal{P}_{2}$ is the property that specifies this relationship. More formally, the relationship $\mathcal{P}_{2}$ holds, if the following conditions are met.

1. (1)

   $\forall i,|\mathcal{S}[i]|=\min(\frac{96}{\varepsilon^{2}},|\mathbf{a}_{u}|)$

2. (2)

   $\forall i,\forall y\notin\mathcal{S}[i],\forall y^{\prime}\in\mathcal{S}[i]\text{ it holds that }H[i](y^{\prime})\preceq H[i](y)$

The following lemma due to Bar-Yossef et al. (Bar-Yossef et al., [n. d.]) establishes the relationship between the property $\mathcal{P}_{2}$ and the number of distinct elements of a multiset. Let $\max(S_{i})$ denote the largest element of the set $S_{i}$.

Therefore, we can transform the $\mathsf{Minimum}$ algorithm for $F_{0}$ estimation to that of model counting given access to a subroutine that can compute $\mathcal{S}$ such that $\mathcal{P}_{2}(\mathcal{S},H,\mathsf{Sol}(\varphi))$ holds true. The following proposition establishes the existence and complexity of such a subroutine, called $\mathsf{FindMin}$:

Equipped with Proposition 5, we are now ready to present the algorithm, called $\mathsf{ApproxModelCountMin}$, for model counting. Since the complexity of $\mathsf{FindMin}$ is PTIME when $\varphi$ is in DNF, we have $\mathsf{ApproxModelCountMin}$ as a FPRAS for DNF formulas.

We now adapt the $\mathsf{Estimation}$ algorithm to model counting. For a given stream $\mathbf{a}$ and chosen hash functions $H$, the sketch $\mathcal{S}$ corresponding to the estimation-based algorithm satisfies the following relation $\mathcal{P}_{3}(\mathcal{S},H,\mathbf{a}_{u})$:

where the procedure $\mathsf{TrailZero}(z)$ is the length of the longest all-zero suffix of $z$. Bar-Yossef et al. (Bar-Yossef et al., [n. d.]) show the following relationship between the property $\mathcal{P}_{3}$ and $F_{0}$.