Weighted Model Counting in FO2 with Cardinality Constraints and Counting Quantifiers: A Closed Form Formula

TL;DR

This paper develops a closed-form formula for weighted model counting in FO2 with added constraints and quantifiers, expanding the class of problems that can be efficiently solved.

Contribution

It introduces lifted interpretations for WFOMC, extends closed-form formulas to include cardinality constraints and counting quantifiers, and broadens the scope of domain-liftable theories.

Findings

Closed-form formulas for WFOMC with additional constraints

Extension of domain-liftability to C2 quantifiers

Introduction of a new family of weight functions

Abstract

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.