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.

翻译：含计数可满足性问题（SMC）涵盖了需要符号决策与统计推理相结合的问题。其通用形式刻画了符号与统计人工智能交叉领域中的诸多实际应用。SMC旨在寻找控制概率结果的策略干预方案。由于SMC具有高度难解性（$\text{NP}^{\text{PP}}$-完全），且需整合统计推断与符号推理，对其求解极具挑战性。现有SMC求解研究或缺乏可证明保证，或在实践中表现欠佳，尤其当涉及组合约束时。本文提出XOR-SMC——一种可调用NP预言机的多项式算法，用于求解具有常数近似保证的高度难解SMC问题。XOR-SMC通过将SMC中的模型计数替换为受随机XOR约束的SAT公式，将高度难解的SMC转化为可满足性问题。在面向社会公益的人工智能重要SMC问题上的实验表明，XOR-SMC能够找到接近真实最优解的方案，其性能优于多个难以对SMC中难解模型计数进行良好近似的基线方法。