Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
This work addresses efficiency issues in exact SMC solving for researchers and practitioners in statistical and symbolic AI, though it is incremental as it builds on existing SMC frameworks.
The paper tackles the problem of slow exact solutions in Satisfiability Modulo Counting (SMC) by proposing KOCO-SMC, an integrated solver that uses partial variable assignments to track bounds, resulting in significantly faster exact solutions compared to existing methods.
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 truth values of a few Boolean variables are determined by probabilistic inference. Approximate solvers may return solutions that violate constraints. Directly integrating available SAT solvers and probabilistic inference solvers gives exact solutions but results in slow performance because of many back-and-forth invocations of both solvers. We propose KOCO-SMC, an integrated exact SMC solver that efficiently tracks lower and upper bounds in the probabilistic inference process. It enhances computational efficiency by enabling early estimation of probabilistic inference using only partial variable assignments, whereas existing methods require full variable assignments. In the experiment, we compare KOCO-SMC with currently available approximate and exact SMC solvers on large-scale datasets and real-world applications. The proposed KOCO-SMC finds exact solutions with much less time.