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.

翻译：加权一阶模型计数（WFOMC）是提升式概率推理中的核心任务：它要求在有限域上计算一阶语句所有模型的加权和。已有大量工作识别出可域提升的一阶逻辑片段，即可以在域大小多项式时间内求解WFOMC的语法类。其中，带计数量词的两变元片段 $\mathbf{C}^2$ 是已知最具表达力的可提升片段之一。然而，现有面向 $\mathbf{C}^2$ 的算法通过多阶段归约来建立可处理性——这些归约通过基数约束消除计数量词，随着域规模增长会引入显著的实际开销。本文提出IncrementalWFOMC3，一种针对 $\mathbf{C}^2$ 及其模计数扩展 $\mathbf{C}^2_{\text{mod}}$ 的WFOMC提升式算法。与依赖归约技术不同，IncrementalWFOMC3直接在推理过程中保留计数量词的斯科伦范式上运行。这种直接处理方式带来两项主要结果。首先，我们推导出 $\mathbf{C}^2$ 中WFOMC更紧的数据复杂度界，将多项式次数从计数参数的二次方降至线性。其次，我们证明 $\mathbf{C}^2_{\text{mod}}$ 是可域提升的，将可处理性从 $\mathbf{C}^2$ 扩展到具有原生模计数支持的更丰富片段。最终，实验评估表明，与现有WFOMC算法和最新命题模型计数器相比，IncrementalWFOMC3实现了数量级的运行时改进和更优的可扩展性。