Weighted Model Counting in the two variable fragment with Cardinality Constraints: A Closed Form Formula

TL;DR

This paper derives a closed-form formula for weighted model counting in the two-variable fragment of first-order logic with cardinality constraints, extending domain-liftability to more general weight functions.

Contribution

It introduces lifted interpretations to formulate polynomials for WFOMC and extends the closed-form to include existential quantifiers and cardinality constraints.

Findings

Closed-form formula for WFOMC in FO2 with cardinality constraints

Extension of domain-liftability to broader weight functions

Reconstruction of earlier polynomial-time WFOMC results

Abstract

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.