Weighted Model Counting in FO2 with Cardinality Constraints and Counting Quantifiers: A Closed Form Formula
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.
Cite
Text
Malhotra and Serafini. "Weighted Model Counting in FO2 with Cardinality Constraints and Counting Quantifiers: A Closed Form Formula." AAAI Conference on Artificial Intelligence, 2022. doi:10.1609/AAAI.V36I5.20525Markdown
[Malhotra and Serafini. "Weighted Model Counting in FO2 with Cardinality Constraints and Counting Quantifiers: A Closed Form Formula." AAAI Conference on Artificial Intelligence, 2022.](https://mlanthology.org/aaai/2022/malhotra2022aaai-weighted/) doi:10.1609/AAAI.V36I5.20525BibTeX
@inproceedings{malhotra2022aaai-weighted,
title = {{Weighted Model Counting in FO2 with Cardinality Constraints and Counting Quantifiers: A Closed Form Formula}},
author = {Malhotra, Sagar and Serafini, Luciano},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2022},
pages = {5817-5824},
doi = {10.1609/AAAI.V36I5.20525},
url = {https://mlanthology.org/aaai/2022/malhotra2022aaai-weighted/}
}