# Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 60 references that are in the map.
- First posted on arXiv 2 Mar 2025.

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

- [Einsum Networks: Fast and Scalable Learning of Tractable Probabilistic Circuits](https://mlsanity.com/paper/2004.06231/) (2020)
- [The Model Counting Competition 2020](https://mlsanity.com/paper/2012.01323/) (2020)
- [ADDMC: Weighted Model Counting with Algebraic Decision Diagrams](https://mlsanity.com/paper/1907.05000/) (2019)
- [Neuro-symbolic Learning Yielding Logical Constraints](https://mlsanity.com/paper/2410.20957/) (2024)
- [Solving Marginal MAP Exactly by Probabilistic Circuit Transformations](https://mlsanity.com/paper/2111.04833/) (2021)
- [Probabilistic Model Counting with Short XORs](https://mlsanity.com/paper/1707.09467/) (2017)
- [Decomposition Bounds for Marginal MAP](https://mlsanity.com/paper/1511.02619/) (2015)
- [SharpSAT-TD in Model Counting Competitions 2021-2023](https://mlsanity.com/paper/2308.15819/) (2023)
- [Developing Multi-Agent Systems with Degrees of Neuro-Symbolic Integration [A Position Paper]](https://mlsanity.com/paper/2305.11534/) (2023)
- [Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees](https://mlsanity.com/paper/2309.08883/) (2023)

## Abstract (arXiv)

Satisfiability Modulo Counting (SMC) is a recently proposed general language to reason about problems integrating statistical and symbolic Artificial Intelligence. An SMC problem is an extended SAT problem in which the truth values of a few Boolean variables are determined by probabilistic inference. Approximate solvers may return solutions that violate constraints. Directly integrating available SAT solvers and probabilistic inference solvers gives exact solutions but results in slow performance because of many back-and-forth invocations of both solvers. We propose KOCO-SMC, an integrated exact SMC solver that efficiently tracks lower and upper bounds in the probabilistic inference process. It enhances computational efficiency by enabling early estimation of probabilistic inference using only partial variable assignments, whereas existing methods require full variable assignments. In the experiment, we compare KOCO-SMC with currently available approximate and exact SMC solvers on large-scale datasets and real-world applications. The proposed KOCO-SMC finds exact solutions with much less time.