Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees
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.
Code (1)
Tasks
Decision MakingSimilar Papers 제목 키워드 기반
Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Satisfiability Modulo Counting (SMC) is a recently proposed general language to reason about problems integrating statistical and symbolic Artificial Intelligence. An SMC problem is an extended SAT problem in which the t…
Computational EfficiencyNeurosymbolic Language Reasoning as Satisfiability Modulo Theory
Natural language understanding requires interleaving textual and logical reasoning, yet large language models often fail to perform such reasoning reliably. Existing neurosymbolic systems combine LLMs with solvers but re…
Natural Language UnderstandingLogical ReasoningProgram SynthesisCSB: A Counting and Sampling tool for Bit-vectors
Satisfiability modulo theory (SMT) solvers have significantly advanced automated reasoning due to their effectiveness in solving problems across various fields. With the advancement in SMT solvers, there is growing inter…
Satisfiability and Synthesis Modulo Oracles
In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification) phase. Many synthesis algorithms use a w…
Program SynthesisA Tool for Computing and Estimating the Volume of the Solution Space of SMT(LA)
There are already quite a few tools for solving the Satisfiability Modulo Theories (SMT) problems. In this paper, we present \texttt{VolCE}, a tool for counting the solutions of SMT constraints, or in other words, for co…