# Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 97 references that are in the map.
- First posted on arXiv 16 Sep 2023.

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

- [Categorical Reparameterization with Gumbel-Softmax](https://mlsanity.com/paper/1611.01144/) (2016)
- [Structured Prediction Energy Networks](https://mlsanity.com/paper/1511.06350/) (2015)
- [Distribution-Aware Sampling and Weighted Model Counting for SAT](https://mlsanity.com/paper/1404.2984/) (2014)
- [Taming the Curse of Dimensionality: Discrete Integration by Hashing and Optimization](https://mlsanity.com/paper/1302.6677/) (2013)
- [Solving Marginal MAP Exactly by Probabilistic Circuit Transformations](https://mlsanity.com/paper/2111.04833/) (2021)
- [A Scalable and Nearly Uniform Generator of SAT Witnesses](https://mlsanity.com/paper/1304.1584/) (2013)
- [Lost Relatives of the Gumbel Trick](https://mlsanity.com/paper/1706.04161/) (2017)
- [Maximum A Posteriori Inference in Sum-Product Networks](https://mlsanity.com/paper/1708.04846/) (2017)
- [Solving Marginal MAP Problems with NP Oracles and Parity Constraints](https://mlsanity.com/paper/1610.02591/) (2016)
- [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)
- [Variational Algorithms for Marginal MAP](https://mlsanity.com/paper/1302.6584/) (2013)
- [Robust Optimization for Tree-Structured Stochastic Network Design](https://mlsanity.com/paper/1612.00104/) (2016)
- [Deductive Optimization of Relational Data Storage](https://mlsanity.com/paper/1903.03229/) (2019)

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

- [Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits](https://mlsanity.com/paper/2503.01009/) (2025)

## Abstract (arXiv)

Satisfiability Modulo Counting (SMC) encompasses problems that require both symbolic decision-making and statistical reasoning. Its general formulation captures many real-world problems at the intersection of symbolic and statistical Artificial Intelligence. SMC searches for policy interventions to control probabilistic outcomes. Solving SMC is challenging because of its highly intractable nature(NPPP-complete), incorporating statistical inference and symbolic reasoning. Previous research on SMC solving lacks provable guarantees and/or suffers from sub-optimal empirical performance, especially when combinatorial constraints are present. We propose XOR-SMC, a polynomial algorithm with access to NP-oracles, to solve highly intractable SMC problems with constant approximation guarantees. XOR-SMC transforms the highly intractable SMC into satisfiability problems, by replacing the model counting in SMC with SAT formulae subject to randomized XOR constraints. Experiments on solving important SMC problems in AI for social good demonstrate that XOR-SMC finds solutions close to the true optimum, outperforming several baselines which struggle to find good approximations for the intractable model counting in SMC.