Weighted First-Order Model Counting (WFOMC) computes the weighted sum of the models of a first-order logic theory on a given finite domain. First-Order Logic theories that admit polynomial-time WFOMC w.r.t domain cardinality are called domain liftable. We introduce the concept of lifted interpretations as a tool for formulating closed-forms for WFOMC. Using lifted interpretations, we reconstruct the closed-form formula for polynomial-time FOMC in the universally quantified fragment of FO2, earlier proposed by Beame et al. We then expand this closed-form to incorporate cardinality constraints, existential quantifiers, and counting quantifiers (a.k.a C2) 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.

本文介绍了一种新的 lifted interpretations 工具，用于重构 Beame et al. 提出的多项式时间 FOMC 的闭合式公式，并将其扩展以涵盖基数约束、存在量词和计数量词（C2），同时仍然保持 domain-liftability。最后，我们展示了所获得的闭合形式促进了一种权重函数家族的自然定义，严格大于对称权重函数。

带基数约束和计数量词的FO2加权模型计数：一个封闭式公式