A Fast Model Counting Algorithm for Two-Variable Logic with Counting and Modulo Counting Quantifiers

arXiv:2605.03391v1 Announce Type: cross
Abstract: Weighted first-order model counting (WFOMC) is a central task in lifted probabilistic inference: It asks for the weighted sum of all models of a first-order sentence over a finite domain. A long line of work has identified domain-liftable fragments of first-order logic, that is, syntactic classes for which WFOMC can be solved in time polynomial in the domain size. Among them, the two-variable fragment with counting quantifiers, $mathbfC^2$, is one of the most expressive known liftable fragments. Existing algorithms for $mathbfC^2$, however, establish tractability through multi-stage reductions that eliminate counting quantifiers via cardinality constraints, which introduces substantial practical overhead as the domain size grows. In this paper, we introduce IncrementalWFOMC3, a lifted algorithm for WFOMC on $mathbfC^2$ and its modulo counting extension, $mathbfC^2_textmod$. Instead of relying on reduction techniques, IncrementalWFOMC3 operates directly on a Scott normal form that retains counting quantifiers throughout inference. This direct treatment yields two main results. First, we derive a tighter data-complexity bound for WFOMC in $mathbfC^2$, reducing the degree of the polynomial from quadratic to linear in the counting parameters. Second, we prove that $mathbfC^2_textmod$ is domain-liftable, extending tractability from $mathbfC^2$ to a richer fragment with native modulo counting support. Finally, our empirical evaluation shows that IncrementalWFOMC3 delivers orders-of-magnitude runtime improvements and better scalability than both existing WFOMC algorithms and state-of-the-art propositional model counters.