From Weighted to Unweighted Model Counting

1 Introduction

Probabilistic reasoning on graphical models has seen an unwavering interest in recent years, with compelling applications from diverse domains like medical diagnostics, behavioral studies, natural language processing and the like [Getoor and Taskar, 2007]. Several computational techniques have therefore been developed to address problems that arise in reasoning about probabilistic graphical models [Koller and Friedman, 2009]. One such important problem is that of probabilistic inference, wherein we are given a graphical model describing conditional dependencies between variables of interest, and we are required to compute the conditional probability of an event, i.e. valuations of a subset of variables, given some evidence in the form of valuations of another

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

†The full version is available at http://www.cs.rice.edu/CS/ Verification/Projects/CUSP/

‡ This work was supported in part by NSF grants CNS 1049862, CCF-1139011, by NSF Expeditions in Computing project "ExCAPE: Expeditions in Computer Augmented Program Engineering", by BSF grant 9800096, by a gift from Intel, by a grant from the Board of Research in Nuclear Sciences, India, Data Analysis and Visualization Cyberinfrastructure funded by NSF under grant OCI-0959097.

Dror Fried, Kuldeep S. Meel, Moshe Y. Vardi

Department of Computer Science, Rice University

subset of variables. It is known [Cooper, 1990; Roth, 1996; Chavira and Darwiche, 2008] that there is a deep connection between probabilistic inference and computing the aggregate weight of all models (or satisfying assignments) of a weighted propositional formula. Owing to the spectacular and sustained improvements in the capabilities of modern tools for propositional satisfiability solving and model counting [Belov et al., 2014; Thurley, 2006], probabilistic inference via weighted model counting promises to be a strong alternative to other probabilistic inference techniques, such as variable elimination, belief propagation, and the like. This motivates investigating further the problem of computing aggregate weights of models of propositional formulas.

Given a propositional formula and a weight function that assigns a non-negative weight to every assignment of values to variables, weighted model counting (henceforth WMC) concerns summing weights of assignments that satisfy the formula. If every assignment has weight 1, the corresponding problem is often simply called model counting; for clarity of presentation, we use unweighted model counting (henceforth UMC) to denote this variant of the problem.

Both UMC and WMC have been extensively studied in theoretical and practical contexts. UMC for propositional formulas in both conjunctive normal form (CNF) and disjunctive normal form (DNF) were shown to be #P-complete in [Valiant, 1979]. Subsequently, #P-completeness of WMC for CNF formulas was stated in [Roth, 1996].

On the practical front, both UMC and WMC have applications in diverse areas even beyond probabilistic reasoning, viz. network reliability estimation, statistical physics, program synthesis and system verification [Roth, 1996; Sang et al., 2004; Domshlak and Hoffmann, 2007; Xue et al., 2012]. Several tools and algorithms for model counting, in both the weighted and unweighted settings, have therefore been proposed in the recent past [Bayardo and Schrag, 1997; Darwiche, 2004; Sang et al., 2005; Thurley, 2006].

Many applications, including probabilistic inference, of WMC arising from real-world can be expressed by a literalweighted representation, in which the weight of an assignment is the product of weights of its literals [Chavira and Darwiche, 2008]. We use this representation throughout this paper, and use literal-weighted WMC to denote the corresponding WMC problem. Note that literal-weighted WMC problems for both CNF and DNF formulas arise in real-life applications; e.g., DNF formulas are used in problems arising from probabilistic databases [Dalvi and Suciu, 2007], while CNF is the de-facto form of representation for probabilisticinference problems [Chavira and Darwiche, 2008].

Recent approaches to WMC have focused on adapting UMC techniques to work in the weighted setting [Sang et al., 2005; Choi and Darwiche, 2013; Chakraborty et al., 2014a]. Such adaption requires intimate understanding of the implementation details of the UMC techniques, and on-going maintenance, since some of these techniques evolve over time. In this paper, we flip this approach and present an efficient reduction of literal-weighted WMC to UMC. The reduction preserves the normal form of the input formula, i.e. it provides the UMC formula in the same normal form as the input WMC formula. Therefore, an important contribution of our reduction is to provide a WMC-to-UMC module that allows any UMC solver, viewed as a black box, to be converted to a WMC solver. This enables the automatic leveraging of progress in UMC solving to progress in WMC solving.

We have implemented our WMC-to-UMC module on top of state-of-the-art exact unweighted model counters to obtain exact weighted model counters for CNF formulas with literalweighted representation. Experiments on a suite of benchmarks indicate that the resulting counters scale to significantly larger problem instances than what can be handled by a state-of-the-art exact weighted model counter [Choi and Darwiche, 2013]. Our results suggest that we can leverage powerful techniques developed for SAT and related domains in recent years to handle probabilistic inference queries for graphical models encoded as WMC instances. Furthermore, we demonstrate that our techniques can be extended to more general representations where weights are associated with constraints instead of individual literals.

The remainder of the paper is organized as follows. We introduce notation and preliminaries in Section 2, and discuss related work in Section 3. We present our main technical contribution - a polynomial-time reduction from WMC to UMC - in Section 4. Ising our reduction, we have implemented a literal-weighted exact model counter module called WeightCount. In Section 5, we present results of our experiments using WeightCount on top of state-of-the-art UMC solvers, and compare them with SDD - a state-of-the-art exact weighted model counter. We then demonstrate, in Section 6, that our reduction can be extended to more general representation of associating weights with constraints. Finally, we discuss future work and conclude in Section 7.

2 Notation and Preliminaries

Let F be a Boolean formula and let X be the set of variables appearing in F . For a variable x ∈ X, we denote the assignment of x to true by x1 and the assignment of x to false by x0 . A satisfying assignment or a witness of F is an assignment of variables in X that makes F evaluate to true. We denote the set of all witnesses of F by RF . If σ is an assignment of variables in X and x ∈ X, we use σ(x) to denote the value assigned to x in σ. For notational convenience, whenever the formula F is clear from the context, we omit mentioning it.

As mentioned earlier, we focus on literal-weighted WMC, in which weights are assigned to literals, and the weight of an assignment is the product of weights of its literals. For a variable x of F and a weight function W(·), we use W (x1 ) and W (x0 ) to denote the weights of the positive and negative literals, respectively. Adopting terminology used in [Sang et al., 2005], we assume that every variable x either has an indifferent weight, i.e. W (x0 ) = W (x1 ) = 1, or a normal weight, i.e. W (x0 ) = 1 - W (x1 ), where 0 ≤ W (x1 ) ≤ 1. This assumption stands well, as many real-world applications, and in particular probabilistic inference, can be efficiently reduced to literal-weighted WMC where every variable has either indifferent or normal weight [Chavira and Darwiche, 2008]. For notational convenience, henceforth whenever we say "literalweighted WMC", we mean literal-weighted WMC with indifferent or normal weights of variables. Note that having a variable with a normal weight of W (x1 ) = 1 (resp. W (x1 ) = 0) makes the variable x redundant for WMC, since in this case only assignments σ with σ(x) = true (resp. σ(x) = false) can contribute to the total weight. Thus, we can assign true (resp. false) to x without changing the overall weight of models of the formula. This suggests that we can further assume 0 < W (x1 ) < 1 for every variable x with a normal weight.

To avoid notational clutter, we overload W(·) to denote the weight of a literal, assignment or formula, depending on the context. Given a set Y of assignments, we use W(Y ) to denote ∑σ∈Y W(σ). Given a formula F, we use W(F) to denote ∑σ∈RF W(σ). For example, the formula F = (x1 ↔ ¬x2) has two satisfying assignments: σ1 = (x1 : true, x2 : false), and σ2 = (x1 : false, x2 : true). Thus, we have W(σ1) = W (x11 ) · W (x02 ) and W(σ2) = W (x01 ) · W (x12 ). The weight of F, or W(F), is then W(σ1) +W(σ2).

For every variable xi with normal weight, we assume that W (x1i ), which is a positive fraction, is specified in binary using mi bits. Without loss of generality, the least significant bit in the binary representation of W (x1i ) is always taken to be 1. Thus, the rational decimal representation of W (x1i ) is ki/2mi , where ki is an odd integer in {1, . . . 2mi - 1}. It follows that W (x0i ) is (2mi - ki)/2mi . Let NF denote the set of indices of variables in X that have normal weights, and let ̂m = Σi∈NF mi. Let CF = ∏i∈NF 2-mi = 2-̂m. Note that W(σ) /CF is a natural number for every assignment σ; hence W(F) /CF is a natural number as well.

An instance of literal-weighted WMC can be defined by a pair (F,W(·)), where F is a Boolean formula, and W(·) is the weight function for literals. Given (F,W(·)), a weighted model counter returns W(F).

Our work uses a special class of Boolean formulas, called chain formulas, that are inductively defined as follows. Every literal (i.e., a variable or its complement) is a chain formula. In addition, if l is a literal and ϕ is a chain formula in which neither l nor ¬l appears, then (l ∨ ϕ) and (l ∧ ϕ) are also chain formulas. Note that chain formulas can be represented as l1 C1 (l2 C2 (· · · (ln-1 Cn-1 ln) · · · )), where the li's are literals and every Ci is either the connector "∨" or the connector "∧". It is easy to see from De Morgan's laws that if ϕ is a chain formula, then so is ¬ϕ.

3 RelatedWork

Theoretical investigations into the problem of model counting were initiated by Valiant, who first showed that UMC is #P-complete for both CNF and DNF formulas [Valiant, 1979]. Subsequently, Roth asserted that probabilistic inference is #P-complete, which by a known connection with WMC [Cooper, 1990; Chavira and Darwiche, 2008], implies that WMC is also #P-complete for both CNF and DNF formulas [Roth, 1996].

On the practical side, the earliest efforts at WMC such as CDP [Birnbaum and Lozinskii, 1999] were inspired from DPLL-style SAT solvers and consisted of incrementally counting the number of solutions after a partial solution was found. Subsequently, heuristics such as component caching, clause learning, no-good learning and the like improved upon the initial approach and ensuing counters such as Relsat [Bayardo and Schrag, 1997], Cachet [Sang et al., 2004], and sharpSAT [Thurley, 2006] have been shown to scale to larger formulas. These approaches were later manually adapted for WMC in Cachet [Sang et al., 2005].Again, alternative approaches based on BDDs and their variants [L¨obbing and Wegener, 1996; Xue et al., 2012] have also been proposed for UMC. Similar to SAT-based approaches, the resulting solvers have also been manually adapted for WMC, resulting in solvers like SDD [sdd, 2014].

In this paper, we adopt a different approach and propose to solve WMC by reducing it to UMC. Our key contribution lies in showing that this reduction is efficient and effective, thereby making it possible to solve weighted model counting problems using any unweighted model counter as a black-box. Our reduction makes use of chain formulas to encode each weighted variable. Interestingly, these formulas can be viewed as adaptations of switching circuits proposed by [Wilhelm and Bruck, 2008] in the context of stochastic switching networks. Chain formulas are also reminiscent of the log-encoding approach of encoding variables with bounded domains in the CSP literature [E´en and S¨orensson, 2006; Frisch et al., 2006; Gavanelli, 2007; Huang, 2008; Walsh, 2000]. Indeed, a chain formula encoding a variable with weight k/2m is logically equivalent to the constraint (X ≥ 2m - k), where X is an unsigned integer represented using m boolean variables, as described in [Gavanelli, 2007; Walsh, 2000]. The use of log-encoding for exact counting weighted models of Boolean formulas is novel, to the best of our knowledge.

4 FromLiteral-weightedWMC to UMC

In this section, we first show how chain formulas can be used to represent normal weights of variables. We then present two polynomial-time reductions from WMC to UMC using chain formulas. These constitute the key technical contributions of the paper. These reductions, though related, are motivated by the need to preserve different normal forms (CNF and DNF) of the input formula. Finally, we discuss the optimality of our reductions with respect to number of variables in the unweighted formula.

Representing Weights using Chain Formulas

The central idea of our reduction is the use of chain formulas to represent weights. Let m > 0 be a natural number, and k < 2m be a positive odd number. Let c1c2 · · · cm be the mbit binary representation of k, where cm is the least significant bit. We then construct a chain formula ϕk,m(·) on m variables a1, . . . am as follows. For every j in {1, . . .m-1}, let Cj be the connector "∨" if cj = 1, and the connector "∧" if cj = 0. Define

For example, consider k = 5 and m = 4. The binary representation of 5 using 4 bits is 0101. Therefore, ϕ5,4(a1, a2, a3, a4) = a1 ∧ (a2 ∨ (a3 ∧ a4)). We first show in Lemma 1 that ϕk,m(·) has exactly k satisfying assignments. Next, as a simple application of the distributive laws of Boolean algebra, Lemma 2 shows that every chain formula can be efficiently represented in both CNF and DNF. The proofs of these and other lemmas are given in the full version of the paper.

Lemma 1. Let m > 0 be a natural number, k < 2m , and ϕk,m as defined above. Then |ϕk,m| is linear in m and ϕk,m has exactly k satisfying assignments.

Recall from Section 2 that NF denotes the set of indices of normal-weighted variables in F . For i in NF , let W (x1i ) = ki/2mi , where ki is a positive odd number less than 2mi . Additionally, let {xi,1, . . . xi,mi } be a set of mi "fresh" variables (i.e. variables that were not used before) for each i in NF . We call the chain formula ϕki,mi (xi,1 · · · xi,mi ), the representative formula of xi. For notational clarity, we simply write ϕki,mi when the arguments of the representative formula are clear from the context.

Lemma 2. Every chain formula ψ on n variables is equivalent to a CNF (resp., DNF) formula ψCNF (resp., ψDNF ) having at most n clauses. In addition, |ψCNF | (resp., |ψDNF |) is in O(n2 ).

Polynomial-time Reductions

We now present two reductions from literal-weighted WMC to UMC. Since weighted model count is a real number in general, while unweighted model count is a natural number, any reduction from WMC to UMC must use a normalization constant. Given that all literal weights are of the form ki/2mi , a natural choice for the normalization constant is CF = ∏i∈NF 2-mi . Theorem 1a gives a transformation of an instance (F,W(·)) of literal-weighted WMC to an unweighted Boolean formula ̂ F such that W(F) = CF · |R̂ F |. This reduction is motivated by the need to preserve CNF form of the input formula. We may also allow an additive correction term when doing the reduction. Theorem 1b provides a transformation of (F,W(·)) to an unweighted Boolean formula ˘ F such that W(F) = CF · |R˘ F | - 2n + 2n-|NF | . The motivation for this reduction comes from the need to preserve DNF form of the input formula. Both reductions take time linear in the size of F and in the number of bits required to represent the weights of normal-weighted variables in F .

Note that since CF = 2-̂m, computing CF · |R̂ F | (respectively, CF · |R˘ F |) amounts to computing |R̂ F | (respectively, |R ̂ F |), which is an instance of UMC, and shifting the radix point in the binary representation of the result to the left by ̂m positions.

Theorem1. Let (F,W(·)) be an instance of literal-weighted WMC, where F has n variables. Then, we can construct in linear time the following unweighted Boolean formulas, each of which has n+ ̂m variables and is of size linear in |F |+ ̂m.

Proof. Let X = {x1, · · · , xn} be the set of variables of F. Without loss of generality, let NF = {1, · · · r} be the set of indices of the normal-weighted variables of F. For each normal-weighted variable xi, let ϕki,mi (xi,1, · · · xi,mi ) be the representative formula, as defined above. Let Ω = (x1 ↔ ϕk1,m1 ) ∧ · · · ∧ (xr ↔ ϕkr,mr ).

Proof of part (a): We define the formula ̂ F as follows.

Recalling ̂m = ∑i∈NF mi, it is easy to see that ̂ F has n + ̂m, variables. From Lemma 1, we know that ϕki,mi (xi,1, · · · xi,mi ) is of size linear in mi, for every i in NF . Therefore, the size of Ω is linear in ̂m, and the size of ̂ F is linear in |F| + ̂m.

We now show that W(F ) = CF · |R ̂ F |. Let W ′ (·) be a new weight function, defined over the literals of X as follows. If xi has indifferent weight, then W ′ (x0i ) = W ′ (x1i ) = 1. If xi has normal weight with W (x1i ) = ki/2mi , then W ′ (x1i ) = ki and W ′ (x0i ) = 2mi - ki. By extending the definition of W ′ (·) in a natural way (as was done for W(·)) to assignments, sets of assignments and formulas, it is easy to see that W(F) =W ′ (F) · ∏i∈NF 2-mi =W ′ (F) · CF .

Next, for every assignment σ of variables in X, let σ1 = {i ∈ NF | σ(xi) = true} and σ0 = {i ∈ NF | σ(xi) = false}. Then, we have W ′ (σ) = ∏i∈σ1 ki ∏i∈σ0 (2mi - ki). Let ̂ σ be an assignment of variables appearing in ̂ F. We say that ̂ σ is compatible with σ if for all variables xi in X, we have ̂ σ(xi) = σ(xi). Observe that ̂ σ is compatible with exactly one assignment, viz. σ, of variables in X. Let Sσ denote the set of all satisfying assignments of ̂ F that are compatible with σ. Then {Sσ|σ ∈ RF} is a partition of R̂ F . From Lemma 1, we know that there are ki witnesses of ϕki,mi and 2mi - ki witnesses of ¬ϕki,mi . Since the representative formula of every normal-weighted variable uses a fresh set of variables, we have from the structure of ̂ F that if σ is a witness of F , then |Sσ| = ∏i∈σ1 ki ∏i∈σ0 (2mi -ki). Therefore |Sσ| = W ′ (σ). Note that if σ is not a witness of F , then there are no compatible satisfying assignments of ̂ F ; hence Sσ = ∅ in this case. Overall, this gives

It follows that W(F) = CF · W ′ (F) = CF · |R̂ F |. This completes the proof of part (a).

Proof of part (b): We define the formula ˘ F as follows.

Clearly, ˘ F has n + ̂m variables. Since the size of Ω is linear in ̂m, the size of ˘ F is linear in |F| + ̂m.

We now show that W(F ) = CF · |R ˘ F | -2n · (1-2-|NF | ). First, note that ˘ F is logically equivalent to ¬Ω∨ (F ∧Ω) = ¬Ω ∨ ̂ F, where ̂ F is as defined in part (a) above. Since ̂ F and ¬Ω are mutually inconsistent, it follows that |R˘ F | is the sum of |R̂ F | and the number of satisfying assignments (over all variables in ˘ F) of ¬Ω. By definition, Ω does not contain any variable in X \ NF . Hence, the number of satisfying assignments (over all variables in ˘ F) of ¬Ω is 2n-|NF | · |R¬Ω|. To calculate |R¬Ω|, observe that |R(xi↔ϕki,mi )| = 2mi , and the sub-formulas (xi ↔ ϕki,mi ) and (xj ↔ ϕkj,mj ) have disjoint variables for i ̸= j. Therefore, |RΩ| = ∏i∈NF 2mi = 2 ̂m, and |R¬Ω| = 2 ̂m+|NF | -2 ̂m = 2 ̂m · (2|NF | - 1). From part (a) above, we also know that |R ̂ F | = W(F ) /CF . Hence, |R ˘ F | = |R̂ F |+2n-|NF | · |R¬Ω| = W(F) /CF + 2n+̂m · (1 - 2-|NF | ). Rearraging terms, we get W(F) = CF · (|R˘ F | - 2n+̂m · (1 - 2-|NF | )). Since CF = 2- ̂m, we obtain W(F ) = CF ·|R ˘ F |-2n ·(1-2-|NF | ). This completes the proof of part (b).

Preservation of Normal Forms

The representative formula of a normal-weighted variable is a chain formula, which is generally neither in CNF nor in DNF. Therefore, even if the input formula F is in a normal form (CNF/DNF), the formulas ̂ F and ˘ F in Theorem 1 may be neither in CNF nor in DNF. We wish to ask if our reductions can be adapted to preserve the normal form (CNF/DNF) of F . Theorem 2 answers this question affirmatively.

Theorem2. Let (F,W(·)) be an instance of literal-weighted WMC, where F is in CNF (resp., DNF) and has n variables. We can construct in polynomial time a CNF (resp., DNF) formula F ⋆ such that W(F) = CF · |RF ⋆| (resp., CF · |RF ⋆| - 2n · (1 - 2-|NF | )). Moreover, F ⋆ has n + ̂m variables and its size is linear in (|F| + ∑i∈NF m2i ).

The key step in the proof is an application of Lemma 2 to show that Ω can be expressed in CNF form in size O(∑i∈NF m2i ). The rest of the proof involves Boolean algebraic manipulations of ̂ F and ˘ F .

Optimality of Reductions

We now ask if there exists an algorithm that reduces literalweighted WMC to UMC and gives unweighted Boolean formulas that have significantly fewer variables than ̂ F or ˘ F . We restrict our discussion to reductions that use CF as a normalization constant, and perhaps use an additive correction term D(n,W(·)) that is agnostic to F, and depends only on the number of variables in F and on the weight function. An example of such a term is -2n · (1 - 2-|NF | ), used in Theorem 1, where NF can be determined from W(·) by querying the weights of individual literals.

Theorem 3. Let Reduce(·) be an algorithm that takes as input an instance (F,W(·)) of literal-weighted WMC, and returns an unweighted Boolean formula ˜ F such that W(F) = CF · |R˜ F | +D(n, W(·)), where D(·, ·) is a real-valued function and n is the number of variables in F. Then ˜ F has at least n - 1 + ̂m - 2|NF |) variables.

Observe that the number of variables in ̂ F and ˘ F in Theorem 1 differ from the lower bound given by Theorem 3 by 2|NF | + 1, which is independent of n as well as the number of bits ( ̂m) used to represent weights.

5 Experimental Analysis

The construction outlined in the proof of Theorem 1 naturally suggests an algorithm for solving WMC using a UMC solver as a black-box. This is particularly important in the context of weighted model counting, since state-ofthe-art unweighted model counters (viz. sharpSAT [Thurley, 2006], DSharp [Muise et al., 2012]) scale to much larger problem sizes than existing state-of-the-art weighted model counters (viz. SDD [Darwiche, 2011]). To investigate the practical advantages of using the reduction based approach, we developed a literal-weighted model counter module called WeightCount, that takes as input an instance (F,W(·)) of literal-weighted WMC and reduces it to an instance F ⋆ of UMC, as outlined in Theorem 1 and 2. The WeightCount module then invokes an underlying state-ofthe-art exact UMC solver, to count the witnesses of F ⋆ . Finally, WeightCount computes CF · |R⋆F | as the weighted model count of (F,W(·)). In our experiments we employed both sharpSAT and DSharp as the underlying exact UMC solver.

We conducted experiments on a suite of diverse CNF benchmarks to compare the performance of WeightCount with that of SDD. We also tried to compare our tool with the weighted variant of Cachet [Sang et al., 2005], but despite extensive efforts, we have not been able to run this tool on our system. 1 We focused on CNF formulas because of the availability of CNF model counters and the lack of DNF model counters in the public-domain. The suite of benchmarks used in our experiments consisted of problems arising from probablistic inference in grid networks, synthetic grid-structured random interaction Ising models, plan recognition, DQMR networks, bit-blasted versions of SMTLIB benchmarks, ISCAS89 combinational circuits with weighted inputs, and program synthesis examples. We used a high performance cluster to conduct multiple 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 of our experiments was run on a single core. Note that normal weights of variables in our benchmarks typically correspond to (conditional) probabilities of events in the original problem from which the benchmark is derived. To allow specification of probabilities with a precision of up to to two decimal places, we rounded off the weights such that all weights were of the form k/2i (1 ≤ i ≤ 7). A uniform timeout of 5 hours was used for all tools in our experiments.

1 The weighted variant of Cachet is broken, and its authors have acknowledged this and expressed their inability to fix the tool. We tried fixing it ourselves and have communicated with several other researchers in this respect, but to no avail.

Table 1 presents the results of comparing the performances of WeightCount and SDD on a subset of our benchmarks. 2 In this table, the benchmarks are listed in Column 1. Columns 2 and 3 list the number of variables and clauses, respectively, for each benchmark. Columns 4 through 8 present our experimental observations on running WeightCount via either sharpSAT or DSharp as UMC solvers. Specifically, columns 4 and 5 give the total number of variables and clauses of the unweighted formula obtained after applying our reduction. Note that these numbers are larger than the corresponding numbers in the original problem, since all normal-weighted variables in the original problem have been replaced by their respective representative formulas. The run-time of WeightCount via sharpSAT is the sum of the transform time taken to reduce a WMC instance to an instance of UMC, as presented in Column 6, and the counting time taken by sharpSAT to solve an instance of UMC, as presented in Column 7. The run-time of WeightCount via DSharp is the sum of the transform time as presented in Column 6, and and the counting time taken by DSharp to solve an instance of UMC, as presented in Column 8. Finally, run-time for SDD to solve the same instance of WMC is presented in column 9. A "-" in a column indicates that the corresponding experiment either did not complete within 5 hours or ran out of memory.

Overall, out of 79 benchmarks for which the weighted model count could be computed by either SDD or WeightCount, SDD timed/spaced out on 30 benchmarks, WeightCount via sharpSAT timed out on 1 benchmarks, and WeightCount via DSharp timed out on 11 benchmarks . Table 1 clearly shows that on most benchmarks WeightCount via either sharpSAT or DSharp outperformed SDD in terms of running time by 1 to 3 orders of magnitude. Moreover, WeightCount could generate weighted counts for a large class of benchmarks for which SDD timed out. Thus, our reduction helps in solving instances of literal-weighted WMC that are otherwise beyond the reach of a state-of-the-art weighted model counter. Significantly, column 6 of Table 1 demonstrates that the overhead for reducing a WMC problem to a UMC instance is very small. The comparison between WeightCount via sharpSAT and WeightCount via DSharp is interesting but beyond the scope of this work.

Overall, our experiments demonstrate that state-of-the-art UMC solvers can be augmented with an implementation of our reduction to obtain literal-weighted model counts on formulas with tens of thousands of variables - problems that are clearly beyond the reach of existing weighted model counters. Significantly, our approach requires no modification of the implementation of the UMC solver, which can therefore be treated as a black-box.

6 Beyond Literal Weights

While literal-weighted representation is typically employed in applications of WMC, richer forms of representations of weights are increasingly used in a wide variety of applications. Of these, associating weights to constraints instead of literals has been widely employed in probabilistic programming, verification, and the like [Ver, 2015; Pfeffer, 2009]. For example, Figaro, a popular probabilistic programming framework, contains a construct called setConstraint that associates weights with constraints. We now demonstrate that our techniques can be generalized to handle such representations as well.

2 An extended version of Table 1 is will be available in full version.

Define ConstraintWMC to be a variant of WMC, wherein the weight of an assignment is specified using a set of constraints. Specifically, given a formula F, a set G = (G1, · · ·Gr) of Boolean constraints, and a weight function W(·) over G, the weight of an assignment σ is defined as the product of the weights of constraints in G that are satisfied by σ. The weight of every constraint Gi is assumed to be of the form ki/2mi , where ki is an odd integer between 1 and 2mi - 1. In case σ satisfies none of the constraints in G, the weight of σ is defined to be 1. The ConstraintWMC problem is to compute the sum of the weights of all witnesses of F .

By an extension of the reasoning used in the proof of Theorem 1a, we can obtain an efficient reduction from ConstraintWMC to UMC. We do not yet know how to do this preserving the normal form of the input formula.

Theorem 4. Let (F,G,W(·)) be an instance of ConstraintWMC, where |G| = r and ϕki,mi (xi,1, · · · xi,mi ) is the chain formula that describes W(Gi). Then by defining ̂ F = F ∧ (G1 → ϕk1,m1 ) ∧ · · · ∧ (Gr → ϕkr,mr ), we get a linear-time reduction from ConstraintWMC to UMC, such that W(F) = CG · |R̂ F |, where CG = ∏ri=1 2-mi .

7 Discussion and FutureWork

The recent surge of interest in probabilistic reasoning has propelled WMC to emerge as a key challenging problem. In this paper, we presented new polynomial-time reductions from WMC to UMC that preserve the normal form of the input formula. This provides a framework that allows any UMC solver, viewed as a black box, to be converted to a WMC solver. We also showed that our approach leads to an efficient practical algorithm for literal-weighted WMC for CNF formulas.

The proposed reductions open up new research directions. While we focused on exact WMC in this paper, the computational difficulty of exact inferencing in complex graphical models has led to significant recent interest in approximate WMC [Chakraborty et al., 2014a]. Approximate WMC concerns computing the weighted model count of a formula within a specified multiplicative tolerance and with a desired minimum confidence. In this context, it is worth noting that the reduction proposed in Theorem 1a allows us to lift approximation guarantees from the unweighted to the weighted setting for CNF formulas. Unfortunately, this is not the case for the reduction proposed in Theorem 1b, which is required for DNF formulas. The question of whether there exists an approximation-preserving reduction from WMC to UMC that also preserves DNF is open. The practical feasibility of solving approximate WMC problems by reducing them to their unweighted counterpart, even in the case of CNF formulas, requires further detailed investigation. This is particularly challenging since the current reductions introduce extra variables, which is known to adversely affect XOR-hashingbased state-of-the-art approximation techniques [Ermon et al., 2014; Chakraborty et al., 2014b].

Another interesting direction of research is CNF/DNFpreserving reductions from ConstraintWMC to UMC. Investigations in this direction can lead to improvements in both modeling and inferencing techniques in probabilistic programming frameworks. The design of practically efficient unweighted DNF model counters is also a fruitful line of research, since our reduction allows us to transform any such tool to a weighted DNF model counter.