A Combinatorial Approach to Weighted Model Counting in the Two-Variable Fragment with Cardinality Constraints

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. In this paper, we reconstruct the closed-form formula for polynomial-time First Order Model Counting (FOMC) in the universally quantified fragment of FO2, earlier proposed by Beame et al.. We then expand this closed-form to incorporate cardinality constraints and existential quantifiers. Our approach requires a constant time (w.r.t the previous linear time result) for handling equality and allows us to handle cardinality constraints in a completely combinatorial fashion. Finally, we show that the obtained closed-form motivates a natural definition of a family of weight functions strictly larger than symmetric weight functions.