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 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.

Many important AI tasks today involve both logic (like solving a puzzle) and probability (like making guesses). But solving problems that combine both is extremely challenging. A recently proposed framework for describing such problems, called Satisfiability Modulo Counting (SMC), helps bridge these two areas, but solving SMC problems exactly can be very slow.Current approaches to solving SMC problems exactly rely on gluing together two separate tools: one that handles logic and another that handles probability. These tools must repeatedly interact, which consumes significant time and computing power.In our work, we introduce KOCO-SMC, a new algorithm that unifies logic and probability solving into a single tool. KOCO-SMC can make in-time decisions about whether to skip unpromising attempts early, using only partial information.We tested KOCO-SMC on large-scale synthetic datasets and real-world problems, and found that it solves them both exactly and much faster than existing methods. This demonstrates that it’s possible to achieve both accuracy and efficiency when tackling some of the most complex AI challenges.