Efficient Symbolic Integration for Probabilistic Inference

1 Introduction

Weighted model counting (WMC) is the problem of computing the mass of a function over the set of models of a propositional theory and lies at the heart of probabilistic artificial intelligence, where a core issue is to quantify uncertainty over logically-structured worlds. Many state-of-the-art algorithms dealing with discrete Bayesian networks [Chavira and Darwiche, 2008], factor graphs [Choi et al., 2013], probabilistic programs [Fierens et al., 2013], and probabilistic databases [Suciu et al., 2011] reduce their inference problem to a WMC computation. While a typical WMC inference task is to compute the partition functions and marginals of factored probability distributions, it has also been used as a subroutine for more general tasks such as automated planning [Domshlak and Hoffmann, 2007].

Many of these successes have been powered by the development of 1) efficient model counting strategies and 2) efficient data structures for manipulating Boolean theories that support WMC. Inference in continuous and mixed discretecontinuous theories, however, had neither enjoyed fast algorithms, nor was it known whether there are efficient data structures for manipulation, until recently. Progress on the algorithmic front accelerated with the introduction of weighted model integration (WMI) [Belle et al., 2015] which extends the usual WMC setting by including real-valued variables, linear real-arithmetic (LRA) theories and symbolic weight functions. WMI (or closely related formulations) have recently been applied to a number of non-trivial graphical modeling and probabilistic programming tasks [Chistikov et al., 2015; Albarghouthi et al., 2017; Morettin et al., 2017; Belle, 2017; Braz et al., 2016]. On the data structure front, an extension of algebraic decision diagrams (ADDs) to piecewise polynomial functions over continuous linear and Boolean theories, so-called extended ADDs (XADDs), was proposed in Sanner et al. (2011) and when combined with symbolic dynamic programming techniques has proven successful for probabilistic planning as well as probabilistic inference [Sanner and Abbasnejad, 2012]. In the software verification community, a subset of XADDs dealing with piecewise-constant functions was independently developed under the name linear decision diagrams (LDDs) [Chaki et al., 2009].

Although impressive, progress in the mixed discretecontinuous domain on both the algorithmic and data structure front is still far from its Boolean counterpart. Most WMI solvers are based on the so-called block-clause strategy, which naively enumerates the models of a LRA theory and is often prohibitive in practice. Finally, most solvers, including improved variants such as the predication abstraction solver introduced by Morettin et al. (2017), do not consider partial WMI and the efficient storage of intermediate results of computation, which can speed up computing repeated conditional queries, occurring in tasks such as parameter estimation from data. Indeed, Belle et al. (2016) considered component caching but is restricted to interval formulas. From the data-structure perspective, current XADD methods suffer from an extremely high cost for integration inWMI; this has severely limited their application to problems with only a handful of variables and formulas [Sanner and Abbasnejad, 2012]. Finally, many probabilistic programming problems, see e.g. the argument of Braz et al. (2016), involve Boolean, real-valued but also integervalued variables, however, both existing state-of-the-art WMI

solvers and XADDs currently do not support integer-valued variables. An exception is actually the work of Braz et al., which is probably closest to our work in terms of functionality. It supports both integer and real values, but does not represent and cache intermediate results, and Morettin et al. (2017) showed that their solver achieved better performance.

In this paper, we address both shortcomings of XADDs and provide additional extensions. Our contribution is centered around a novel and powerful symbolic dynamic programming algorithm for marginalization and integration. Concretely, we make the following contributions: 1) we explore the use of XADDs [Sanner et al., 2011] as a compilation language for WMI and show how to structure WMI problems as symbolic dynamic programming over XADDs; 2) we contribute a novel marginalization and integration algorithm for XADDs that efficiently computes partial integrations, improving the state-of-the-art integration algorithms [Sanner and Abbasnejad, 2012] by exploiting shared substructures in the XADD's directed acyclic graph through caching and we additionally show how to handle integer-valued variables; and 3) we show that the algorithm can be adapted for volume computations and, moreover, that XADDs can be used to compute partial WMI through partial integration, obtaining parametrized solutions that can be used for repeated query computations or, for example, computing the argmax for the remaining variables.

Our empirical results show that our novel WMI solver can lead to an exponential to linear computational reduction over previous state-of-the-art solvers for problem domains containing high levels of mutually exclusive or XOR structure, and that its performance exceeds or matches existing WMI solvers.

We remark that the decision versions of both #SAT and Bayesian inference are #P-complete. Nonetheless, the caching of partial computations and memoization schemes have been shown to achieve strong time-space tradeoffs, and are often very effective in practice [Bacchus et al., 2009].

2 Background

Foundations of WeightedModel Integration. We assume that the reader is familiar with propositional logic and the SAT problem. Satisfiability Modulo Theories (SMT) generalizes SAT to determining the satisfiability of a formula with respect to a decidable background theory. We consider the background theories LRA and LIA, which are first-order logic fragments restricting the interpretation of numbers, inequalities and operators (sum, product) to their semantics in linear real and integer arithmetic, respectively, as in, e.g., a ∧ (b ∨ (u + v ≤ 5)).

Model counting (#SAT) refers to the task of counting the number of models that satisfy a given formula. Weighted model counting (WMC) generalizes this task by summing the weights assigned to models satisfying a formula. Corresponding to the generalization of SAT to hybrid domains, weighted model integration (WMI) generalizes WMC to support SMT(LRA) formulas and real variables [Belle et al., 2015]. We, additionally, extend the WMI formulation to also support linear arithmetic over integers (LIA). Formulas are then Boolean combinations of Boolean literals, inequalities over real variables and inequalities over integer variables, which we will refer to as LA formulas.

Given n real variables x, m Boolean variables A, p integer variables I, an LA formula θ(x, A, I) over x, A and I and a weight function w(x, A, I) that maps variable assignments to real weights, the weighted model integral (WMI), following its most recent definition [Morettin et al., 2017], is defined as (using WMI (θ, w) to abbreviate WMI (θ, w|A, x, Z)):

That is, the WMI is obtained by summing over every pair of total truth assignments µA and µZ to the Boolean- and integer variables, substituting every Boolean or integer variable in θ and w with its truth value in µA or µZ , and integrating w(x, µA, µZ ) over the values {x∗ |θ(x∗ , µA, µZ )}.

In order to obtain algorithmic results we restrict w to the class of piecewise-polynomial case functions, i.e.,

where the fi are polynomial functions over real and integer variables and the case conditions θi are LA formulas that partition the underlying space. This class strictly generalizes the class of polynomial under LRA conditions functions [Morettin et al., 2017]. As input language for defining polynomial case functions, we fix the language of nested arithmetic and ite compositions, i.e., a single case φ = {θ : f, ¬θ : 0} is a case function; if φ1, φ2 are case functions, then so are φ1 + φ2, φ1 ∗ φ2, and, ite(θ, φ1, φ2), where θ is a sentence from one of B, LRA or LIA, and ite expands to if-then-else understood in the usual manner. This language corresponds to the one implemented in the well-known PySMT package [Gario and Micheli, 2015]. A case function is identified by its PySMT abstract syntax tree.

Decision diagrams. DDs or arithmetic circuits are used to compactly represent logical formulas by compiling them into directed acyclic graphs (DAGs) whose internal nodes are labeled by atoms and whose leaf nodes are labeled by expressions. Every internal node has two edges labeled with true (⊤) and false (⊥) (traditionally called high and low) that correspond to the atom of the internal node being satisfied or not. We denote the label of an internal node f by fC or C(f), its two child nodes as f⊤ and f⊥, following the high and low edge respectively, the label of an edge e as v(e) and the expression of a leaf node l as exp(l).

Binary decision diagrams (BDDs) use Boolean variables as atoms and truth values ({⊤, ⊥} or {1, 0}) as expressions. Any propositional logical formula can be compiled into a BDD and decision diagrams support various efficient operations. E.g., computing SAT for a formula represented by a BDD corresponds to determining if there is a path from the root to 1. We consider three extensions of BDDs: LDDs, ADDs and XADDs (Table 1). LDDs support LRA atoms over continuous variables in internal nodes while ADDs allow an arbitrary number of leaf expressions labeled with real numbers. XADDs extends both by allowing LRA atoms in internal nodes as well as arbitrary symbolic polynomial functions over continuous variables in leaf nodes. Some XADD operations restrict the leaf nodes to be, e.g., linear functions.

XADDs [Sanner et al., 2011] represent case functions with linear inequality conditions and polynomial values. Every path in an XADD corresponds to a case and its DAG structure allows compact representation of multiple cases with common structure (see Fig. 1 for an example XADD). For a path p = n1 →e1 ... →en-1 nn →en l, the case condition and function can be obtained by taking the conjunction of the labels of the nodes and the expression of the leaf node l, respectively:

One of the advantages of DDs is that they allow operations to be performed on them. The if-then-else (ite) construct allows DDs to be combined. E.g., given two decision diagrams d1 and d2 and a condition atom c, we can construct a new diagram d = ite(c, d1, d2). The new diagram introduces a new internal node n with nC = c, n⊤ = d1 and n⊥ = d2, i.e., it behaves as d1 if c is fulfilled and as d2 otherwise. By using the so-called apply operation we can apply a binary operator to two decision diagrams. This operation constructs a new DD that corresponds to the composition of the two functions represented by the input diagrams. For BDDs and LDDs, diagrams are combined using ∧ and ∨, for ADDs and XADDs, diagrams can also be combined using element-wise sum and product, and both support marginalization for Boolean variables. In addition, XADDs also support integration for real variables. We refer to marginalization through summation and integration (based on the variable type) as SO, short for sum-out. For real variable x, integer variable i, Boolean variable b and an XADD Xf corresponding to a polynomial case function f over x, i, b, we obtain SO(x, Xf ) = ∫ ∞ -∞ f (x)dx, SO(i, Xf ) = ∑∞i=-∞ f and SO(b, Xf ) = ∑b∈{⊥,⊤} f . We write SO(b, SO(i, SO(x, Xf ))) as SO∗ ({x, i, b}, Xf ).

3 XADDCompilation forWMI

We propose a top-down compilation scheme to convert an SMT(LA) formula or polynomial case function from a nested arithmetic and ite abstract syntax tree to a valid XADD with a consistent node ordering. Our scheme recursively applies a set of grammar rules defined inductively in Table 2. The three base cases convert polynomials (including constants) to equivalent single-leaf XADDs and SMT(LA) literals a or ¬a to 0-1 XADDs with a single test on a corresponding to ite(a, 1, 0) or ite(a, 0, 1), respectively. For composite expressions, the terms are recursively compiled and combined using the XADD apply operator [Sanner et al., 2011] that automatically collapses paths sharing sub-diagrams.

Example 1. The XADD depicted left in Fig. 1 is obtained by compiling the WMI problem with θ = x ≥ v∧(x < y∨x ≤ z) and w = ite(x ≤ z ∧ x ≥ w, 3x2 , 2x).

Marginalization for XADDs is currently supported for tests over Boolean variables, LRA atoms and difference arithmetic atoms, i.e., over a subset of LIA. In this paper we consider marginalization through summation and integration, leaving other operations, such as maximization, as future work.

Theorem 1. Given an SMT(LA) formula θ and a polynomial case function w both over Boolean, integer and real variables A, Z and x, then, using Xψ = comp(ψ):

Proof. Any case function defined by the input language of nested ite and arithmetic combinations can be compiled to an XADD by recursively applying the rules of Table 2. Similarly, every SMT(LA) function can be compiled to a 0-1 case function by the same procedure. Since Xθ ∗Xw = Xite(θ,w,0) and WMI (θ, w) = WMI (⊤, ite(θ, w, 0)), summing out all variables from Xθ ∗ Xw yields the weighted model integral.

4 Novel XADD Partial Integrator

Having clarified that WMI-amenable theories of interest can be compiled to XADDs, we now discuss the WMI computation.

The computational cost of the XADD marginalization (SO) algorithm introduced by Sanner et al. (2012) is often prohibitive even for relatively simple models. We identify the main issue as the inability to effectively cache intermediate results of the integration process in the XADDs DAG and in this section we aim to develop more efficient alternatives. In the following, we: 1) review Sanner et al.'s algorithm that is based on path enumeration; 2) introduce and discuss two variants of a novel algorithm based on bound resolution that introduce caching to SO; 3) conclude with an extension of XADDs and the marginalization algorithms to integer theories.

Every internal node containing a numeric variable x imposes an upper-bound on one child and a lower bound on the other. For the sake of brevity, we assume in our algorithms and discussions that upper bounds are always imposed on the high child and that all numeric variables are continuous (not integer). In practice, the algorithmwould detect if an internal node test imposes a lower or upper bound and swap the child nodes if necessary. Note that w.r.t. integrating continuous variables strict and non-strict inequalities are equivalent.

4.1 Path Enumeration

Sanner et al. 's SO algorithm is summarized in Alg. 1. Essentially, it works like a symbolic version of DPLL, expanding the XADD DAG into an XADD tree, i.e., it recursively traverses every path in the XADD, collecting all expressions that can bound the integration variable x along the way. Reaching a leaf, the recursion returns the leaf integral ∫x∈C f(x)dx, where the set C is the intersection of bounds on x collected during the descent. Since C may depend parametrically on all non-integrated variables, the integral is computed symbolically as follows. For each bound pair u ∈ U, l ∈ L, we consider the case where u is the smallest of all possible upper bounds and l is the largest of all lower bounds, described by the formula θul := ∧u′∈U (u ≤ u′ ) ∧l′∈L(l ≥ l′ ) ∧ (u ≥ l) , where the last atom ensures consistency (the upper bound must be at least as large as the lower bound for the integral to be well-defined). These formulas partition the space completely, so the integral of {θ : f} is then the case function {θul : ∫ u x=l f(x)dx | ul ∈ U ×L}. Let us quickly illustrate this with an example.

Example 2. Consider the case function corresponding to the red path of Fig. 1 (omitting the cases where the result is 0):

The XADD of that integral is illustrated in Fig. 1, right.

The computational disadvantage of this algorithm is that it does not exploit the DAG structure of the XADD. This is reflected in the fact that the SO function receives all upper/lower bounds accumulated so far as an argument, hence the output of each recursive call depends on the entire context from which it is called. This eliminates any opportunity for caching, and what looks as dynamic programming is essentially a treestructured recursion which must always traverse exponentially many paths. This renders the algorithm inapplicable on anything but toy models.

This is also akin to the depth-first PRAiSe algorithm [Braz et al., 2016] which explicitly uses a symbolic extension of DPLL but not XADDs to represent piecewise functions.

Algorithm 1 Integration using path enumeration.

• 1: procedure SO(var x, XADD f, U, L) 2: ▷ U: upper-bounds, L: lower-bounds 3: if f is terminal then 4: return integrate(x, f, U, L) 5: if x ∈ fC then 6: (l, u) ← get bounds(x, fC) 7: return SO(x, f⊤, U ∪ {u}, L) +SO(x, f⊥, U, L ∪ {l}) 8: return ite(fC, SO(x, f⊤,U,L), SO(x, f⊥,U,L))

4.2 Bound Resolution

We will now develop two alternatives of this algorithm that introduce increasing amounts of caching. The main idea is as follows: instead of collecting all candidate bounds until the bottom of the recursion and then introducing cases to compare among them, we maintain a single upper and lower bound candidate. As soon as a new potential upper or lower bound appears due to some test, the recursion introduces two cases: 1) if the new upper bound is greater than the current one, we keep the current bound and descend on child node; 2) if the new upper bound is less than the current one, it replaces the current bound before we descend on the child node. In the latter case, a consistency test is added to enforce that the new upper bound is greater than the current lower bound. For our first version, Alg. 2, we end up with the following recursive rule for the upper bound:

The output of this algorithm is identical to the output of Alg. 1, however, the context influence is reduced to only the upper and lower bound candidate. Hence, the triple u, l, f can serve as the key for caching the result.

Example 3. Reconsider the left XADD from Fig. 1. Both the green path and the blue path will at some point encounter the call SO(x, 3, z, v) as on both paths z and v appear as upper- and lower bound to x, respectively, and both paths go through node 3. However, since the two paths go through different branches of node 2, the recursion for green also invokes SO(x, 3, v, y), whereas the recursion for blue invokes SO(x, 3, y, z). The latter two calls cannot profit from caching even though the paths generating them rejoin in the diagram.

Finally, we consider the version of Alg. 2b which is completely context-independent. The key idea is that instead of calling SO(x, f⊤, unew, l), the same result is obtained by calling SO(x, f⊤, uS, lS), where uS and lS are symbolic variables, and then substituting uS by unew and lS by l in the resulting XADD. Similarly, we obtain SO(x, f⊤, u, l)) by substituting uS by u and lS by l. Notice that while unew is available at the time of the recursion call, as it comes from the current node, we want to eliminate u from the list of arguments. Hence, the second branch of the ite expression is left with the dummy variable uS as a placeholder. This will be substituted with the various upper bounds as the algorithm emerges from the recursion. We end up with the following

Algorithm 2 Integration using bound resolution

(2a) Algorithm for bound-pair caching

• 1: procedure SO(var x, XADD f, u, l) 2: ▷ u: current upper-bound, l: current lower-bound 3: if f is terminal then 4: return integrate(x, u, l, f) 5: if x /∈ fC then 6: return ite(fC, SO(x, f⊤, u, l), SO(x, f⊥, u, l)) 7: (lnew, unew) ← get bounds(x, fC) 8: fu ← ite(unew > u, SO(x, f⊤, u, l), (unew ≥ l) ∗ SO(x, f⊤, unew, l)) 9: fl ← ite(lnew < l, SO(x, f⊥, u, l), (lnew ≤ u) ∗ SO(x, f⊥, u, lnew))
• 10: return fu + fl

(2b) Algorithm for symbolic caching

• 1: procedure SO(var x, XADD f) 2: 3: if f is terminal then 4: return integrate(x, f) 5: if x /∈ fC then 6: return ite(fC, SO(x, f⊤), SO(x, f⊥)) 7: (lnew, unew) ← get bounds(x, fC) 8: fu ← ite(unew > uS, SO(x, f⊤), (unew ≥ lS) ∗ SO(x, f⊤){uS/unew})
• 9: fl ← ite(lnew < lS, SO(x, f⊥), (lnew ≤ uS) ∗ SO(x, f⊥){lS/lnew})
• 10: return fu + fl

recursive step:

where uS/unew denotes the substitution of the dummy variable uS by the concrete bound unew. We have now eliminated any context information from the call to SO, and the result of SO(x, f) depends only on f. This algorithm is able to reuse any partial computation, exactly as the marginalization algorithm on ADDs, and can be implemented in bottom-up message-passing style, as is characteristic for dynamic programming algorithms. To see the difference with the previous version, note that the entire computation of the integral under node 3 on Fig. 1 can be reused for both green and blue paths.

It is important to note that the second version of the algorithm does not subsume the first. Unlike the Boolean setting, where more caching almost universally improves performance, for linear theories this is not always the case. Having concrete bounds allows us to prune the diagram early by detecting conflicting bounds, e.g., if unew ≥ l can be detected to be unsatisfiable, the recursion can be terminated. In practice, the first version seems to be the most versatile.

4.3 Theory-specific considerations

We currently support XADDs that, aside from Boolean variables, can contain either real or integer variables. For integer variables symbolic summation is used instead of symbolic integration. 1 In order to guarantee that (symbolic) summation bounds are integral, we need to restrict the language of the tests. One amenable sub-theory of LIA is difference arithmetic. Additionally, for the integration of real variables, strict and weak inequalities are equivalent (the set of boundary points has measure zero), hence negation is obtained by simply flipping the inequality. However, for integer variable this is not the case, e.g., the inverse of x ≤ 5 is x > 5 or x ≥ 6, which leads to some implementation differences. Finally, a pruning routine for inconsistent paths in XADDs is implemented using linear programming for real variables, while for integer variables we currently use SMT(LIA) solvers as an oracle for testing inconsistency, as well as linear programming for a relaxed version of inconsistency.

1 Implemented in Python using sympy [Meurer et al., 2017].

5 XADD Integration forWMI

We can now show how WMI can be realized using XADD based SO-algorithms. Specifically, we introduce two techniques for solving single WMI problems and then propose a partial-WMI algorithm for computing probabilities of sets of WMI queries efficiently.

5.1 WMI using Repeated SO

Calculating the WMI corresponds to summing out a set of variables from an XADD, i.e., SO∗ (vars,X). The simplest way to compute the outcome is to reuse an SO algorithm for XADDs, e.g., path enumeration or bound resolution, and sum out variables one by one.

5.2 WMI usingMass-SO

Alternatively, we can tweak our recursive bound-resolution algorithm to immediately sum-out all variables before emerging. This algorithm requires an variable-ordered XADD in which the ordering of tests in the XADD depends on the variables occurring in them. Specifically, given a variable ordering O = v1, v2, ..., vn we call an XADD variable-ordered with respect to O if any test whose last variable has rank i, i.e., it has position i in the ordering, occurs deeper in the diagram than any test whose last variable has a lower rank j < i. The last variable of a test is the variable in the test with the highest rank. The modified algorithm now proceeds by first summing out the variable v1 with the lowest rank using the original bounds-resolve algorithm (Alg. 2) and, whenever a test is encountered whose last variable vj is ranked higher than the current variable vi, summing out variables vi+1, ..., vj-1, vj recursively before proceeding to sum out vi from the resulting diagram. The ordering guarantees that after summing out a variable with rank i, the resulting diagram contains no variable with rank j ≥ i.

5.3 Partial WMI for Computing Query Probabilities

In practice, weighted model integration is used to compute query probabilities, where queries are arbitrary SMT(LA) formulas over both Boolean and numeric variables. Given a query q over variables vars(q) ⊆ D, its probability is obtained by computing the ratio WMI (θ∧q,w|D) WMI(θ,w|D) . Current solvers obtain this answer by computing both volumes separately and dividing the results. For a set Q of n queries, this requires n + 1 WMI computations. By exploiting symbolic SO, we propose a new technique for computing probabilities for sets of queries. This approach can drastically reduce the execution time when the number of variables DQ occurring in any query is much lower than the number of variables in the domain. The algorithmWMI ∗ consists of three steps: 1) it pre-computes a temporary diagram XQ by summing out variables D \ DQ that do not occur in any query; 2) it computes WMI (θ, w) by summing out variables VQ from XQ; and 3) for every query q it computes WMI (θ ∧ q, w) by summing out variables VQ from XQ ∗ Xq .

Theorem 2. Given θ, Q and w over variables D, as before, then WMI ∗ computes { WMI (θ∧q,w|D) WMI(θ,w|D) |∀q ∈ Q}.

Proof. The algorithm computes WMI (θ ∧ q,w|D) and WMI (θ,w|D), where q = ⊤, using SO. Since WMI (θ ∧ q,w|D) = SO∗ (D,Xθ ∗ Xq ∗ Xw) and Xq is independent of D \ DQ it follows that the WMI can be computed as SO∗ (DQ, SO∗ (D \ DQ, Xθ ∗ Xw) ∗ Xq).

XQ is the result of partial WMI, i.e., WMI (θ, w|D \ DQ), and it should be clear that this can also be used to compute, e.g., argmaxDQ XQ, which is a standard XADD operation.

6 Empirical Evaluations

We analyze the performance of our improved SO algorithm and how XADDs can be used to tackle WMI problems. First, we demonstrate our algorithms ability to exploit caching in very structured diagrams. Second, we compare our algorithm to the current XADD-based SO algorithm [Sanner and Abbasnejad, 2012] and the state-of-the-art WMI solver [Morettin et al., 2017] (PA) on WMI computation for synthetic benchmark problems from the paper by Morettin et al. Third, we show how partial integration for XADDs can be leveraged to repeatedly compute query probabilities and compare this approach to the PA solver. We generally use the ordering in which literals (or variables for mass-SO) appear during compilation. The code for the implementations used in our evaluation can be found at: https://xadd-wmi.github.io.

6.1 Structured diagrams

Our SO algorithm exploits caching in order to avoid redundant computations when sub-diagrams can be reached by multiple paths. We investigate the performance of our algorithm on two common types of heavily structured problems: 1) mutualexclusivity (also called exactly one) formulas; and 2) XOR formulas.

These structured constraints arise naturally in data and in modeling multi-valued attributes using arithmetic circuits, where each multi-valued attribute is converted into multiple binary variables with mutual exclusivity constraints.

For both problem types, given a number of terms n, we introduce n + 1 variables V = {c1, ..., cn, x}, n + 1 terms that introduce real-valued bounds for the variables (e.g., bx = ((lx ≤ x) ∧ (x ≤ ux)) where lx, ux ∈ R ∧ (lx < ux)) and n terms T = {x ≤ c1, ..., x ≤ cn}. Then we compute the mutual-exclusivity formula fME and the XOR formula fXOR as follows:

We compute WMI (fXOR, 1|V ) and WMI (fME, 1|V ) for increasing n using bound resolution, path enumeration, and the state-of-the-art WMI solver.

For both the XOR- and mutual-exclusivity-problems, our algorithm is able to compute the volume in well under 120 seconds as its execution time grows slowly with the problem size. Therefore, it outperforms the state-of-the-art approaches that both exhibit exponentially growing execution times, see Fig. 2.

6.2 Predicate-abstraction solver benchmark

In the paper [Morettin et al., 2017], the authors demonstrate that their approach outperforms Praise [Braz et al., 2016] and block-clause based approaches [Belle et al., 2015] using a set of synthetically generated problems. Using the publicly available code for the PA solver we generated 50 such WMI problems and compared the performance of: 1) SO using path enumeration; 2) SO using bound-resolution; 3) mass-SO using bound-resolution; and 4) the PA solver. For every problem we record the execution time per solver, with a time-out of 60s.

Both bound-resolution based algorithms and the PA solver can compute any of the problems within 60 seconds, while the path enumeration based algorithm times out for many of the problems (Fig 3). Both bound-resolution based algorithms outperform the predicate-abstraction based solver by solving more problems faster. Additionally, the mass-SO approach solves all but one problem within a second.

6.3 Answering sets of WMI queries

As described earlier, computing the probabilities of a set of queries can be sped up using XADDs. We compare our approach to the state-of-the-art WMI solver by comparing the time required to solve an increasing number of queries for a set of benchmark WMI problems consisting of random pairs of nested SMT formulas and polynomial case functions in the form of PySMT ASTs, generated using the predicate-abstraction solver software package. For every problem 100 queries were generated consisting of different inequalities over the variable of interest.

Our experiments show that our partial integration approach can achieve large speedups as the number of queries increases (Fig. 4). Since only few variables occur in the queries, our approach results in much lower execution times per query as it avoids repeatedly computing the WMI for all variables. Time-outs can occur since, for arbitrary XADDs, operations may lead to exponential numbers of nodes, however, in practice variable-reordering strategies can help alleviate this problem. Reordering schemes based on sifting have shown to be effective for arithmetic based diagrams [Chaki et al., 2009].

7 Conclusion

Weighted model integration (WMI) is a promising and general approach to reasoning about mixed discrete and continuous spaces needed for probabilistic inference. We proposed the first XADD-based WMI solver that can cache partial computations, smartly exploit DAG structure in integration, and handle integer-valued variables. Empirical results show this new WMI solver performs comparable to state-of-the-art solvers and often drastically better. We also showed that XADDs are a suitable compilation language for WMI and we hope it serves as a step towards making WMI as versatile a tool as WMC.

Acknowledgements

Samuel Kolb is supported by the Research FoundationFlanders (FWO-Vlaanderen).