Scaling up Hybrid Probabilistic Inference with Logical and Arithmetic Constraints via Message Passing

Weighted model integration (WMI) is a very appealing framework for\nprobabilistic inference: it allows to express the complex dependencies of\nreal-world problems where variables are both continuous and discrete, via the\nlanguage of Satisfiability Modulo Theories (SMT), as well as to compute\nprobabilistic queries with complex logical and arithmetic constraints. Yet,\nexisting WMI solvers are not ready to scale to these problems. They either\nignore the intrinsic dependency structure of the problem at all, or they are\nlimited to too restrictive structures. To narrow this gap, we derive a\nfactorized formalism of WMI enabling us to devise a scalable WMI solver based\non message passing, MP-WMI. Namely, MP-WMI is the first WMI solver which allows\nto: 1) perform exact inference on the full class of tree-structured WMI\nproblems; 2) compute all marginal densities in linear time; 3) amortize\ninference inter query. Experimental results show that our solver dramatically\noutperforms the existing WMI solvers on a large set of benchmarks.\n