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

TL;DR

This paper introduces IncrementalWFOMC3, a direct, efficient algorithm for weighted first-order model counting in two-variable logic with counting and modulo counting quantifiers, improving scalability and complexity bounds.

Contribution

It presents a novel direct inference algorithm for $ ext{C}^2$ and $ ext{C}^2_{ ext{mod}}$, reducing complexity and extending domain-liftability to richer logic fragments.

Findings

Tighter data-complexity bound with linear polynomial degree.

Proves domain-liftability of $ ext{C}^2_{ ext{mod}}$.

Achieves orders-of-magnitude runtime improvements over existing methods.

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, $\mathbf{C}^2$, is one of the most expressive known liftable fragments. Existing algorithms for $\mathbf{C}^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 $\mathbf{C}^2$ and its modulo counting extension, $\mathbf{C}^2_{\text{mod}}$. 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 $\mathbf{C}^2$, reducing the degree of the polynomial from quadratic to linear in the counting parameters. Second, we prove that $\mathbf{C}^2_{\text{mod}}$ is domain-liftable, extending tractability from $\mathbf{C}^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.