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

TL;DR

This work addresses the intractable problem of solving Satisfiability Modulo Counting (SMC), which lies at the crossroads of symbolic and probabilistic AI and is $NP^{PP}$-complete. It introduces XOR-SMC, a polynomial-time approach with access to NP-oracles that achieves constant-approximation guarantees by converting model counting into SAT via randomized XOR constraints, and provides a formal guarantee (Theorem th:xor-smc). The method is demonstrated on two AI-for-social-good problems: emergency shelter placement and robust supply chain design, where XOR-SMC outperforms baselines in both solution quality and running time. The results suggest that transforming counting-based reasoning into SAT with randomized constraints extends the reach of SAT solvers to highly intractable SMC problems, enabling provable, scalable policy-aware decision making in safety-critical domains.

Abstract

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($\text{NP}^{\text{PP}}$-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.

Figures (5)

• Figure 1: Our $\mathtt{XOR}$-$\mathtt{SMC}$ (shown in Algorithm \ref{['alg:xor-smc']}) solves the intractable model counting with satisfiability problems subject to randomized XOR constraints and obtains constant approximation guarantees for SMC.
• Figure 2: Example assignment of shelters that guarantee sufficient alternative paths from the resident areas, at Hawaii Island. Every orange dot corresponds to shelters and the green dot indicates a resident area.
• Figure 3: $\mathtt{XOR}$-$\mathtt{SMC}$ finds better shelter locations with orders of magnitudes more paths from the resident area to the chosen shelters than competing baselines across different graphs (y-axis in log scale).
• Figure 4: Example of the supply chain design application. (a) The initial supply chain where nodes 1 and 2 are suppliers of wheat; nodes 3 and 4 are producers of bread; nodes 5 and 6 are markets. (b) Graph after trade (edge) selection of each demander. (c) Under the effect of random events, e.g., natural disasters, some trades (edges) are disabled.
• Figure 5: Example of the bread production supply chain network from zokaee2017robust. The example includes 3 wheat suppliers, 2 flour factories, 2 bread factories, and 2 markets. A black solid arrow from $i$ to $j$ indicates a trade between them ($x_{i,j}=1$ in the trading plan), and a dashed arrow from $p$ to $q$ represents an unchosen trade ($x_{p,q}=0$). Each edge also incorporates a cost and capacity which are not shown in the figure. The red cross indicates the edge is destroyed due to stochastic events (with a probability specified by ${Pr}(\boldsymbol{\theta})$).

Theorems & Definitions (3)

• Lemma 1
• Theorem 2
• proof