关于加权模型积分在DNF结构上的逼近性
On the Approximability of Weighted Model Integration on DNF Structures
摘要：
加权模型计数（Weighted Model Counting，WMC）是计算一个命题公式的所有满足赋值的加权和。WMC是众所周知的是精确求解的#P-困难，但承认一个完全多项式随机逼近方案（FPRAS）时，限制到DNF结构。在这项工作中，我们研究加权模型集成，加权模型计数的推广，其中涉及到真实的变量，除了命题变量，并提出以下问题：是否加权模型集成DNF结构承认FPRAS？基于近似体积计算和近似加权模型计数的经典结果，我们证明了DNF结构上的加权模型积分确实可以近似为一类权重函数。我们的近似算法基于三个子程序，每个子程序都可以是弱（即，近似的），或强的（即，精确）Oracle，并且在所有情况下都有准确性保证。我们通过实验验证了我们的方法在不同大小的随机生成的DNF实例，并表明我们的算法可扩展到大型问题实例，涉及多达1 K个变量，这是目前现有的通用加权模型集成求解器无法达到的。
英文摘要：
Weighted model counting (WMC) consists of computing the weighted sum of all satisfying assignments of a propositional formula. WMC is well-known to be #P-hard for exact solving, but admits a fully polynomial randomized approximation scheme (FPRAS) when restricted to DNF structures. In this work, we study weighted model integration, a generalization of weighted model counting which involves real variables in addition to propositional variables, and pose the following question: Does weighted model integration on DNF structures admit an FPRAS? Building on classical results from approximate volume computation and approximate weighted model counting, we show that weighted model integration on DNF structures can indeed be approximated for a class of weight functions. Our approximation algorithm is based on three subroutines, each of which can be a weak (i.e., approximate), or a strong (i.e., exact) oracle, and in all cases, comes along with accuracy guarantees. We experimentally verify our approach over randomly generated DNF instances of varying sizes, and show that our algorithm scales to large problem instances, involving up to 1K variables, which are currently out of reach for existing, general-purpose weighted model integration solvers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
