# Top-Down Knowledge Compilation for Counting Modulo Theories

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 39 references that are in the map.
- First posted on arXiv 7 Jun 2023.

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

- [On The Reasons Behind Decisions](https://mlsanity.com/paper/2002.09284/) (2020)
- [Probabilistic Inference Modulo Theories](https://mlsanity.com/paper/1605.08367/) (2016)

## 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)
- [Canonical Decision Diagrams Modulo Theories](https://mlsanity.com/paper/2404.16455/) (2024)

## Abstract (arXiv)

Propositional model counting (#SAT) can be solved efficiently when the input formula is in deterministic decomposable negation normal form (d-DNNF). Translating an arbitrary formula into a representation that allows inference tasks, such as counting, to be performed efficiently, is called knowledge compilation. Top-down knowledge compilation is a state-of-the-art technique for solving #SAT problems that leverages the traces of exhaustive DPLL search to obtain d-DNNF representations. While knowledge compilation is well studied for propositional approaches, knowledge compilation for the (quantifier free) counting modulo theory setting (#SMT) has been studied to a much lesser degree. In this paper, we discuss compilation strategies for #SMT. We specifically advocate for a top-down compiler based on the traces of exhaustive DPLL(T) search.