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.

翻译：加权一阶计算模型(WFOMC) 计算了一个特定有限域第一阶理论模型模型的加权总和。 WFOMC 已成为概率推论的基本工具。 以多角度时间运行的WFOMC 的数值被称为解除推论算法。 这种算法是为对称加权函数特例的FO2( 第一阶逻辑的碎片和两个变量)的多重扩展而开发的。 我们引入了取消解释的概念,作为为WFOMC 制定多角度解释的工具。 我们利用取消的解释,在Beame等人先前提议的FO2的通用碎片中重建多角度时FOMC的封闭式公式。 然后我们扩大这种封闭式的公式,在不丧失可移动性的情况下纳入存在量定值和基点限制。 最后,我们表明,获得的封闭式为一个重量函数大家庭的自然定义,其重量功能严格大于对称重量函数的自然定义。