Solving Satisfiability Modulo Counting Problems in Computational Sustainability with Guarantees

Many real-world problems in computational sustainability require tight integrations of symbolic and statistical AI. Interestingly, Satisfiability Modulo Counting (SMC) captures a wide variety of such problems. SMC searches for policy interventions to control probabilistic outcomes. Solving SMC is challenging because of its highly intractable nature ($NP^{PP}$-complete), incorporating statistical inference andsymbolic 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, replacing the model counting in SMC with SAT formulae subject to randomized XOR constraints. Experiments on solving important SMC problems in computational sustainability 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.