Weighted Model Counting in FO2 with Cardinality Constraints and Counting Quantifiers: A Closed Form Formula
Keywords:Knowledge Representation And Reasoning (KRR), Machine Learning (ML), Reasoning Under Uncertainty (RU)
AbstractWeighted 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.
How to Cite
Malhotra, S., & Serafini, L. (2022). Weighted Model Counting in FO2 with Cardinality Constraints and Counting Quantifiers: A Closed Form Formula. Proceedings of the AAAI Conference on Artificial Intelligence, 36(5), 5817-5824. https://doi.org/10.1609/aaai.v36i5.20525
AAAI Technical Track on Knowledge Representation and Reasoning