# Probabilistic Inference Modulo Theories

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 May 2016.

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

- [Verifying Quantized Neural Networks using SMT-Based Model Checking](https://mlsanity.com/paper/2106.05997/) (2021)
- [Collapsed Inference for Bayesian Deep Learning](https://mlsanity.com/paper/2306.09686/) (2023)
- [Enhancing SMT-based Weighted Model Integration by Structure Awareness](https://mlsanity.com/paper/2302.06188/) (2023)
- [Top-Down Knowledge Compilation for Counting Modulo Theories](https://mlsanity.com/paper/2306.04541/) (2023)
- [Measure Theoretic Weighted Model Integration](https://mlsanity.com/paper/2103.13901/) (2021)

## Abstract (arXiv)

We present SGDPLL(T), an algorithm that solves (among many other problems) probabilistic inference modulo theories, that is, inference problems over probabilistic models defined via a logic theory provided as a parameter (currently, propositional, equalities on discrete sorts, and inequalities, more specifically difference arithmetic, on bounded integers). While many solutions to probabilistic inference over logic representations have been proposed, SGDPLL(T) is simultaneously (1) lifted, (2) exact and (3) modulo theories, that is, parameterized by a background logic theory. This offers a foundation for extending it to rich logic languages such as data structures and relational data. By lifted, we mean algorithms with constant complexity in the domain size (the number of values that variables can take). We also detail a solver for summations with difference arithmetic and show experimental results from a scenario in which SGDPLL(T) is much faster than a state-of-the-art probabilistic solver.