# Enhancing SMT-based Weighted Model Integration by Structure Awareness

arXiv: https://arxiv.org/abs/2302.06188 · HTML: https://mlsanity.com/paper/2302.06188/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 55 references that are in the map.
- First posted on arXiv 13 Feb 2023.

## Builds on (most cited first, 11 of 11)

- [Efficient Search-Based Weighted Model Integration](https://mlsanity.com/paper/1903.05334/) (2019)
- [Scaling up Hybrid Probabilistic Inference with Logical and Arithmetic Constraints via Message Passing](https://mlsanity.com/paper/2003.00126/) (2020)
- [Solving #SAT and Bayesian Inference with Backtracking Search](https://mlsanity.com/paper/1401.3458/) (2014)
- [Approximate Counting in SMT and Value Estimation for Probabilistic Programs](https://mlsanity.com/paper/1411.0659/) (2014)
- [Volesti: Volume Approximation and Sampling for Convex Polytopes in R](https://mlsanity.com/paper/2007.01578/) (2020)
- [Probabilistic Inference Modulo Theories](https://mlsanity.com/paper/1605.08367/) (2016)
- [SMT-based Weighted Model Integration with Structure Awareness](https://mlsanity.com/paper/2206.13856/) (2022)
- [Nonuniform Dynamic Discretization in Hybrid Networks](https://mlsanity.com/paper/1302.1555/) (2013)
- [On the Approximability of Weighted Model Integration on DNF Structures](https://mlsanity.com/paper/2002.06726/) (2020)
- [Are You Satisfied by This Partial Assignment?](https://mlsanity.com/paper/2003.04225/) (2020)
- [Tractable Querying and Learning in Hybrid Domains via Sum-Product Networks](https://mlsanity.com/paper/1807.05464/) (2018)

## Built on by (most cited first, 5 of 5)

- [A Probabilistic Neuro-symbolic Layer for Algebraic Constraint Satisfaction](https://mlsanity.com/paper/2503.19466/) (2025)
- [Canonical Decision Diagrams Modulo Theories](https://mlsanity.com/paper/2404.16455/) (2024)
- [The Theory and Practice of MAP Inference over Non-Convex Constraints](https://mlsanity.com/paper/2602.08681/) (2026)
- [Probabilistic ML Verification via Weighted Model Integration](https://mlsanity.com/paper/2402.04892/) (2024)
- [Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration](https://mlsanity.com/paper/2503.01536/) (2025)

## Abstract (arXiv)

The development of efficient exact and approximate algorithms for probabilistic inference is a long-standing goal of artificial intelligence research. Whereas substantial progress has been made in dealing with purely discrete or purely continuous domains, adapting the developed solutions to tackle hybrid domains, characterised by discrete and continuous variables and their relationships, is highly non-trivial. Weighted Model Integration (WMI) recently emerged as a unifying formalism for probabilistic inference in hybrid domains. Despite a considerable amount of recent work, allowing WMI algorithms to scale with the complexity of the hybrid problem is still a challenge. In this paper we highlight some substantial limitations of existing state-of-the-art solutions, and develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure. This allows our algorithm to avoid generating redundant models, resulting in drastic computational savings. Additionally, we show how SMT-based approaches can seamlessly deal with different integration techniques, both exact and approximate, significantly expanding the set of problems that can be tackled by WMI technology. An extensive experimental evaluation on both synthetic and real-world datasets confirms the substantial advantage of the proposed solution over existing alternatives. The application potential of this technology is further showcased on a prototypical task aimed at verifying the fairness of probabilistic programs.