# Canonical Decision Diagrams Modulo Theories

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 43 references that are in the map.
- First posted on arXiv 25 Apr 2024.

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

- [SDDs are Exponentially More Succinct than OBDDs](https://mlsanity.com/paper/1601.00501/) (2016)
- [Enhancing SMT-based Weighted Model Integration by Structure Awareness](https://mlsanity.com/paper/2302.06188/) (2023)
- [Disjoint Partial Enumeration without Blocking Clauses](https://mlsanity.com/paper/2306.00461/) (2023)
- [Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories](https://mlsanity.com/paper/1401.3878/) (2014)
- [Top-Down Knowledge Compilation for Counting Modulo Theories](https://mlsanity.com/paper/2306.04541/) (2023)
- [Model Counting Modulo Theories](https://mlsanity.com/paper/1504.02796/) (2015)

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

- [A Fast Convoluted Story: Scaling Probabilistic Inference for Integer Arithmetic](https://mlsanity.com/paper/2410.12389/) (2024)
- [Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration](https://mlsanity.com/paper/2503.01536/) (2025)

## Abstract (arXiv)

Decision diagrams (DDs) are powerful tools to represent effectively propositional formulas, which are largely used in many domains, in particular in formal verification and in knowledge compilation. Some forms of DDs (e.g., OBDDs, SDDs) are canonical, that is, (under given conditions on the atom list) they univocally represent equivalence classes of formulas. Given the limited expressiveness of propositional logic, a few attempts to leverage DDs to SMT level have been presented in the literature. Unfortunately, these techniques still suffer from some limitations: most procedures are theory-specific; some produce theory DDs (T-DDs) which do not univocally represent T-valid formulas or T-inconsistent formulas; none of these techniques provably produces theory-canonical T-DDs, which (under given conditions on the T-atom list) univocally represent T-equivalence classes of formulas. Also, these procedures are not easy to implement, and very few implementations are actually available. In this paper, we present a novel very-general technique to leverage DDs to SMT level, which has several advantages: it is very easy to implement on top of an AllSMT solver and a DD package, which are used as blackboxes; it works for every form of DDs and every theory, or combination thereof, supported by the AllSMT solver; it produces theory-canonical T-DDs if the propositional DD is canonical. We have implemented a prototype tool for both T-OBDDs and T-SDDs on top of OBDD and SDD packages and the MathSAT SMT solver. Some preliminary empirical evaluation supports the effectiveness of the approach.