Advanced SMT techniques for weighted model integration

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. WMI is computationally very demanding as it requires to explicitly enumerate all possible truth assignments to be integrated over. Component caching strategies which proved extremely effective for WMC are difficult to apply in this formalism because of the tight coupling induced by the arithmetic constraints. In this paper we present a novel formulation of WMI, which allows to exploit the power of SMT-based predicate abstraction techniques in designing efficient inference procedures. 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.