论文标题
加权模型在两个变量片段中计数具有基数约束：封闭式公式
Weighted Model Counting in the two variable fragment with Cardinality Constraints: A Closed Form Formula
论文作者
论文摘要
加权的一阶模型计数（WFOMC）计算给定有限域的一阶理论的加权总和。 WFOMC已成为概率推断的基本工具。在多项式时间W.R.T.运行的WFOMC的算法域大小称为提升推理算法。已经开发了针对FO2的多个扩展（具有两个变量的一阶逻辑的片段）的算法。我们介绍了解释作为制定WFOMC多项式的工具的概念。使用提升的解释，我们重建了FO2通用片段中多项式时间FOMC的闭合形式公式，Beame等人早些时候提出。然后，我们扩展了此封闭形式，以结合存在量化符和基数约束，而不会丢失域可容纳性。最后，我们表明，所获得的封闭形式激励了重量家族的自然定义，严格比对称重量功能大。
Weighted First-Order Model Counting (WFOMC) computes the weighted sum of the models of a first-order theory on a given finite domain. WFOMC has emerged as a fundamental tool for probabilistic inference. Algorithms for WFOMC that run in polynomial time w.r.t. the domain size are called lifted inference algorithms. Such algorithms have been developed for multiple extensions of FO2(the fragment of first-order logic with two variables) for the special case of symmetric weight functions. We introduce the concept of lifted interpretations as a tool for formulating polynomials for WFOMC. Using lifted interpretations, we reconstruct the closed-form formula for polynomial-time FOMC in the universal fragment of FO2, earlier proposed by Beame et al. We then expand this closed-form to incorporate existential quantifiers and cardinality constraints without losing domain-liftability. Finally, we show that the obtained closed-form motivates a natural definition of a family of weight functions strictly larger than symmetric weight functions.
