Weighted Model Counting in the two variable fragment with Cardinality Constraints: A Closed Form Formula
This work provides a theoretical advancement for probabilistic inference in AI, specifically for lifted inference algorithms, but it is incremental as it builds on prior closed-form results for the universal fragment.
The paper tackles the problem of weighted first-order model counting (WFOMC) in the two-variable fragment of first-order logic with cardinality constraints, by introducing lifted interpretations to derive a closed-form formula that extends domain-liftability to include existential quantifiers and cardinality constraints, resulting in a broader family of weight functions beyond symmetric ones.
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.