Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls

1 Introduction

Probabilistic inference is increasingly being used to reason about large uncertain data sets arising from diverse applications including medical diagnostics, weather modeling, computer vision and the like [Bacchus et al., 2003; Domshlak and Hoffmann, 2007; Sang et al., 2004; Xue et al., 2012]. Given a probabilistic model describing conditional dependencies between variables in a system, the problem of probabilistic inference requires us to determine the probability of an event of interest, given observed evidence. This problem has been the subject of intense investigations by both theoreticians and practitioners for more than three decades (see [Koller and Friedman, 2009] for a nice survey).

Exact probabilistic inference is intractable due to the curse of dimensionality [Cooper, 1990; Roth, 1996]. As a result, Moshe Y. Vardi Rice University researchers have studied approximate techniques to solve real-world instances of this problem. Techniques based on Markov Chain Monte Carlo (MCMC) methods [Brooks et al., 2011], variational approximations [Wainwright and Jordan, 2008], interval propagation [Tessem, 1992] and randomized branching choices in combinatorial reasoning algorithms [Gogate and Dechter, 2007] scale to large problem instances; however they fail to provide rigorous approximation guarantees in practice [Ermon et al., 2014; Kitchen and Kuehlmann, 2007].

⇤The author list has been sorted alphabetically by last name; this should not be used to determine the extent of authors' contributions.

A promising alternative approach to probabilistic inference is to reduce the problem to discrete integration or constrained counting, in which we count the models of a given set of constraints [Roth, 1996; Chavira and Darwiche, 2008]. While constrained counting is known to be computationally hard, recent advances in hashing-based techniques for approximate counting have revived a lot of interest in this approach. The use of universal hash functions in counting problems was first studied in [Sipser, 1983; Stockmeyer, 1983]. However, the resulting algorithms do not scale well in practice [Meel, 2014]. This leaves open the question of whether it is possible to design algorithms that simultaneously scale to large problem instances and provide strong theoretical guarantees for approximate counting. An important step towards resolving this question was taken in [Chakraborty et al., 2013b], wherein a scalable approximate counter with rigorous approximation guarantees, named ApproxMC, was reported. In subsequent work [Ermon et al., 2013a; Chakraborty et al., 2014a; Belle et al., 2015], this approach has been extended to finitedomain discrete integration, with applications to probabilistic inference.

Given the promise of hashing-based counting techniques in bridging the gap between scalability and providing rigorous guarantees for probabilistic inference, there have been several recent efforts to design efficient universal hash functions [Ivrii et al., 2015; Chakraborty et al., 2016a]. While these efforts certainly help push the scalability frontier of hashing-based techniques for probabilistic inference, the structure of the underlying algorithms has so far escaped critical examination. For example, all recent approaches to probabilistic inference via hashing-based counting use a linear search to identify the right values of parameters for the hash functions. As a result, the number of calls to the NP oracle (SAT solver in practice) increases linearly in the number of variables, n, in the input constraint. Since SAT solver calls are by far the computationally most expensive steps in these algorithms [Meel et al., 2016], this motivates us to ask: Can we design a hashing-based approximate counting algorithm that requires sub-linear (in n) calls to the SAT solver, while providing strong theoretical guarantees?

The primary contribution of this paper is a positive answer to the above question. We present a new hashing-based approximate counting algorithm, called ApproxMC2, for CNF formulas, that reduces the number of SAT solver calls from linear in n to logarithmic in n. Our algorithm provides SPAC, strongly probably approximately correct, guarantees; i.e., it computes a model count within a prescribed tolerance " of the exact count, and with a prescribed confidence of at least 1 - δ, while also ensuring that the expected value of the returned count matches the exact model count. We also show that for DNF formulas, ApproxMC2 gives a fully polynomial randomized approximation scheme (FPRAS), which differs fundamentally from earlier work [Karp et al., 1989].

Since the design of recent probabilistic inference algorithms via hashing-based approximate counting can be broadly viewed as adaptations of ApproxMC [Chakraborty et al., 2013b], we focus on ApproxMC as a paradigmatic representative, and show how ApproxMC2 improves upon it. Extensive experiments demonstrate that ApproxMC2 outperforms ApproxMC by 1-2 orders of magnitude in running time, when using the same family of hash functions. We also discuss how the framework and analysis of ApproxMC2 can be lifted to other hashing-based probabilistic inference algorithms [Chakraborty et al., 2014a; Belle et al., 2015]. Significantly, the algorithmic improvements of ApproxMC2 are orthogonal to recent advances in the design of hash functions [Ivrii et al., 2015], permitting the possibility of combining ApproxMC2-style algorithms with efficient hash functions to boost the performance of hashing-based probabilistic inference even further.

The remainder of the paper is organized as follows. We describe notation and preliminaries in Section 2. We discuss related work in Section 3. In Section 4, we present ApproxMC2 and its analysis. We discuss our experimental methodology and present experimental results in Section 5. Finally, we conclude in Section 6.

2 Notation and Preliminaries

Let F be a Boolean formula in conjunctive normal form (CNF), and let Vars(F) be the set of variables appearing in F. The set Vars(F) is also called the support of F. An assignment σ of truth values to the variables in Vars(F) is called a satisfying assignment or witness of F if it makes F evaluate to true. We denote the set of all witnesses of F by RF . Given a set of variables S ✓ Vars(F), we use RF#S to denote the projection of RF on S. Furthermore, given a function h : ¶0↪ 1♦♣Vars(F)♣ ! ¶0↪ 1♦m and an ↵ 2 ¶0↪ 1♦m, we use RhF↪h↪↵i#S to denote the projection on S of the witnesses of F that are mapped to ↵ by h, i.e. R(F^(h(Y )=↵))#S, where Y is a vector of support variables of F.

We write Pr [X : P] to denote the probability of outcome X when sampling from a probability space P. For brevity, we omit P when it is clear from the context. The expected value of X is denoted E [X] and its variance is denoted V [X].

The constrained counting problem is to compute ♣RF#S♣ for a given CNF formula F and sampling set S ✓ Vars(F). A probably approximately correct (or PAC) counter is a probabilistic algorithm ApproxCount(·↪ ·↪ ·↪ ·) that takes as inputs a formula F, a sampling set S, a tolerance " > 0, and a confidence 1 - δ 2 (0↪ 1], and returns a count c such that Prh♣RF#S♣◁(1+")  c  (1+")♣RF#S♣i ≥ 1-δ. The probabilistic guaranteee provided by a PAC counter is also called an ("↪ δ) guarantee, for obvious reasons. A PAC counter that additionally ensures that the expected value of the returned count equals ♣RF#S♣ is called strongly probably approximately correct (or SPAC). Intuitively, SPAC is a more useful notion of approximation than PAC in the context of counting, since the expectation of the returned count equals ♣RF#S♣ for a SPAC counter.

For positive integers n and m, a special family of 2universal hash functions mapping ¶0↪ 1♦n to ¶0↪ 1♦m, called Hxor(n↪m), plays a crucial role in our work. Let y[i] denote the ith component of a vector y. The family Hxor(n↪m) can then be defined as ¶h ♣ h(y)[i] = ai↪0 ⊕ (Lnk=1 ai↪k · y[k])↪ ai↪k 2 ¶0↪ 1♦↪ 1  i  m↪ 0  k  n♦, where ⊕ denotes "xor" and · denotes "and". By choosing values of ai↪k randomly and independently, we can effectively choose a random hash function from Hxor(n↪m). It was shown in [Gomes et al., 2007b] that Hxor(n↪m) is 3-universal (and hence 2-universal too). We use h U - Hxor(n↪m) to denote the probability space obtained by choosing a function h uniformly at random from Hxor(n↪m). The property of 2-universality guarantees that for all ↵1↪ ↵2 2 ¶0↪ 1♦m and for all distinct y1↪ y2 2 ¶0↪ 1♦n , Pr hV2i=1 h(yi) = ↵i : h U -Hxor(n↪m)i = 2-2m. Note that ApproxMC [Chakraborty et al., 2013b] also uses the same family of hash functions.

3 RelatedWork

The deep connection between probabilistic inference and propositional model counting was established in the seminal work of [Cooper, 1990; Roth, 1996]. Subsequently, researchers have proposed various encodings to solve inferencing problems using model counting [Sang et al., 2004; Chavira and Darwiche, 2008; Chakraborty et al., 2014a; Belle et al., 2015; Chakraborty et al., 2015b]. What distinguishes this line of work from other inferencing techniques, like those based on Markov Chain Monte Carlo methods [Jerrum and Sinclair, 1996] or variational approximation techniques [Wainwright and Jordan, 2008], is that strong guarantees can be offered while scaling to large problem instances. This has been made possible largely due to significant advances in model counting technology.

Complexity theoretic studies of propositional model counting were initiated by Valiant, who showed that the problem is #P-complete [Valiant, 1979]. Despite advances in exact model counting over the years [Sang et al., 2004; Thurley, 2006], the inherent complexity of the problem poses significant hurdles to scaling exact counting to large problem instances. The study of approximate model counting has therefore been an important topic of research for several decades. Approximate counting was shown to lie in the third level of the polynomial hierarchy in [Stockmeyer, 1983]. For DNF formulas, Karp, Luby and Madras gave a fully polynomial randomized approximation scheme for counting models [Karp et al., 1989]. For the general case, one can build on [Stockmeyer, 1983] and design a hashing-based probably approximately correct counting algorithm that makes polynomially many calls to an NP oracle [Goldreich, 1999]. Unfortunately, this does not lend itself to a scalable implementation because every invocation of the NP oracle (a SAT solver in practice) must reason about a formula with significantly large, viz. O(n◁"), support.

In [Chakraborty et al., 2013b], a new hashing-based strongly probably approximately correct counting algorithm, called ApproxMC, was shown to scale to formulas with hundreds of thousands of variables, while providing rigorous PAC-style ("↪ δ) guarantees. The core idea of ApproxMC is to use 2-universal hash functions to randomly partition the solution space of the original formula into "small" enough cells. The sizes of sufficiently many randomly chosen cells are then determined using calls to a specialized SAT solver (CryptoMiniSAT [Soos et al., 2009]), and a scaled median of these sizes is used to estimate the desired model count. Finding the right parameters for the hash functions is crucial to the success of this technique. ApproxMC uses a linear search for this purpose, where each search step invokes the specialized SAT solver, viz. CryptoMiniSAT, O(1◁"2 ) times. Overall, ApproxMC makes a total of O( n log(1◁δ) "2 ) calls to CryptoMiniSAT. Significantly, and unlike the algorithm in [Goldreich, 1999], each call of CryptoMiniSAT reasons about a formula with only n variables.

The works of [Ermon et al., 2013b; Chakraborty et al., 2014a; 2015a; Belle et al., 2015] have subsequently extended the ApproxMC approach to finite domain discrete integration. Furthermore, approaches based on ApproxMC form the core of various sampling algorithms proposed recently [Ermon et al., 2013a; Chakraborty et al., 2014b; 2014a; 2015a]. Therefore, any improvement in the core algorithmic structure of ApproxMC can potentially benefit several other algorithms.

Prior work on improving the scalability of hashing-based approximate counting algorithms has largely focused on improving the efficiency of 2-universal linear (xor-based) hash functions. It is well-known that long xor-based constraints make SAT solving significantly hard in practice [Gomes et al., 2007a]. Researchers have therefore investigated theoretical and practical aspects of using short xors [Gomes et al., 2007a; Chakraborty et al., 2014b; Ermon et al., 2014; Zhao et al., 2016].

Recently, Ermon et al. [Ermon et al., 2014] and Zhao et al. [Zhao et al., 2016] have shown how short xor constraints (even logarithmic in the number of variables) can be used for approximate counting with certain theoretical guarantees. The resulting algorithms, however, do not provide PAC-style ("↪ δ) guarantees. In other work with ("↪ δ)

Algorithm 1 ApproxMC2(F↪ S↪ "↪ δ)

• 1: thresh 1+9▷84 ⇣1+ " 1+" ⌘ (1 + 1" )2 ; 2: Y BSAT(F↪ thresh↪ S);
• 3: if (♣Y ♣ < thresh) then return ♣Y ♣;
• 5: nCells 2; C emptyList; iter 0;
• 4: t d17 log2(3◁δ)e;
• 6: repeat
• 7: iter iter + 1;
• 8: (nCells↪ nSols) ApproxMC2Core(F↪ S↪ thresh↪ nCells);
• 9: if (nCells 6= ?) then AddToList(C↪ nSols ⇥ nCells);
• 10: until (iter < t);
• 11: finalEstimate FindMedian(C);
• 12: return finalEstimate

guarantees, techniques for identifying small independent supports have been developed [Ivrii et al., 2015], and word-level hash functions have been used to count in the theory of bitvectors [Chakraborty et al., 2016a]. A common aspect of all of these approaches is that a linear search is used to find the right parameters of the hash functions, where each search step involves multiple SAT solver calls. We target this weak link in this paper, and drastically cut down the number of steps required to identify the right parameters of hash functions. This, in turn, reduces the SAT solver calls, yielding a scalable counting algorithm.

4 FromLinear to Logarithmic SAT Calls

We now present ApproxMC2, a hashing-based approximate counting algorithm, that is motivated by ApproxMC, but also differs from it in crucial ways.

4.1 The Algorithm

Algorithm 1 shows the pseudocode for ApproxMC2. It takes as inputs a formula F, a sampling set S, a tolerance " (> 0), and a confidence 1 - δ 2 (0↪ 1]. It returns an estimate of ♣RF#S♣ within tolerance ", with confidence at least 1 - δ. Note that although ApproxMC2 draws on several ideas from ApproxMC, the original algorithm in [Chakraborty et al., 2013b] computed an estimate of ♣RF ♣ (and not of ♣RF#S♣). Nevertheless, the idea of using sampling sets, as described in [Chakraborty et al., 2014b], can be trivially extended to ApproxMC. Therefore, whenever we refer to ApproxMC in this paper, we mean the algorithm in [Chakraborty et al., 2013b] extended in the above manner.

There are several high-level similarities between ApproxMC2 and ApproxMC. Both algorithms start by checking if ♣RF#S♣ is smaller than a suitable threshold (called pivot in ApproxMC and thresh in ApproxMC2). This check is done using subroutine BSAT, that takes as inputs a formula F, a threshold thresh, and a sampling set S, and returns a subset Y of RF#S, such that ♣Y ♣ = min(thresh↪ ♣RF#S♣). The thresholds used in invocations of BSAT lie in O(1◁"2 ) in both ApproxMC and ApproxMC2, although the exact values used are different. If ♣Y ♣ is found to be less than thresh, both algorithms return ♣Y ♣ for the size of ♣RF#S♣. Otherwise, a core subroutine, called ApproxMCCore in ApproxMC and ApproxMC2Core in ApproxMC2, is invoked. This subroutine tries to randomly partition RF#S into "small" cells using hash functions from Hxor(♣S♣↪m), for suitable values of m. There is a small probability that this subroutine fails and returns (?↪?). Otherwise, it returns the number of cells, nCells, into which RF#S is partitioned, and the count of solutions, nSols, in a randomly chosen small cell. The value of ♣RF#S♣ is then estimated as nCells ⇥ nSols. In order to achieve the desired confidence of (1 - δ), both ApproxMC2 and ApproxMC invoke their core subroutine repeatedly, collecting the resulting estimates in a list C. The number of such invocations lies in O(log(1◁δ)) in both cases. Finally, both algorithms compute the median of the estimates in C to obtain the desired estimate of ♣RF#S♣.

Despite these high-level similarities, there are key differences in the ways ApproxMC and ApproxMC2 work. These differences stem from: (i) the use of dependent hash functions when searching for the "right" way of partitioning RF#S within an invocation of ApproxMC2Core, and (ii) the lack of independence between successive invocations of ApproxMC2Core. We discuss these differences in detail below.

Subroutine ApproxMC2Core lies at the heart of ApproxMC2. Functionally, ApproxMC2Core serves the same purpose as ApproxMCCore; however, it works differently. To understand this difference, we briefly review the working of ApproxMCCore. Given a formula F and a sampling set S, ApproxMCCore finds a triple (m↪ hm↪ ↵m), where m is an integer in ¶1↪ ▷ ▷ ▷ ♣S♣ - 1♦, hm is a hash function chosen randomly from Hxor(♣S♣↪m), and ↵m is a vector chosen randomly from ¶0↪ 1♦m, such that ♣RhF↪hm↪↵mi#S♣ < thresh and ♣RhF↪hm-1↪↵m-1i#S♣ ≥ thresh. In order to find such a triple, ApproxMCCore uses a linear search: it starts from m = 1, chooses hm and ↵m randomly and independently from Hxor(♣S♣↪m) and ¶0↪ 1♦m respectively, and checks if ♣RhF↪hm↪↵mi#S♣ ≥ thresh. If so, the partitioning is considered too coarse, hm and ↵m are discarded, and the process repeated with the next value of m; otherwise, the search stops. Let m⇤ ↪ hm⇤ and ↵m⇤ denote the values of m, hm and ↵m, respectively, when the search stops. Then ApproxMCCore returns ♣RhF↪hm⇤ ↪↵m⇤i#S♣ ⇥2m⇤ as the estimate of ♣RF#S♣. If the search fails to find m, hm and ↵m with the desired properties, we say that ApproxMCCore fails.

Every iteration of the linear search above invokes BSAT once to check if ♣RhF↪hm↪↵mi#S♣ ≥ thresh. A straightforward implementation of BSAT makes up to thresh calls to a SAT solver to answer this question. Therefore, an invocation of ApproxMCCore makes O(thresh▷♣S♣) SAT solver calls. A key contribution of this paper is a new approach for choosing hash functions that allows ApproxMC2Core to make at most O(thresh▷ log2 ♣S♣) calls to a SAT solver. Significantly, the sizes of formulas fed to the solver remain the same as those used in ApproxMCCore; hence, the reduction in number of calls comes without adding complexity to the individual calls.

A salient feature of ApproxMCCore is that it randomly and independently chooses (hm↪ ↵m) pairs for different values of m, as it searches for the right partitioning of RF#S. In contrast, in ApproxMC2Core, we randomly choose one function h from Hxor(♣S♣↪ ♣S♣ - 1), and one vector ↵ from

Algorithm 2 ApproxMC2Core(F↪ S↪ thresh↪ prevNCells)

• 1: Choose h at random from Hxor(♣S♣↪ ♣S♣ - 1);
• 3: Y BSAT(F ^ h(S) = ↵↪ thresh↪ S);
• 2: Choose ↵ at random from ¶0↪ 1♦♣S♣-1 ;
• 4: if (♣Y ♣ ≥ thresh) then return (?↪?);
• 5: mPrev log2 prevNCells;
• 6: m LogSATSearch(F↪ S↪ h↪ ↵↪ thresh↪mPrev);
• 7: nSols ♣BSAT(F ^ h(m) (S) = ↵(m) ↪ thresh↪ S)♣;
• 8: return (2m↪ nSols);

¶0↪ 1♦♣S♣-1 . Thereafter, we use "prefix-slices" of h and ↵ to obtain hm and ↵m for all other values of m. Formally, for every m 2 ¶1↪ ▷ ▷ ▷ ♣S♣ - 1♦, the mth prefix-slice of h, denoted h(m) , is a map from ¶0↪ 1♦♣S♣ to ¶0↪ 1♦m, such that h(m) (y)[i] = h(y)[i], for all y 2 ¶0↪ 1♦♣S♣ and for all i 2 ¶1↪ ▷ ▷ ▷m♦. Similarly, the mth prefix-slice of ↵, denoted ↵(m) , is an element of ¶0↪ 1♦m such that ↵(m) [i] = ↵[i] for all i 2 ¶1↪ ▷ ▷ ▷m♦. Once h and ↵ are chosen randomly, ApproxMC2Core uses h(m) and ↵(m) as choices of hm and ↵m, respectively. The randomness in the choices of h and ↵ induces randomness in the choices of hm and ↵m. However, the (hm↪ ↵m) pairs chosen for different values of m are no longer independent. Specifically, hj(y)[i] = hk(y)[i] and ↵j[i] = ↵k[i] for 1  j < k < ♣S♣ and for all i 2 ¶1↪ ▷ ▷ ▷ j♦. This lack of independence is a fundamental departure from ApproxMCCore.

Algorithm 2 shows the pseudo-code for ApproxMC2Core. After choosing h and ↵ randomly, ApproxMC2Core checks if ♣RhF↪h↪↵i#S♣ < thresh. If not, ApproxMC2Core fails and returns (?↪?). Otherwise, it invokes sub-routine LogSATSearch to find a value of m (and hence, of h(m) and ↵(m) ) such that ♣RhF↪h(m) ↪↵(m) i#S♣ < thresh and ♣RhF↪h(m-1) ↪↵(m-1) i#S♣ ≥ thresh. This ensures that nSols computed in line 7 is ♣RhF↪h(m) ↪↵(m) i#S♣. Finally, ApproxMC2Core returns (2m↪ nSols), where 2m gives the number of cells into which RF#S is partitioned by h(m) .

An easy consequence of the definition of prefix-slices is that for all m 2 ¶1↪ ▷ ▷ ▷ ♣S♣ -1♦, we have RhF↪h(m) ↪↵(m) i#S ✓ RhF↪h(m-1) ↪↵(m-1) i#S. This linear ordering is exploited by sub-routine LogSATSearch (see Algorithm 3), which uses a galloping search to zoom down to the right value of m, h(m) and ↵(m) . LogSATSearch uses an array, BigCell, to remember values of m for which the cell ↵(m) obtained after partitioning RF#S with h(m) is large, i.e. ♣RhF↪h(m) ↪↵(m) i#S♣ ≥ thresh. As boundary conditions, we set BigCell[0] to 1 and BigCell[♣S♣ - 1] to 0. These are justified because (i) if RF#S is partitioned into 20 (i.e. 1) cell, line 3 of Algorithm 1 ensures that the size of the cell (i.e. ♣RF#S♣) is at least thresh, and (ii) line 4 of Algorithm 2 ensures that ♣RhF↪h♣S♣-1 ↪↵♣S♣-1 i#S♣ < thresh. For every other i, BigCell[i] is initialized to ? (unknown value). Subsequently, we set BigCell[i] to 1 (0) whenever we find that ♣RhF↪h(i) ↪↵(i) i#S♣ is at least as large as (smaller than) thresh.

In the context of probabilistic hashing-based counting algorithms like ApproxMC, it has been observed [Meel, 2014]

Algorithm 3 LogSATSearch(F↪ S↪ h↪ ↵↪ thresh↪ mPrev)

1: loIndex 0; hiIndex ♣S♣ -1; m mPrev; 2: BigCell[0] 1; BigCell[♣S♣ -1] 0; 3: BigCell[i] ? for all i other than 0 and ♣S♣ -1; 4: while true do 5: Y BSAT(F ^ (h(m) (S) = ↵(m) )↪ thresh↪ S); 6: if (♣Y ♣ ≥ thresh) then 7: if (BigCell[m + 1] = 0) then return m + 1; 8: BigCell[i] 1 for all i 2 ¶1↪ ▷ ▷ ▷m♦; 9: loIndex m; 10: if (♣m-mPrev♣ < 3) thenm m+1; 11: else if (2▷m< ♣S♣) thenm 2▷m; 12: else m (hiIndex +m)◁2; 13: else 14: if (BigCell[m - 1] = 1) then return m; 15: BigCell[i] 0 for all i 2 ¶m↪ ▷ ▷ ▷ ♣S♣♦; 16: hiIndex m; 17: if (♣m-mPrev♣ < 3) thenm m-1; 18: else m (m+ loIndex)◁2;

that the "right" values of m, hm and ↵m for partitioning RF#S are often such that m is closer to 0 than to ♣S♣. In addition, repeated invocations of a hashing-based probabilistic counting algorithm with the same input formula F often terminate with similar values of m. To optimize LogSATSearch using these observations, we provide mPrev, the value of m found in the last invocation of ApproxMC2Core, as an input to LogSATSearch. This is then used in LogSATSearch to linearly search a small neighborhood of mPrev, viz. when ♣mmPrev♣ < 3, before embarking on a galloping search. Specifically, if LogSATSearch finds that ♣RhF↪h(m) ↪↵(m) i#S♣ ≥ thresh after the linear search, it keeps doubling the value of m until either ♣RhF↪h(m) ↪↵(m) i#S♣ becomes less than thresh, or m overshoots ♣S♣. Subsequently, binary search is done by iteratively bisecting the interval between loIndex and hiIndex. This ensures that the search requires O(log2m⇤ ) calls (instead of O(log2 ♣S♣) calls) to BSAT, where m⇤ (usually ⌧ ♣S♣) is the value of m when the search stops. Note also that a galloping search inspects much smaller values of m compared to a naive binary search, if m⇤ ⌧ ♣S♣. Therefore, the formulas fed to the SAT solver have fewer xor clauses (or number of components of h(m) ) conjoined with F than if a naive binary search was used. This plays an important role in improving the performance of ApproxMC2.

In order to provide the right value of mPrev to LogSATSearch, ApproxMC2 passes the value of nCells returned by one invocation of ApproxMC2Core to the next invocation (line 8 of Algorithm 1), and ApproxMC2Core passes on the relevant information to LogSATSearch (lines 5-6 of Algorithm 2). Thus, successive invocations of ApproxMC2Core in ApproxMC2 are no longer independent of each other. Note that the independence of randomly chosen (hm↪ ↵m) pairs for different values of m, and the independence of successive invocations of ApproxMCCore, are features of ApproxMC that are exploited in its analysis [Chakraborty et al., 2013b]. Since these independence no longer hold in ApproxMC2, we must analyze ApproxMC2 afresh.

4.2 Analysis

For lack of space, we state only some key results and provide sketches of proofs here. The complete proofs are deferred to a detailed technical report [Chakraborty et al., 2016b].

Lemma 1. For 1  i < ♣S♣, let θi = RF#S◁2i . For every β > 0 and 0 < " < 1, we have the following:

Proof sketch. For every y 2 ¶0↪ 1♦♣S♣ and for every ↵ 2 ¶0↪ 1♦i , define an indicator variable γy↪↵↪i which is 1 iff h(i) (y) = ↵. Let Γ↵↪i = Py2RF#S (γy↪↵↪i), θ↵↪i = E [Γ↵↪i] and σ2↵↪i = V [Γ↵↪i]. Clearly, Γ↵↪i = ♣RhF↪h(i) ↪↵i#S♣ and θ↵↪i = 2-i ♣RF#S♣. Note that θ↵↪i is independent of ↵ and equals θi, as defined in the statement of the Lemma. From the pairwise independence of h(i) (y) (which, effectively, is a randomly chosen function from Hxor(♣S♣↪ i)), we also have σ2↵↪i  θ↵↪i = θi. Statements 1 and 2 of the lemma then follow from Chebhyshev inequality and Paley-Zygmund inequality, respectively.

Let B denote the event that ApproxMC2Core either returns (?↪?) or returns a pair (2m↪ nSols) such that 2m ⇥ nSols does not lie in the interval h ♣RF#S♣ 1+" ↪ ♣RF#S♣(1+ ")♣i. We wish to bound Pr [B] from above. Towards this end, let Ti denote the event (♣RhF↪h(i) ↪↵(i) i#S♣ < thresh), and let Li and Ui denote the events ⇣♣RhF↪h(i) ↪↵(i) i#S♣ < ♣RF#S♣ (1+")2i ⌘ and ⇣♣RhF↪h(i) ↪↵(i) i#S♣ > ♣RF#S♣ 2i (1+ " 1+" )⌘, respectively. Furthermore, let m⇤ denote the integer blog2 ♣RF#S♣ - log2 ⇣4▷92 (1 + 1" )2⌘c.

Lemma 2. The following bounds hold:

The proofs follow from the definitions of m⇤ , thresh, θi, and from applications of Lemma 1 with appropriate values of β.

Proof sketch. For any event E, let E denote its complement. For notational convenience, we use T0 and U♣S♣ to denote the empty (or impossible) event, and T♣S♣ and L♣S♣ to denote the universal (or certain) event. It then follows from the definition of B that Pr [B]  Pr hSi2¶1↪▷▷▷♣S♣♦ (Ti-1 \ Ti \ (Li [ Ui))i.

We now wish to simplify the upper bound of Pr [B] obtained above. In order to do this, we use three observations, labeled O1, O2 and O3 below, which follow from the definitions of m⇤ , thresh and θi, and from the linear ordering of RhF↪h(m) ↪↵(m) i#S .

Using O1, O2 and O3, we get Pr[B]  Pr[Tm⇤-3] + Pr[Lm⇤-2]+Pr[Lm⇤-1]+Pr[Lm⇤ [Um⇤ ]. Using the bounds from Lemma 2, we finally obtain Pr [B]  0▷36.

• 1+" ), we have Ti \ Ui = ;.

Note that Lemma 3 holds regardless of the order in which the search in LogSATSearch proceeds. Our main theorem now follows from Lemma 3 and from the count t of invocations of ApproxMC2Core in ApproxMC2 (see lines 4-10 of Algorithm 1).

Theorem 4. Suppose ApproxMC2(F↪ S↪ "↪ δ) returns c after making k calls to a SAT solver. Then Pr[♣RF#S♣◁(1 + ")  c  (1 + ")♣RF#S♣] ≥ 1 - δ, and k 2 O( log(♣S♣) log(1◁δ) "2 ). Furthermore, E[c] = ♣RF#S♣. Hence ApproxMC2 is a SPAC counter.

Note that the number of SAT solver calls in ApproxMC [Chakraborty et al., 2013b] lies in O( ♣S♣ log(1◁δ) "2 ), which is exponentially worse than the number of calls in ApproxMC2, for the same " and δ. Furthermore, if the formula F fed as input to ApproxMC2 is in DNF, the subroutine BSAT can be implemented in PTIME, since satisfiability checking of DNF + XOR is in PTIME. This gives us the following result.

Theorem 5. ApproxMC2 is a fully polynomial randomized approximation scheme (FPRAS) for #DNF.

Note that this is fundamentally different from FPRAS for #DNF described in earlier work, viz. [Karp et al., 1989].

4.3 Generalizing beyond ApproxMC

So far, we have shown how ApproxMC2 significantly reduces the number of SAT solver calls vis-a-vis ApproxMC, without sacrificing theoretical guarantees, by relaxing independence requirements. Since ApproxMC serves as a paradigmatic representative of several hashing-based counting and probabilistic inference algorithms, the key ideas of ApproxMC2 can be used to improve these other algorithms too. We discuss two such cases below.

PAWS [Ermon et al., 2013a] is a hashing-based sampling algorithm for high dimensional probability spaces. Similar to ApproxMC, the key idea of PAWS is to find the "right" number and set of constraints that divides the solution space into appropriately sized cells. To do this, PAWS iteratively adds independently chosen constraints, using a linear search. An analysis of the algorithm in [Ermon et al., 2013a] shows that this requires O(n logn) calls to an NP oracle, where n denotes the size of the support of the input constraint. Our approach based on dependent constraints can be used in PAWS to search out-of-order, and reduce the number of NP oracle calls from O(n logn) to O(logn), while retaining the same theoretical guarantees.

Building on ApproxMC, a weighted model counter called WeightMC was proposed in [Chakraborty et al., 2014a]. WeightMC has also been used in other work, viz. [Belle et al., 2015], for approximate probabilistic inference. The core procedure of WeightMC, called WeightMCCore, is a reworking of ApproxMCCore that replaces ♣RF#S♣ with the total weight of assignments in RF#S. It is easy to see that the same replacement can also be used to extend ApproxMC2Core, so that it serves as the core procedure for WeightMC.

5 Evaluation

To evaluate the runtime performance and quality of approximations computed by ApproxMC2, we implemented a prototype in C++ and conducted experiments on a wide variety of publicly available benchmarks. Specifically, we sought answers to the following questions: (a) How does runtime performance and number of SAT invocations of ApproxMC2 compare with that of ApproxMC ? (b) How far are the counts computed by ApproxMC2 from the exact counts?

Our benchmark suite consisted of problems arising from probabilistic inference in grid networks, synthetic gridstructured random interaction Ising models, plan recognition, DQMR networks, bit-blasted versions of SMTLIB benchmarks, ISCAS89 combinational circuits, and program synthesis examples. For lack of space, we discuss results for only a subset of these benchmarks here. The complete set of experimental results and a detailed analysis can be found in [Chakraborty et al., 2016b].

We used a high-performance cluster to conduct experiments in parallel. Each node of the cluster had a 12-core 2.83 GHz Intel Xeon processor, with 4GB of main memory, and each experiment was run on a single core. For all our experiments, we used " = 0▷8 and δ = 0▷2, unless stated otherwise. To further optimize the running time, we used improved estimates of the iteration count t required in ApproxMC2 by following an analysis similar to that in [Chakraborty et al., 2013a].

5.1 Results

Performance comparison: Table 1 presents the performance of ApproxMC2 vis-a-vis ApproxMC over a subset of our benchmarks. Column 1 of this table gives the benchmark name, while columns 2 and 3 list the number of variables and clauses, respectively. Columns 4 and 5 list the runtime (in seconds) of ApproxMC2 and ApproxMC respectively, while columns 6 and 7 list the number of SAT invocations for ApproxMC2 and ApproxMC respectively. We use "-" to denote timeout after 8 hours. Table 1 clearly demonstrates that ApproxMC2 outperforms ApproxMC by 1-2 orders of magnitude. Furthermore, ApproxMC2 is able to compute counts for benchmarks that are beyond the scope of ApproxMC. The runtime improvement of ApproxMC2 can be largely attributed to the reduced (by almost an order of magnitude) number of SAT solver calls vis-a-vis ApproxMC.

There are some large benchmarks in our suite for which both ApproxMC and ApproxMC2 timed out; hence, we did not include these in Table 1. Importantly, for a significant number of our experiments, whenever ApproxMC or ApproxMC2 timed out, it was because the algorithm could execute some, but not all required iterations of ApproxMCCore or ApproxMC2Core, respectively, within the specified time limit. In all such cases, we obtain a model count within the specified tolerance, but with reduced confidence. This suggests that it is possible to extend ApproxMC2 to obtain an anytime algorithm. This is left for future work.

Approximation quality: To measure the quality of approximation, we compared the approximate counts returned by ApproxMC2 with the counts computed by an exact model counter, viz. sharpSAT [Thurley, 2006]. Figure 1 shows the model counts computed by ApproxMC2, and the bounds obtained by scaling the exact counts with the tolerance factor (" = 0▷8) for a small subset of benchmarks. The yaxis represents model counts on log-scale while the x-axis represents benchmarks ordered in ascending order of model counts. We observe that for all the benchmarks, ApproxMC2 computed counts within the tolerance. Furthermore, for each instance, the observed tolerance ("obs) was calculated as max( AprxCount ♣RF#S♣ - 1↪ 1 - ♣RF#S♣ AprxCount ), where AprxCount is the estimate computed by ApproxMC2. We observe that the geometric mean of "obs across all benchmarks is 0▷021 - far better than the theoretical guarantee of 0▷8. In comparison, the geometric mean of the observed tolerance obtained from ApproxMC running on the same set of benchmarks is 0▷036.

6 Conclusion

The promise of scalability with rigorous guarantees has renewed interest in hashing-based counting techniques for probabilistic inference. In this paper, we presented a new approach to hashing-based counting and inferencing, that allows out-of-order-search with dependent hash functions, dramatically reducing the number of SAT solver calls from linear to logarithmic in the size of the support of interest. This is achieved while retaining strong theoretical guarantees and without increasing the complexity of each SAT solver call. Extensive experiments demonstrate the practical benefits of our approach vis-a-vis state-of-the art techniques. Combining our approach with more efficient hash functions promises to push the scalability horizon of approximate counting further.

Acknowledgements

The authors thank Jeffrey Dudek for several helpful discussions and comments on early draft of this paper. This work was supported in part by NSF grants IIS-1527668, CCF1139011, by NSF Expeditions in Computing project "ExCAPE: Expeditions in Computer Augmented Program Engineering", by BSF grant 9800096, by a grant from the Board of Research in Nuclear Sciences, India, Data Analysis and Visualization Cyberinfrastructure funded by NSF under grant OCI-0959097. Part of this work was done during a visit to the Israeli Institute for Advanced Studies.