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.

通过使用 XOR-SMC，我们提出了一种多项式算法，用于解决高度棘手的 SMC 问题，该算法具有恒定近似保证，并通过将 SMC 中的模型计数替换为受随机 XOR 约束的 SAT 公式，将高度棘手的 SMC 转化为可满足性问题。我们在 AI 有益于社会的重要 SMC 问题的求解实验中展示了 XOR-SMC，它找到了接近真实最优解的解决方案，胜过了几个难以找到可靠逼近 SMC 中棘手模型计数的基线方法。

解决符号与统计人工智能集成的可证明保证下的可满足性模数计数