提出高效精确求解计数模逻辑问题的新方法
Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
- 将概率推断与布尔求解融合，动态追踪上下界
- 仅需部分变量赋值即可早期估计，显著提速
- 在真实数据上比现有方法快数倍，适合精准推理场景
可满足性模计数（SMC）是一种新兴的统一语言，用于整合统计与符号人工智能的问题。SMC 问题是扩展的布尔可满足性问题，其中少数布尔变量的真值由概率推断决定。近似求解器可能返回违反约束的解；直接结合现有的 SAT 求解器与概率推断求解器虽能获得精确解，但因频繁往返调用两者导致性能缓慢。本文提出 KOCO-SMC，一种集成式精确 SMC 求解器，能在概率推断过程中高效跟踪下界和上界。该方法通过仅依赖部分变量赋值即可实现概率推断的早期估计，而现有方法需完整赋值。实验中，我们在大规模数据集和真实应用场景上对比了 KOCO-SMC 与当前可用的近似及精确 SMC 求解器。结果表明，所提方法以更少时间找到精确解。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。