# SMT-based Weighted Model Integration with Structure Awareness

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 24 references that are in the map.
- First posted on arXiv 28 Jun 2022.

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

- [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)

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

- [A Probabilistic Neuro-symbolic Layer for Algebraic Constraint Satisfaction](https://mlsanity.com/paper/2503.19466/) (2025)
- [Enhancing SMT-based Weighted Model Integration by Structure Awareness](https://mlsanity.com/paper/2302.06188/) (2023)
- [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)

## Abstract (arXiv)

Weighted Model Integration (WMI) is a popular formalism aimed at unifying approaches for probabilistic inference in hybrid domains, involving logical and algebraic constraints. 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 substantial computational savings. An extensive experimental evaluation on both synthetic and real-world datasets confirms the advantage of the proposed solution over existing alternatives.