--- title: "Efficient Weighted Model Integration via SMT-Based Predicate Abstraction" authors: - "Paolo Morettin" - "Andrea Passerini" - "Roberto Sebastiani" doi: "10.24963/ijcai.2017/100" url: "https://ijcai.org/proceedings/2017/100" pdf: "https://ijcai.org/proceedings/2017/0100.pdf" venue: "Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence" year: 2017 pages: "720-728" track: "Main track" keywords: - "Uncertainty in AI: Relational Inference" - "Uncertainty in AI: Exact Probabilistic Inference" - "Constraints and Satisfiability: Constraints and Satisfiability" --- # Efficient Weighted Model Integration via SMT-Based Predicate Abstraction Paolo Morettin, Andrea Passerini, Roberto Sebastiani *Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence*, pages 720-728. DOI: [10.24963/ijcai.2017/100](https://doi.org/10.24963/ijcai.2017/100) ## Abstract Weighted model integration (WMI) is a recent formalism generalizing weighted model counting (WMC) to run probabilistic inference over hybrid domains, characterized by both discrete and continuous variables and relationships between them. Albeit powerful, the original formulation of WMI suffers from some theoretical limitations, and it is computationally very demanding as it requires to explicitly enumerate all possible models to be integrated over. In this paper we present a novel general notion of WMI, which fixes the theoretical limitations and allows for exploiting the power of SMT-based predicate abstraction techniques. A novel algorithm combines a strong reduction in the number of models to be integrated over with their efficient enumeration. Experimental results on synthetic and real-world data show drastic computational improvements over the original WMI formulation as well as existing alternatives for hybrid inference. ## Full text ## 1 Introduction Weighted model counting (WMC) is the task of computing the weighted sum of all satisfying assignments of a propositional formula, where weights are associated to models and are typically factorized into the product of weights of individual variables. In recent years, WMC was shown to be an effective solution for addressing probabilistic inference in a wide spectrum of formalisms [Chavira and Darwiche, 2008; Choi et al., 2013; Suciu et al., 2011]. An inherent limitation of WMC is that it can only deal with discrete distributions. In order to overcome this restriction, weighted model integration (WMI) [Belle et al., 2015] was recently introduced as a formulation generalizing WMC to deal with hybrid domains, characterized by both discrete and continuous variables and their relationships. The formalism relies on satisfiability modulo theory (SMT) [Barrett et al., 2009] technology, which allows to reason about the satisfiability of formulas involving e.g. linear constraints over integers or reals. WMI works by replacing the weighted sum of models of a propositional formula with a sum of integrals over weight functions defined over the models of an SMT formula. Weight functions here play the role of (un-normalized) densities, whereas logic formulas in the model define the integration domain. In this paper, we elaborate on the notion of WMI and provide a refined formalization fixing some theoretical and practical limitations of the original definition. The novel formalization guarantees that equivalent formulas have the same WMI, and that probabilistic manipulations like marginalization are always consistent. A novel notion of conditional weight function allows for a more effective decomposition of the function into its separately integrable components. Building on the properties of this novel formulation, we devise an efficient algorithm combining a strong reduction in the number of models to be generated and integrated over, with efficiency in enumerating these models. The key ingredient is the use of SMT-based predicate abstraction techniques [Graf and Sa¨ıdi, 1997; Lahiri et al., 2006; Cavada et al., 2007] to efficiently and effectively generate the set of models needed to compute the exact integral. Our experimental evaluation confirms that the approach is drastically faster than existing alternatives over synthetic and realworld problems, and that both aspects contribute to the gain. ## 2 Background ## 2.1 SMT, AllSMT and Predicate Abstraction We assume the reader is familiar with the basic syntax, semantics and results of propositional and first-order logics. We adopt some terminology and concepts from Satisfiability Modulo Theories (SMT), which we briefly summarize below (see [Sebastiani, 2007; Barrett et al., 2009] for details). Our context is that of SMT on quantifier-free formulas in the theory of linear arithmetic over the reals, LRA. R denotes the set of real values and B def= {⊤,⊥} the set of Boolean values. LRA formulas are combinations by means of the standard Boolean operators {¬, ∧, ∨, →, ↔} of atomic propositions Ai ∈ B (aka Boolean atoms/variables) and of LRA atomic formulas (aka LRA atoms) in the form (∑i cixi ▷◁ c), s.t. xi are variables in R, ci are rational values and ▷◁ ∈ {=, ̸=, ≥, ≤, >, <}, with their usual semantics. "|=LRA" denotes entailment in LRA (e.g. (x ≥ 2) |=LRA (x ≥ 1)), whereas "|=B" denotes tautological entailment (e.g. A1∧(x ≥ 2) |=B ((A1∨(x ≤ 1))∧(¬A1∨(x ≥ 2)).) Notice that |=B is strictly stronger than |=LRA. ϕ1, ϕ2 are LRAequivalent, written ϕ1 ⇔LRA ϕ2, iff |=LRA (ϕ1 ↔ ϕ2). We frequently use the following abbreviations. Let t, ti be LRA terms, ϕ, ϕi be LRA formulas, and I = [l, u] be some interval; then we use "Jt∈ IK" as a shortcut for the formula (t ≥ l) ∧ (t ≤ u), possibly with ">" or "<" if some end of the interval is open; we use "(If ϕ Then t1 Else t2)" to represent an if-then-else conditional expression, returning the value of t1 if ϕ holds, the value of t2 otherwise; we use "(Case ϕ1 : t1; ϕ2 : t2; ...)" to generalize the if-thenelse to the case of multiple mutually-exclusive conditions. We use "OneOf({ϕ1, ..., ϕn})" as a shortcut for the formula (∨ni=1 ϕi) ∧ ∧1≤i<j≤n ¬(ϕi ∧ϕj), i.e, exactly one ϕi holds. Given a set of LRA formulas Ψ def= {ψ1, ..., ψK}, we call a total [resp. partial] truth assignment µ for Ψ any total [resp. partial] map from Ψ to B. We represent µ alternatively and equivalently either as a set or a conjunction: We denote by BK the set of all truth assignments over Ψ. Let x def= {x1, ..., xN} ∈ RN and A def= {A1, ...,AM} ∈ BM for some N and M. Consider a generic LRA formula ϕ on (subsets of) x and A, and let Ψ def= Atoms(ϕ), i.e. the set of propositional and LRA atoms occurring in ϕ. Given a truth assignment µ for Atoms(ϕ), we denote by µA and µLRA its two components on the Boolean atoms in A and on the LRA atoms respectively, so that µ = µA ∧ µLRA. (E.g., if µ = A1 ∧¬A2 ∧(x ≥ 1)∧¬(x ≥ 3), then µA = A1 ∧¬A2 and µLRA = (x ≥ 1) ∧¬(x ≥ 3)). Importantly, and unlike with pure propositional logic, µ can be LRA-unsatisfiable due to its µLRA component (e.g. µ def= ¬A1 ∧ (x1 + x2 = 3) ∧ ¬(x1 + x2 ≥ 2)). A (possibly partial) truth assignment µ propositionally satisfies ϕ iff µ |=B ϕ. The SMT problem for ϕ in LRA is the problem of checking the existence of a LRA-satisfiable assignment µ s.t. µ |=B ϕ. We denote by TTA(ϕ) def= {µ1, ..., µj, ...} the set of all LRA-satisfiable total truth assignments µj on Atoms(ϕ) propositionally satisfying ϕ. TTA(ϕ) is unique. We denote by TA(ϕ) def= {µ1, ..., µj , ...} any set of LRA-satisfiable possibly-partial truth assignments µj propositionally satisfying ϕ, s.t. every pair µi, µj assign opposite truth values to at least one element, i.e., µi ∧ µj |=B ⊥ (hence µi ∧ µj |=LRA ⊥). TA(ϕ) is not unique, and TTA(ϕ) is a particular case of TA(ϕ). The disjunction of the µj's in TA(ϕ) is LRA-equivalent to ϕ (see e.g. [Sebastiani, 2007]): The AllSMT problem for ϕ in LRA is the problem of enumerating one set TA(ϕ) matching the above definition. For example, if ϕ def= (x ≤ 0) ∨ (x ≥ 1), then TTA(ϕ) def= {(x ≤ 0) ∧¬(x ≥ 1), ¬(x ≤ 0) ∧ (x ≥ 1)}. (TTA(ϕ) does not contain (x ≤ 0) ∧ (x ≥ 1) as it is not LRA-satisfiable.) The other admissible TA(ϕ)'s are: {(x ≤ 0), ¬(x ≤ 0) ∧ (x ≥ 1)} and {(x ≥ 1), (x ≤ 0) ∧¬(x ≥ 1)}. The set of unary truth assignments {(x ≤ 0), (x ≥ 1)} is not an admissible TA(ϕ) because there is no atom to which they assign different truth values, i.e., (x ≤ 0) ∧ (x ≥ 1) ̸|=B ⊥. Definition 1 Let ϕ(x,A) be a LRA-formula on x and A; let Ψ def= {ψ1, ..., ψK} be a set of LRA-formulas over x and A, and B def= {B1, ...,BK} be a set of fresh atomic propositions s.t. A ∩ B = ∅. Then we call a Predicate Abstraction of ϕ wrt. Ψ on B, namely PredAbs[ϕ,Ψ](B), (any formula equivalent to) the propositional formula We define PredAbs[ϕ](Ψ) def= PredAbs[ϕ,Ψ](B)[B ← Ψ], that is, the LRA-formula obtained from PredAbs[ϕ,Ψ](B) by substituting each Bk with its corresponding ψk. Importantly, if Ψ is A, then PredAbs[ϕ](A) reduces to ∃x.ϕ(x, A). Notice that in Definition 1 the formulas ψi are neither necessarily atomic, nor necessarily sub-formulas of ϕ. PredAbs[ϕ,Ψ](B) defines an equivalence class of Boolean formulas over B, i.e., (2) may represent many syntacticallydifferent albeit logically-equivalent Boolean formulas. Very effective SMT-based techniques for computing PredAbs[ϕ,Ψ](B)-and hence PredAbs[ϕ](Ψ)-have been proposed in the literature (e.g. [Lahiri et al., 2006; Cavada et al., 2007]) and are implemented in modern SMT solvers like MATHSAT5 [Cimatti et al., 2013]. Very importantly for our purposes, these techniques work by iteratively producing a set of propositional truth assignments on B, which are then disjoined as in (1). In particular MATHSAT5, on demand, can either produce a set of total assignments TTA(PredAbs[ϕ,Ψ](B)), or a set of partial ones TA(PredAbs[ϕ,Ψ](B)) by means of assignmentminimization techniques. (3) is built as the disjunction of total assignments on B, whereas (4) is built as the disjunction of partial ones-e.g., by the clause-minimization techniques in MATHSAT5-s.t.: Notice also that the other two total assignments, B1 ∧B2 and B1 ∧ ¬B2, are not part of (3) because they force the formula to be LRA-unsatisfiable. ⋄ ## 2.2 WeightedModel Counting and Integration WMC is the task of computing the weighted sum of all satisfying assignments of a propositional formula, with weights typically factorized as a product of weights over literals. Definition 2 (WeightedModel Count) Let ϕ be a propositional formula and let w be a function associating a nonnegative weight to each atom in ϕ, both asserted and negated. The Weighted Model Count of ϕ is defined as: WMI generalizes WMC to hybrid domains. Following is the original definition of WMI [Belle et al., 2015], which serves as a starting point for our revised formulation. The definition assumes LRA formulas, for which efficient solvers exist, albeit the concept could in principle accommodate other theories over continuous domains. ## Definition 3 (WeightedModel Integral) Let ϕ be a LRA formula on the set of LRA variables x def= {x1, ..., xN} and Boolean atoms A def= {A1, ..., AM}. Let w be a function associating an expression (possibly constant) over x to each atom in ϕ, both asserted and negated. The Weighted Model Integral of ϕ is defined as: ## 3 WeightedModel Integration, Revisited Definition 3 is a very direct and intuitive generalization of WMC to the hybrid case. Nethertheless, it suffers from some theoretical and practical limitations, which are fixed by the revised formalization we introduce in this section. First, Definition 3 implicitly assumes WMI to be computed over the Boolean and LRA variables in the formula. Explicitly defining the domain is however of primary importance in order to guarantee consistency e.g. in marginalization, as will be shown in the following (see Remarks 1 and 2). Second, the fact that weights are associated to literals can produce situations in which two formulas are equivalent, but their WMI over the same weight function w differ. Our novel formalization guarantees instead that two LRAequivalent formulas have the same WMI (Property 2.b). ⋄ Finally, the fact that the summation is over all total truth assignments may be a major source of inefficiency, because often many LRA atoms do not really contribute to the computation of the WMI. Our novel formalization allows to model these cases, opening the way to a more efficient algorithm for WMI computation (see §5). ## 3.1 Basic case: WMI Without Atomic Propositions We investigate first the simple case where no atomic proposition comes into play. Let x def= {x1, ..., xN} ∈ RN . We consider thus a generic weight function w(x) s.t. w : RN ↦-→ R+, and LRA formulas ϕ(x) s.t. ϕ : RN ↦-→ B. Definition 4 Assume ϕ does not contain atomic propositions and w : RN ↦-→ R+. Then the Weighted Model Integral of w over ϕ on x is defined as: "nb" meaning "no-Booleans", that is, as the integral of w(x) over the set {x | ϕ(x) is true}. The following property of WMInb(ϕ, w|x) derives directly from Definition 4. Property 1 Given x, w, ϕ, and ϕ′ as above, - a. if ϕ is LRA-unsatisfiable, thenWMInb(ϕ,w|x) = 0. - b. if ϕ⇔LRA ϕ′ , then WMInb(ϕ, w|x) = WMInb(ϕ′ , w|x) Remark 1 We stress the fact that in the definition of WMInb(ϕ,w|x) specifying the domain "|x" is of primary importance. In fact, even if some xn does not occur in ϕ, WMInb(ϕ,w|x) = ∫R WMInb(ϕ,w|x\{xn}) dxn ̸= WMInb(ϕ,w|x\{xn}). "|x" defines the dimensions of the space we are integrating on, which must be stated. (E.g., integrating on volumes differs from integrating on surfaces.) ## 3.2 General Case: WMI With Atomic Propositions We investigate now the general case, where atomic propositions come into play and both w and ϕ depend also on them. Let A def= {A1, ...,AM} ∈ BM . We consider thus a generic weight function w(x,A) s.t. w : RN × BM ↦-→ R+, and LRA formulas ϕ(x, A) s.t. ϕ : RN × BM ↦-→ B. In what follows, µA denotes a total truth assignment on A, ϕ[µA](x) denotes (any formula equivalent to) the formula obtained from ϕ by substituting every Boolean value Ai with its truth value in µA, and w[µA](x) is w computed on x and on the truth values of µA. Thus, ϕ[µA] : RN ↦-→ B and w[µA] : RN ↦-→R+. Definition 5 Given x, A, the Weighted Model Integral of w over ϕ is defined as follows: where the µA's are all total truth assignments on A. Example 3 Let ϕ def= (A ↔ (x ≥ 0)) ∧ (x ≥ -1) ∧ (x ≤ 1), and w(x,A) def= (If A Then x Else - x). If µA def= {(¬A)}, then ϕ[µA] = ¬(x ≥ 0) ∧ (x ≥ -1) ∧ (x ≤ 1) and w[µA] = -x. Notice that ϕ[µA] can be simplified into the equivalent formula ¬(x ≥ 0) ∧ (x ≥ -1). Similarly, if µA def= {(A)}, then ϕ[µA] can be simplified into (x ≥ 0) ∧ (x ≤ 1) and w[µA] = x. Thus, Notice that in Definition 5 the truth assignments µA of practical interest are only those for which ϕ[µA] is LRAsatisfiable, because for the others WMInb(ϕ[µA],w[µA]|x) = 0 by Property 1.a. We address this issue in §5. The following property of WMI(ϕ,w|x,A) derives directly from Definition 5, by applying Property 1 to w[µA], ϕ[µA], ϕ′[µA] , (ϕ∧ψ)[µA], and (ϕ∧¬ψ)[µA], for every µA. Property 2 Given x, A, w, ϕ, and ϕ′ as above, Remark 2 As with Remark 1, in WMI(ϕ, w|x,A), specifying not only "|x", but also "|x,A" is of primary importance. In fact, even if some of the Am does not occur in ϕ, WMI(ϕ,w|x,A) = WMI(ϕ,w[{Am}]|x,A\{Am}) + WMI(ϕ, w[{¬Am}] |x, A\{¬Am}) ̸= WMI(ϕ, w|x, A\{Am}). Predicate abstraction in Def. 1 and other forms of frequently-used formula manipulations require the introduction of fresh propositions B "labelling" sub-formulas ψ. The next result shows that this does not affect the value of WMI. Theorem 1 Let x, A, w, and ϕ be as in Definition 5; let ψ(x,A) be some LRA-formula; let ϕ′ def= ϕ ∧ (B ↔ ψ), where B ̸∈ A; let w′ extend w s.t. w′ (x,A ∪ {B}) = w(x, A) for every x, A and B. Then we have that Proof (sketch) We notice that ϕ′[µA∧B] ⇔LRA (ϕ ∧ ψ)[µA] and that ϕ′[µA∧¬B] ⇔LRA (ϕ∧¬ψ)[µA], so that (10) follows directly from Definition 5 and Property 1.c. ✷ ## 3.3 Conditional Weight Functions We call a (non-minimal) support of a weight function w(x, A) any subset of RN × BM out of which w(x, A) = 0. In many situations we may want to provide the representation of a support of w(x,A) as a LRA-formula χ(x,A). When this is the case, the following property follows trivially. Property 3 Let ϕ and w be as above. If χ(x,A) is a LRAformula representing a support of w, then: We introduce a novel kind of weight function, which can be defined also in terms of LRA conditions. (See §4 for an example application). We consider first the generic class of functions P(x), which we call feasibly integrable on LRA (F I LRA), which contain no combinatorial component, and for which there exists some procedure able to compute WMInb(µLRA, P |x) for every set of LRA atoms on x. (E.g., polynomials are FI LRA [Baldoni et al., 2011]). Such background procedure, which we use as a blackbox, is the basic building block of our WMI calculations. Definition 6 We call a weight function w(x,A), feasibly integrable under LRA conditions (FIUC LRA) iff it can be described in terms of - a support LRA-formula χ(x, A) (if no support description is provided, than χ def= ⊤), - a set Ψ def= {ψ1(x, A), ..., ψK(x, A)} of LRA-formulas (conditions), in such a way that, for every total truth assignment µA to A and for every total truth assignment µΨ to Ψ, w[µAµΨ](x) is FI LRAin the domain given by the values of 〈x,A〉 which satisfy (χ ∧ µΨ)[µA]. We denote such FI LRAfunctions by fµAµΨ(x), s.t. for every 〈µA, µΨ〉, (Notice that a plain FI LRAweight function is a subcase in which χ def= ⊤ and Ψ def= ∅.) Example 4 Let x def= {x1, x2}, A def= {A}, and w is FIUC LRA. In fact, its value depends on the combination of the truth values of the conditions Ψ def= {(x1 ≥ 0)} and A def= {A} -i.e., of {(x1 ≥ 0), (x2 ≥ 0)} by (14)- so that: f{A,(x1≥0)} = x31 + 3x2 s.t. x1 ∈ [0, 1), x2 ∈ [0, 1), f{A,¬(x1≥0)} = -2x1 + 3x2, s.t. x1 ∈ [-1, 0), x2 ∈ [0, 1), f{¬A,(x1≥0)} = x31 - x52 , s.t. x1 ∈ [0, 1), x2 ∈ [-1, 0), f{¬A,¬(x1≥0)} = -2x1-x52 . s.t. x1 ∈ [-1, 0), x2 ∈ [-1, 0). All four fµAµΨ are positive polynomials in their respective domain and as such they can be integrated. ⋄ Intuitively, Definition 6 captures the class of all the weight functions which can be described by means of arbitrary combinations of nested if-then-elses on conditions in A and Ψ, s.t. each branch 〈µA, µΨ〉 results into a FI LRAweight function. Each pair 〈µA, µΨ〉 describes a portion of the domain of w, inside which w is the FI LRAfunction fµAµΨ. Theorem 2 Let w(x,A), Ψ and χ be as in Definition 6. Let B def= {B1, ...,BK} be fresh propositional atoms and let w∗ (x, A∪B) be the weight function obtained by substituting in w(x, A) each condition ψk with Bk, for every k ∈ [1..K]. Let ϕ∗ def= ϕ∧χ∧ ∧Kk=1 (Bk ↔ψk). Then: Proof To every truth assignment µΨ to Ψ we associate the corresponding truth assignment µB to B s.t. µB(Bk) = µΨ(ψk), for every k ∈ [1..K]. We notice that, for every µA ∈ BM and µB ∈ BK (with its corresponding µΨ): because every ψk is forced by µΨ to assume the same truth value Bk assumes in µB. Let w′ extend w s.t. w′ (x, A∪B) = w(x,A) for every x, A and B. Then, since ϕ∗ forces every Bk to hold if and only if Ψk holds, we have: Then, by applying K times Theorem 1, and then (19): Example 5 Let A = ∅, χ def= (x ≥ -1) ∧ (x ≤ 1), ϕ def= ⊤, ψ def= (x ≥ 0), and the weight w(x) def= (If (x ≥ 0) Then x Else - x). (I.e., w(x) def= |x|. Then WMI(ϕ, w|x, ∅) = WMInb(ϕ, w|x) = ∫[-1,1] |x| dx = 1. By Theorem 1, ϕ∗ = (x ≥ -1) ∧ (x ≤ 1) ∧ (B ↔ (x ≥ 0)) and w∗ = (If B Then x Else - x), which are the same formula and weight function as in Example 3 (modulo some reordering and variable renaming), s.t. WMI(ϕ∗ ,w∗ |x,B) = 1. ⋄ Intuitively, during the computation of the WMIs, Theorem 2 allows for extracting out of the integrals the if-thenelse component on LRA conditions, which are labeled by Boolean atoms and can be thus handled externally. Notice that the pairs of truth assignments 〈µA, µΨ〉 of practical interest are only those for which (χ ∧ µΨ)[µA] is LRA-satisfiable. We will address this issue in §5. ## 4 ACase Study Consider modelling journey time on a road network for e.g. a delivery agency. In order to safely organize priority deliveries, the agency could be interested in knowing well in advance the probability of completing the journey within a certain time, given the time of departure. An accurate estimate requires to consider how travel duration between locations can change according to the time of the day, and combine these duration distributions over the entire route. A different encoding for the same problem was presented in the original WMI work [Belle et al., 2015]. Suppose that the day is partitioned into {I 1 , ..., I M } intervals such that, for each adjacent location li and lj in the road network and for each I m def= [cm, cm+1), we know the distribution of the journey time from li to lj given that we move at time t ∈ I m. Let f m li,lj : R ↦→ R+ denote such distribu- tion and let the interval Rm li ,lj def= [amli,lj , bmli,lj ) be its support. (Notice that the I ms are all disjoint whereas the Rm li,lj s are typically not.) Given a path (l0, ..., lN) and the departure time tdep, we can encode the problem as follows. Let tn be the time at step n and xn the journey time between ln-1 and ln. Let x def= {x1, ..., xN}. (Here A def= ∅.) where "Jtn-1 ∈ I mK" is a shortcut for the LRA formula "(∑n-1 i=1 xi + tdep ≥ cm) ∧ (∑n-1 i=1 xi + tdep < cm+1)", "Jxn ∈ Rm ln-1,lnK" is a shortcut for the LRA formula "(xn ≥ amln-1,ln ) ∧ (xn < bmln-1,ln )", and fn(x) is: (Case Jtn-1 ∈ I 1K : f 1 ln-1,ln (xn); ... Jtn-1 ∈ I MK : f M ln-1,ln (xn)). Under the assumption that each distribution f m li,lj (x) is feasibly integrable if x ∈ Rm li,lj , then w(x) is FIUC LRA with N · M conditions ψm n def= Jtn ∈ I mK. Thus we can introduce N · M fresh Boolean atoms Bm n and apply Theorem 2, s.t.: where f ∗ n (xn, {B1n-1 , ..., BM n-1 }) is the case-split formula (Case B1n-1 : f 1 ln-1,ln (xn); ... BM n-1 : f M ln-1,ln (xn)). Each distribution f m ln-1,ln is thus associated to Bm n . Notice that, for each step n, exactly one condition variable Bm n is true, representing the fact that the n-th location is reached during the m-th interval. Intuitively, this allows to select at each step the distribution corresponding to the interval in which the location is reached. Example 6 Consider an instance of our case study where where the f m ln-1ln (xn) are function which are integrable and positive in their respective domain stated in χ(x) (e.g., f 1 l0l1 (x1) is integrable and positive in Jx1∈ [0.5, 1)K). Then, by applying Theorem 2, we can introduce 6 Boolean variables Bm n and reformulate the problem as follows: ## 5 Efficient WMI Computation We consider the general problem of computing a WMI with a FIUC LRA weight function. The first step (if needed) is a preprocessing in which the problem is transformed by labeling all conditions Ψ with fresh Boolean atoms B, as in Theorem 2. Let ϕ∗ ,w∗ , x,A∗ be the result of such process, where A∗ def=A∪B. Consequently, for every µA∗ , w∗ [µA∗ ] is feasibly integrable on ϕ∗[µA∗ ] . WMI-AllSMT. Consider µ = µA∗ ∧ µLRA ∈ TTA(ϕ∗ ). Then µLRA ∈ TTA(ϕ∗[µA∗ ] ), so that we can compute WMInb(µLRA, w∗ [µA∗ ] |x). This allows us to compute (9) as: The set TTA(ϕ∗ ) is computed by an AllSMT procedure implemented on top of an SMT solver like MATHSAT5-i.e., as TTA(PredAbs[ϕ∗ ](Atoms(ϕ∗ ))), without the assignment-minimization technique (see §2.1); each WMInb(µLRA, w∗ [µA∗ ] |x) is computed by invoking our background integration procedure for FI LRA functions of §3.3. We call this algorithmWMI-AllSMT. ## Algorithm 1 WMI-PA(ϕ, w, x, A) WMI-PA. A much more efficient technique, which we call WMI-PA because it exploits the full power of SMT-based predicate abstraction, can be implemented by noticing that and that eachWMInb(ϕ∗[µA∗ ] ,w∗ [µA∗ ] |x) can be computed as: The pseudocode of WMI-PA is reported in Algorithm 1. First, the problem is transformed (if needed) by labeling conditions Ψ with fresh Boolean variables B. After this preprocessing stage, the set MA∗ def= TTA(∃x.ϕ∗ ) is computed by invoking TTA(PredAbs[ϕ∗ ](A∗ )) (see §2.1). Then, the algorithm iterates over each Boolean assignment µA∗ in MA∗ . ϕ∗[µA∗ ] is simplified by the Simplify procedure, by propagating truth values (e.g., ϕ1 ∧ (⊤ ∨ ϕ2) ∧ (⊥ ∨ ϕ3) ∧ (¬ϕ3 ∨ ϕ4) ⇒ ϕ1 ∧ ϕ3 ∧ ϕ4) and by applying arithmetical simplifications like theory propagation [Barrett et al., 2009]. This improves the chances of reducing ϕ∗[µA∗ ] to a conjunction of literals, and allows for reducing the size of Atoms(ϕ∗[µA∗ ] ) to feed to PredAbs (see below). Then, if ϕ∗[µA∗ ] is already a conjunction of literals, then the algorithm directly computes its contribution to the volume by calling WMInb(ϕ∗[µA∗ ] , w∗ [µA∗ ] |x). Otherwise, TA(ϕ∗[µA∗ ] ) is computed as TA(PredAbs[ϕ∗[µA∗ ] ](Atoms(ϕ∗[µA∗ ] ))), using the minimization technique to produce partial assignments (see §2.1), and the algorithm iteratively computes contributions to the volume for each µLRA. Comparing (23) with (9) -even if ϕ∗ , w∗ , x, A∗ were respectively ϕ,w, x,A- we notice that the restriction of the sum to TTA(∃x.ϕ∗ ) in (23) removes a priori all the assignments µA∗ which cannot be expanded by any assignment µLRA s.t. µA∗ ∧µLRA propositionally satisfy ϕ∗ and µLRA is LRA-consistent, whose integrals would be 0-valued. We argue that WMI-PA produces much less calls to the background integration procedure WMInb(µLRA,w∗ [µA∗ ] |x) thanWMI-AllSMT, for two main reasons. First, the size of Atoms(ϕ∗[µA∗ ] ) which is fed to PredAbs in (24) can be made much smaller than the number of LRAatoms in Atoms(ϕ∗ ) fed to PredAbs in (22), since many LRA-atoms are simplified out by µA∗ . (E.g., (x ≤ 1)∧(A2∨ (x ≥ 0)))[A2] is simplified into (x ≤ 1), so that (x ≥ 0) is eliminated.) Thus, for each µA∗ , the number of assignments in the form µA∗ ∧ µLRA which are enumerated in (23)-(24) can be drastically reduced wrt. those enumerated in (22). Second, with (24) it is possible to search for a set TA(...) of partial assignments, each of which substitutes 2i total ones, i being the number of unassigned LRA-atoms. Notice that, unlike with Boolean atoms, we can safely produce partial assignments on LRA-atoms because w(x, A) does not depend directly on them. (If ϕ∗[µA∗ ] def= (x ≥ 0)∧((x ≤ 2)∨(x ≤ 1)), the partial assignment µLRA def= (x ≥ 0) ∧ (x ≤ 2) prevents enumerating the two total ones µLRA ∧ (x ≤ 1) and µLRA ∧ ¬(x ≤ 1), computing one integral rather than two. Example 7 Consider the problem described by ϕ∗ and w∗ in Example 6. Suppose we want to leave l0 no earlier than 7 and no later than 10, and arrive to l2 strictly before 11. These constraints correspond to conjoining Jtdep ∈ [7, 10)K ∧ (tarr = tdep + x1 + x2) ∧ (tarr < 11) to ϕ∗ . In such case, PredAbs[ϕ∗ ](B) is the following formula: so that TTA(PredAbs[ϕ∗ ](B)) is the set of the three disjuncts (25)-(27). Importantly, notice that the other 6 assignments, which would make ϕ∗ LRA-unsatisfiable causing WMInb to return 0, are not generated by PredAbs[ϕ∗ ](B). (E.g., if B1 0 = ⊤ then l1 is necessarily reached strictly before 9, which forces B3 1 = ⊥, s.t. the assignment (B1 0 ∧ ... ∧B3 1 ) is not generated.) Suppose we fix tdep to some value val ∈ [7, 10) by conjoining (tdep = val) to ϕ∗ (see §7): if val ∈ [7, 7.5), this forces B1 0 = ⊤, so that TTA(PredAbs[ϕ∗ ](B)) contains only (25) and (26); if val ∈ [7.5, 8), this forces B1 0 = ⊤, so that TTA(PredAbs[ϕ∗ ](B)) contains only (26); if val ∈ [8, 9), this forces B2 0 = ⊤, so that TTA(PredAbs[ϕ∗ ](B)) reduces only to (27); if val ∈ [9, 10), this makes the whole formula LRA-inconsistent, so that TTA(PredAbs[ϕ∗ ](B)) is empty. Now suppose, e.g., we set (tdep = 7.4), so that TTA(PredAbs[ϕ∗ ](B)) contains only (25) and (26). Let (25) be the first assignment selected in the for loop, that is, µB def= (B1 0 ∧¬B2 0 ∧¬B3 0 ∧B1 1 ∧¬B2 1 ∧¬B3 1 ). Propagating its truth values inside ϕ∗ and w∗ in (20) and (21) and simplifying the truth values, we obtain: 1 ϕ∗[µB] is a conjunction of LRA-literals, so that WMInb can be invokes on it directly without further invoking another predicate abstraction. ⋄ ## 6 RelatedWork Most works on probabilistic inference in hybrid graphical models are either limited to joint Gaussian distributions [Lauritzen and Jensen, 2001], or perform approximate inference [Gogate and Dechter, 2005; Afshar et al., 2016]. A recent line of research focused on developing exact inference algorithms for graphical models with mixtures of polynomials [Shenoy and West, 2011; Sanner and Abbasnejad, 2012; Wang et al., 2014]. The WMI formalism extends these approaches allowing to represent constraints in terms of arbitrary combinations of Boolean connectives. The first solver for exact WMI [Belle et al., 2015] was a proof-of-concept relying on a simple block-clause strategy (WMI-BC in the following), which iteratively generates new models by adding the negation of the latest model to the formula for the following iteration. In the propositional (WMC) case, substantial efficiency gains can be obtained by leveraging component caching techniques [Sang et al., 2004; Bacchus et al., 2009]. Unfortunately, these strategies are difficult to apply in the WMI case, because of the additional coupling induced by algebraic constraints. A recent work [Belle et al., 2016] did show substantial computational savings in adapting #DPLL with component caching from the WMC to the WMI case. The approach however works with purely piecewise polynomial densities, and cannot be appliedwhenever algebraic constraints exist between variables, e.g. their sum being within a certain range, a rather common situation in many practical cases (see §4). In the same paper, an approach equivalent to WMI-ALLSMT applied to the original WMI formulation was shown to improve over the WMI-BC baseline. Nethertheless, further improvements are not possible without revising the formulation as we do in this work. Closest to WMI is probabilistic inference modulo theories [de Salvo Braz et al., 2016], an elegant framework where a combination of DPLL, SMT and symbolic variable elimination allows to perform probabilistic inference on a variety of theories. While initially focused on integer arithmetic, the system developed by the authors (called PRAISE 2 ) was recently provided with support for arithmetic over the reals and polynomial densities. 1 Notice that Jtdep ∈ [7, 10)K and Jtdep ∈ [7, 8)K are made redundant by (tdep = 7.4); however, they do not affect the result. 2 http://aic-sri-international.github.io/aic-praise/ Figure 1: Query execution times and number of integrals computed in the synthetic setting by the three WMI approaches (resp. left and center). Query execution times of WMI-PA and PRAISE on the Strategic Road Network setting (right). ![Image](https://ijcai.org/proceedings/2017/fulltext/100/image_000000_a44cf56981ad0c9adb1e50165cc6e5c6fc93c2507faf91c61ce411aa3e0ed0d6.png) ## 7 Experiments Our implementation uses MATHSAT5 3 [Cimatti et al., 2013] for SMT reasoning and LATTE INTEGRALE 4 [Loera et al., 2012] to compute integrals of polynomials. All experiments were run on a Virtual Machine with 7 cores running at a frequency of 2.2 GHz and 94 GB of RAM. Query timeout was set at 10000 seconds. When terminating, on each query all tools returned the same value modulo roundings. Synthetic setting. To evaluate the ability of WMI-PA to deal with weight functions with arbitrarily complex supports, we randomly generated LRA formulas like: where N is a parameter controlling the size of ϕ(x,A), RLRA i (x) are randomly generated sets of LRA-atoms over x and RB i (A) are random subsets of A, for i ∈ [1, N]. For each formula ϕ(x,A), randomly generated (polynomial) weight functions are associated to the Boolean variables A. We then compared the performance of WMI-PA in computing randomly generated queries against the WMI-BC baseline (see §6) and WMI-ALLSMT. Figure 1(left) shows the execution time in seconds of the three methods over all randomly generated formulas, where formulas are ordered by increasing running time according to the baseline. Whereas WMI-ALLSMT performs better than the baseline for the most difficult cases, WMI-PA achieves drastic speedups wrt both alternatives. Figure 1(center) reports the number of integrals computed by the three methods, where formulas are ordered as before. The curves for WMI-BC and WMI-ALLSMT are indistinguishable, an expected result as the two formulations generate the very same set of total truth assignments, with WMI-ALLSMT doing it more efficiently. Conversely, the predicate abstraction steps of WMI-PA allow it to drastically reduce the number of assignments, and thus integrals to be computed. Real-world setting. In order to show the applicability of our method to real world tasks, we implemented the case study described in §4. The data was taken from the Strategic Road Network Dataset 5 , which provides average journey times on all the motorways managed by the English Highways Agency. From this dataset we extrapolated polynomial distributions of journey times between all junctions, with a 15 minutes granularity. In this setting, the task is to perform queries of the form P((tN ≤ tarr)|tdep ∧ {li}Ni=0 ). We encoded an equivalent formulation for PRAISE and compared the two approaches 6 over random queries for increasing path lengths. The results in Figure 1(right) show the mean and standard deviation of the execution times for both methods, computed over 5 randomly generated queries for each path length. Our approach is much faster, being able to compute queries up to two steps longer without reaching the timeout. 7 3 http://mathsat.fbk.eu/ 4 https://www.math.ucdavis.edu/∼latte/ ## 8 Conclusion and FutureWork In this paper we proposed a revised definition of WMI which addresses some theoretical and practical limitations of the original formulation. Building on the properties of the novel formulation, we developed an efficient WMI algorithm combining a substantial reduction in the number of integrations with their efficient enumeration. Experimental comparisons over synthetic and real-world data confirm the drastic efficiency improvement over existing alternatives. Future research directions include the study of decomposition strategies for further scalability, and the generalization of WMI to combinations of theories, like linear arithmetic over reals and integers. ## Acknowledgments This work has been partially supported by the EC project CogNet, 671625 (H2020-ICT-2014-2, Research and Innovation action). We thank Alberto Griggio for useful suggestions about the usage of MATHSAT5. 5 https://data.gov.uk/dataset/dft-eng-srn-routes-journey-times 6 WMI-BC and WMI-ALLSMT are not considered here as their execution times are prohibitive for all but the smallest path lengths. 7 Note that the complexity of the query is due to the combination of the path length and the number of time intervals in which the time horizon is divided (M=12 in these experiments). For paths of length 8, the total number of potential cases is M 8 = 429981696. Clearly, many of these cases are unfeasible and are ruled out by the SMT solver before the integration. ## References 1. WMI-BC and WMI-ALLSMT are not considered here as their execution times are prohibitive for all but the smallest path lengths. 7 Note that the complexity of the query is due to the combination of the path length and the number of time intervals in which the time horizon is divided (M=12 in these experiments). For paths of length 8, the total number of potential cases is M 8 = 429981696. Clearly, many of these cases are unfeasible and are ruled out by the SMT solver before the integration. 2. [Afshar et al., 2016] Hadi Mohasel Afshar, Scott Sanner, and Christfried Webers. Closed-form gibbs sampling for graphical models with algebraic constraints. In AAAI, 2016. 3. [Bacchus et al., 2009] Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. Solving #SAT and Bayesian inference with backtracking search. Journal of Artificial Intelligence Research, 34(1):391-442, 2009. 4. [Baldoni et al., 2011] Velleda Baldoni, Nicole Berline, Je- sus De Loera, Matthias Köppe, and Michéle Vergne. How to integrate a polynomial over a simplex. Mathematics of Computation, 80(273):297-325, 2011. 5. [Barrett et al., 2009] Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability Mod- ulo Theories. In Handbook of Satisfiability, chapter 26, pages 825-885. IOS Press, 2009. 6. [Belle et al., 2015] Vaishak Belle, Andrea Passerini, and Guy Van den Broeck. Probabilistic inference in hybrid domains by weighted model integration. In IJCAI, 2015. 7. [Belle et al., 2016] Vaishak Belle, Guy Van den Broeck, and Andrea Passerini. Component caching in hybrid domains with piecewise polynomial densities. In AAAI, 2016. 8. [Cavada et al., 2007] Roberto Cavada, Alessandro Cimatti, Anders Franzén, Krishnamani Kalyanasundaram, Marco Roveri, and RK Shyamasundar. Computing Predicate Ab- stractions by Integrating BDDs and SMT Solvers. In FM- CAD, 2007. 9. [Chavira and Darwiche, 2008] Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172(6-7):772-799, 2008. 10. [Choi et al., 2013] Arthur Choi, Doga Kisa, and Adnan Dar- wiche. Compiling probabilistic graphical models using sentential decision diagrams. In Symbolic and Quanti- tative Approaches to Reasoning with Uncertainty, pages 121-132. Springer, 2013. 11. [Cimatti et al., 2013] Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. The MathSAT 5 SMT Solver. In TACAS, 2013. 12. [de Salvo Braz et al., 2016] Rodrigo de Salvo Braz, Ciaran O'Reilly, Vibhav Gogate, and Rina Dechter. Probabilistic Inference Modulo Theories. In IJCAI, 2016. 13. [Gogate and Dechter, 2005] Vibhav Gogate and Rina Dechter. Approximate inference algorithms for hybrid bayesian networks with discrete constraints. In UAI, 2005. 14. [Graf and Saïdi, 1997] Susanne Graf and Hassen Saïdi. Con- struction of abstract state graphs with pvs. In CAV, 1997. 15. [Lahiri et al., 2006] Shuvendu K. Lahiri, Robert Nieuwen- huis, and Albert Oliveras. SMT techniques for fast predi- cate abstraction. In CAV, 2006. 16. [Lauritzen and Jensen, 2001] Steffen L. Lauritzen and Frank Jensen. Stable local computation with conditional gaus- sian distributions. Statistics and Computing, 11(2):191- 203, 2001. 17. [Loera et al., 2012] Jesus De Loera, Brandon Dutra, Matthias Koeppe, Stanislav Moreinis, Gregory Pinto, and Jianqiu Wu. Software for exact integration of polynomials over polyhedra. ACM Communications in Computer Algebra, 45(3/4):169-172, 2012. 18. [Sang et al., 2004] Tian Sang, Fahiem Bacchus, Paul Beame, Henry A. Kautz, and Toniann Pitassi. Combining com- ponent caching and clause learning for effective model counting. In SAT, 2004. 19. [Sanner and Abbasnejad, 2012] Scott Sanner and Ehsan Ab- basnejad. Symbolic variable elimination for discrete and continuous graphical models. In AAAI, 2012. 20. [Sebastiani, 2007] Roberto Sebastiani. Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Mod- eling and Computation, JSAT, 3(3-4):141-224, 2007. 21. [Shenoy and West, 2011] Prakash P. Shenoy and James C. West. Inference in hybrid bayesian networks using mix- tures of polynomials. International Journal of Approxi- mate Reasoning, 52(5):641-657, 2011. 22. [Suciu et al., 2011] Dan Suciu, Dan Olteanu, Christopher Ré, and Christoph Koch. Probabilistic databases. Syn- thesis Lectures on Data Management, 3(2):1-180, 2011. 23. [Wang et al., 2014] Shenlong Wang, Alex Schwing, and Raquel Urtasun. Efficient inference of continuous markov random fields with polynomial potentials. In NIPS, 2014.