Hashing-Based Approximate Probabilistic Inference in Hybrid Domains: An Abridged Report

1 Introduction

Weighted model counting (WMC) on a propositional knowledge base is an e↵ective and general approach to probabilistic inference in a variety of formalisms, including Bayesian and Markov Networks. It extends the model counting task, or #SAT, which is to count the number of assignments (or models) that satisfy a logical sentence [Gomes et al., 2009]. In WMC, one accords a weight to every model, and computes the sum of the weights of all models. The WMC formulation has recently emerged as an assembly language for probabilistic reasoning, o↵ering a basic formalism for encoding various inference problems. State-of-the-art reasoning algorithms for Bayesian networks [Chavira and Darwiche, 2008], probabilistic programs [Fierens et al., 2013] and probabilistic databases [Suciu et al., 2011] reduce their inference problem to a WMC computation. Exact WMC solvers are based on Andrea Passerini University of Trento passerini@disi.unitn.it knowledge compilation or component caching [Chavira and Darwiche, 2008].

⇤This is an abridged version of a paper that appeared in the Proceedings of Uncertainty in Artificial Intelligence, 2015.

However, exact inference is #P-hard [Valiant, 1979], and so, there is a growing interest in approximate model counters. Beginning with Stockmeyer [1983], who showed that approximating model counting with a tolerance factor can be achieved in deterministic polynomial time using a ⌃ P 2 - oracle, a number of more recent results show how random polynomial-time realizations are possible using an NP-oracle, such as a SAT solver [Jerrum et al., 1986; Karp et al., 1989; Ermon et al., 2013; Chakraborty et al., 2014]. The central idea here is the use of random parity constraints, in the form of universal hash functions [Sipser, 1983], that partition the model counting solution space in an inexpensive manner. Most significantly, such methods come with tight toleranceconfidence guarantees, unlike classical variational methods that only provide asymptotic guarantees.

The popularity of WMC can be explained as follows. Its formulation elegantly decouples the logical or symbolic representation from the statistical or numeric one, which is encapsulated in the weight function. When building solvers, this allows us to reason about logical equivalence and reuse SAT solving technology (such as constraint propagation and clause learning). WMC also makes it more natural to reason about deterministic, hard constraints in a probabilistic context. Nevertheless, WMC has a fundamental limitation: it is purely Boolean. This means that the advantages mentioned above only apply to discrete probability distributions.

To counter this, in a companion paper [Belle et al., 2015b], we proposed the notion of weighted model integration (WMI). It is based on satisfiability modulo theories (SMT), which enable us to reason about linear arithmetic constraints. The WMI task is defined on the models of an SMT theory ∆, containing mixtures of Boolean and continuous variables. For every assignment to these variables, the WMI problem defines a weight. The total WMI is computed by integrating these weights over the domain of solutions of ∆, which is a mixed discrete-continuous space. Consider, for example, the special case when ∆ has no Boolean variables, and the weight of every model is 1. Then, WMI simplifies to computing the volume of the polytope encoded in ∆. More generally, weighted SMT theories admit a natural encoding of hybrid graphical models, analogous to the encodings of discrete graphical models using weighted propositional theories.

In this work, we consider the problem of approximating inference tasks for a probability distribution defined over discrete and continuous random variables. Formulated as a WMI task, we address the question as to whether fast hashing-based approximate WMC solvers can be leveraged for hybrid domains. What we show is that an NP-oracle can indeed effectively partition the model counting solution space of the more intricate mixed discrete-continuous case using universal hashing. (Of course, volume computation via integration is still necessary, but often over very small spaces.) In this sense, hybrid domains can now be put within reach of approximate WMC solvers. 1 In particular, the hashing approach that we consider here builds on the recent work of Chakraborty et al. [2014] on approximate WMC, and inherits their toleranceconfidence guarantees. In our empirical evaluations, the approximate technique is shown to be significantly faster than an exact WMI solver. We then demonstrate the practical efficacy of the system on a complex real-world dataset where we compute conditional queries over intricate arithmetic constraints that would be difficult (or impossible) to realize in existing formalisms.

Let us finally mention that current inference algorithms for hybrid graphical models often make strong assumptions on the form of the potentials, such as Gaussian distributions, or approximate using variational methods [Murphy, 1999]. There is also a recent focus on piecewise-polynomial potentials [Shenoy and West, 2011; Sanner and Abbasnejad, 2012], which are based on generalizations of techniques such as the join-tree algorithm. Such piecewise-polynomials can also be represented in the WMI context, but in a general framework allowing arbitrary Boolean connectives and deterministic hard constraints.

2 WeightedModel Integration

We briefly review the ideas behind WMI.

From a probabilistic perspective, we are imagining a set of Boolean random variables B and real-valued random variables X. In particular, we let (b, x) = (b1, . . . , bm, x1, . . . , xn) be an element of the probability space ¶0, 1♦m ⇥ R n , and we let Pr(b, x) denote the probability of the assignments (b, x) to the variables in B [ X. Assuming the joint probability density function Pr can be suitably factorized, e.g. via graphical models, we would like to perform probabilistic inference, that is, compute things like the partition function and conditional probabilities [Koller and Friedman, 2009].

For the discrete case, that is, when limited to Boolean variables B only, 2 , a prominent approach to perform inference is WMC [Chavira and Darwiche, 2008]. The idea is to encode the graphical model as a weighted propositional theory, and then compute the model count on this theory. Recall that SAT is the problem of finding a satisfying assignment M to a propositional formula φ. WMC, an extension of #SAT, computes the number of models of φ, and defines a weight to each of these based on the input theory. Formally, Given a formula ∆ in propositional logic over literals L, and a weight function w : L ! R, WMC is defined as:

1 In an independent and recent e↵ort, Chistikov et al. [2015] also introduce the notion of approximate model counting for SMT theories. The most significant di↵erence between the proposals is that they focus only on unweighted model counting. Moreover, they define model counting as a measure on first-order models. Our approach is a simpler one that, as we will see, allows us to cast statements for WMI in terms of WMC.

2 Handling random variables that take values from finite sets, rather than ¶0, 1♦, is also possible [Sang et al., 2005], but we omit a discussion on this for simplicity.

where, w(M) is shorthand for Q l2M w(l). Here, given an assignment (or model) M, we write M ♣= φ to denote satisfaction. We write l 2 M to denote the literals (that is, propositions or their negations) that are satisfied at M. We often write M(φ) to mean the set of models of φ.

The key insight behind WMI is that for hybrid graphical models, we would need to talk about satisfiability and model counting over logical theories with propositions (for B) as well as real-valued variables (for X). This is made possible by satisfiability modulo theories (SMT) technology [Barrett et al., 2009]. More precisely, in SMT, DPLL is generalized to decide the satisfiability of a (typically quantifier-free) firstorder formula with respect to some decidable background theory T . Formally, assume a bijection between ground firstorder atoms (from the language of linear arithmetic) and a propositional vocabulary; formula abstraction, denoted φ-, proceeds by replacing the atoms by propositions, and refinement, denoted φ + , replaces the propositions with the atoms. For example, if ∆ = (x  4) ^ (x  5), then ∆- = p ^ q where (say) p denotes x  4 and q denotes x  5; also, q + = x  5. Then, suppose ∆ is an linear arithmetic theory over Boolean and rational variables B and X, and literals L. Suppose w : L ! EXPR(X), where EXPR(X) are expressions over X . WMI is defined as:

The intuition is as follows. The WMI of a linear arithmetic theory ∆ is defined in terms of the models of its propositional abstraction ∆-. For each such model, we compute its volume, that is, we integrate the weight values of the literals that are true at the model. The interval of the integral is obtained from the refinement of each literal. Finally, EXPR(X) is the weight function mapping an expression e to its density function, which is usually another expression mentioning the variables in e.

To see a very simple example, let ∆ = (0  x) ^ (x  10), and suppose w maps (0  x) to 2 and (x  10) to x. Suppose p ^ q is the abstraction. Then ∆ has only one model, namely the one where both p and q are true, and we find:

Thus, WMI(∆, w) = 100.

The correctness of WMI and the fact that it is a strict generalization of WMC are argued elsewhere [Belle et al., 2015b].

3 ApproximatingWMI

The purpose of this section is to identify how to approximate WMI(∆, w). As mentioned before, we would like such an algorithm to come with strong theoretical guarantees. To better understand what we o↵er, consider the well-understood WMC version [Chakraborty et al., 2014]:

Definition 1: Given a propositional sentence ∆ and a weight function w, an exact algorithm for WMC returns WMC(∆, w). An approximate algorithm for WMC given tolerance ✏ 2 (0, 1] and confidence 1 - δ 2 (0, 1], simply called an (✏, δ)- algorithm, returns a value v such that

Intuitively, when the weight of every model is 1, an exact algorithm returns the size of the set M(∆) = ¶M ♣ M ♣= ∆♦ while an approximate one samples from that solution space. The main question, then, is how can we sample from an unknown solution space while o↵ering such tight bounds? We return to this question shortly.

3.1 Problem Statement

To see how the above notion applies to our task, consider an SMT theory ∆ and weight function w. We observe that

where, for any model M of ∆-, u is a weight function such that u(M) = VOL(M, w). More precisely, u is to be seen as a weight function that does not factorize over literals and directly maps interpretations to R. (This is without any loss of generality.) Thus, our problem statement becomes:

Definition 2: An (✏, δ)-algorithm for a WMI problem over ∆ and w is an (✏, δ)-algorithm for WMC over ∆- and weight function u, where for any model M of ∆-, u(M) = VOL(M, w).

The idea is that by treating the volumes of models as weights over propositional interpretations, we can viewWMI simply in terms of WMC. Theoretical results can then be inherited.

There are two caveats, however. First, the weights on the propositional abstraction need to be actually computed using integration during inference. Second, such an algorithm samples feasible satisfying assignments for ∆-, but these need not be consistent in arithmetic. For example, if p denotes x  3 and q denotes x ≥ 5, then the interpretation ¶p, q♦ is not a model in linear arithmetic. We refer interested readers to the full paper [Belle et al., 2015a] for details on how these are addressed.

3.2 Approach

Approximate algorithms for model counting (i.e. when the weights are uniform) with strong guarantees have been the focus of many papers, e.g. [Jerrum et al., 1986; Karp et al., 1989; Ermon et al., 2013; Chakraborty et al., 2014]. The main technical device is the use of uniform hash functions [Sipser, 1983], a discussion of which we omit here. Roughly speaking, given a propositional theory φ, rather than counting M(φ) exactly, which is #P-hard, one computes the models of φ^χ, where χ is a random parity constraint corresponding to the hash function. The parity constraint has the e↵ect of partitioningM(φ) into a set of well-balanced cells: such a cell is a relatively small subset of the solution space. We count solutions for such cells, which is relatively easy owing to their size, and leverage that count as an estimate for the solution space as a whole. It can be shown that for an efficient family of hash functions, such an approach provides the desired bounds.

At this point, our formulation for approximating WMI is basically agnostic about the counting algorithm used, giving us a direct way to adapt its bounds. In this paper, we demonstrate that by leveraging the work of Chakraborty et al. [2014] (CFMSV henceforth). As argued by Ermon et al. [2013], the one major limitation when applying approximate model counters for probabilistic inference is that weights play an important role in deeming which samples are interesting. Therefore, uniformly sampling from M(φ) is not appealing, and would lead to poor estimates of conditional probabilities. The approach taken by CFMSV is to bias the sampling by means of a parameter called tilt.

Definition 3: Suppose (∆, w) is a weighted propositional theory. Let wmax = maxMw(M) and let wmin = minMw(M). We define the tilt ✓ to be the ratio wmax/wmin.

They introduce an algorithm WeightMC(∆, w, ✏, δ, ✓) for which they show (our rewording):

Theorem 4 : [CFMSV] Suppose (∆, w) is a weighted propositional theory, and ✏, δ, ✓ are as above. Then WeightMC(∆, w, ✏, δ, ✓) is an (✏, δ)-algorithm for WMC(∆, w). Given a SAT-oracle, it runs in time polynomial in log 2 (1/δ), ✓, ♣∆♣ and 1/✏ relative to the oracle.

For our purposes, we adapt the notion as follows:

Definition 5: Suppose (∆, w) is a weighted SMT theory. Let wmax = maxM VOL(M, w) and let wmin = minM VOL(M, w). We define the tilt ✓ to be the ratio wmax/wmin.

We then compute:

where u is calculated using u(M) = VOL(M, w).

We are (almost) done. The algorithmWeightMC has to be adapted to address the caveats mentioned earlier (theory consistency, computing integrals optimally). We argued in [Belle et al., 2015a] that this adaption does not a↵ect the algorithm's theoretical properties, which allows us to show:

Corollary 6: Suppose ∆ is an SMT theory, w is a weight function, and ✏, δ, ✓ are as above. Suppose u is the derived weight function for ∆-. Then, WeightMC(∆-, u, ✏, δ, ✓) is an (✏, δ)-algorithm for WMI(∆, w). Suppose we are given an oracle to the weight function u and a SAT-oracle. Then, WeightMC(∆-, u, ✏, δ, ✓) runs in time polynomial in log 2 (1/δ), ✓, ♣∆-♣ and 1/✏ relative to the oracles.

The oracle to u computes the volumes of T -consistent models, which is shown to be efficient by Baldoni et al. [2011].

4 Empirical Evaluations

We now study the scaling behavior and expressivity of an approximate inference system on a complex real-world scenario; see [Belle et al., 2015a] for a comprehensive report and implementation details. The scenario involves computing conditional queries over arithmetic constraints, and is based on a data series released by the UK government that provides the average journey time, speed and traffic flow information on all motorways in England, known as the Strategic Road Network. 3 Motorways are split into junctions, and each information record refers to a specific junction, day and time period. Figure 1 shows the portion of the network around the A6 motorway, limited to at most two junctions from A6.

Imagine a planning problem for a supply system for motorway service stations. The operations center (located, say, somewhere along A6) receives supply requests from a number of stations, and needs to predict whether the delivery vehicle will be able to reach all stations and return within a certain amount of time. Travel time between every pair of stations, and between stations and the operations center, is computed in terms of shortest paths across the network. We compute shortest paths for both minimum and maximum travel times, so as to get a distribution for the shortest path duration wrt every pair of relevant points (stations and operations center). Then, given a certain route between stations, the probability of completing it within the desired time can be computed by integrating over travel time distributions between consecutive stops.

For example, based on our statistical model, the probability of beginning from the operations center at 8 a.m. and completing the route touching A14, A1304, A43, and A5199 by 9 a.m. is: Pr(T < 3600) = 0.765. Here, T is the time taken for the route in seconds. Suppose, however, we request that station A14 should be reached only after visiting A1304 (owing to a delivery request between these two stations) but A1304 should not be visited before 8:30 a.m. (say, because the package to deliver will not be available until then). Then the system would compute: Pr(T < 3600 ♣ tA14 > tA1304 ^ tA1304 ≥ 1800) = 0.557. Finally, suppose a last constraint were to require the station A5199 to be also visited after 8:30 a.m. (say, when a package to be delivered to the operations center will be made available). This additional constraint makes it infeasible to complete the route in the required time: Pr(T < 3600 ♣ tA14 > tA1304 ^ tA1304 ≥ 1800 ^ tA5199 ≥ 1800) = 0.

3 http://data.gov.uk/dataset/dft-eng-srn-routes-journey-times

We use this construction as a template for considering cycle paths of increasing lengths to study the implementation extensively (see the full paper for details). To the best of our knowledge, a probabilistic inference system for hybrid specifications against intricate Boolean combinations of propositional and arithmetic constraints has not been deployed on such a scale previously.

5 Conclusions

We introduced a novel way to leverage a fast hashing-based approximate WMC methodology for inference with discrete and continuous random variables. On the one hand, SAT technology can now be exploited in challenging inference and learning tasks in hybrid domains. On the other, strong tolerance-confidence guarantees can be inherited in this more complex setting. Weighted SMT theories allow a natural encoding of hybrid graphical networks while also admitting the specification of arithmetic constraints in conditional queries, all of which are difficult to realize in standard formalisms. We demonstrated its practical efficacy in a complex novel application, deployed on a scale not considered previously.