Weighted First-Order Model Counting in the Two-Variable Fragment With Counting Quantifiers

TL;DR

This paper extends the polynomial-time solution for weighted first-order model counting from the two-variable fragment to include counting quantifiers, broadening the scope of efficient reasoning in logical models.

Contribution

It introduces a method to perform WFOMC efficiently in the two-variable fragment with counting quantifiers, expanding previous results.

Findings

WFOMC in the two-variable fragment with counting quantifiers is solvable in polynomial time

Extension of previous polynomial-time results to more expressive logical fragments

Broader applicability of efficient model counting in logical reasoning

Abstract

It is known due to the work of Van den Broeck et al [KR, 2014] that weighted first-order model counting (WFOMC) in the two-variable fragment of first-order logic can be solved in time polynomial in the number of domain elements. In this paper we extend this result to the two-variable fragment with counting quantifiers.