arXiv:2605.03391cs.LOcs.AI2026-05

提出新算法,显著加速带计数和模计数的二元逻辑模型计数。

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

论文配图:A Fast Model Counting Algorithm for Two-Variable Logic with Counting and Modulo Counting Quantifiers
图 1 · 摘自论文原文
  • 直接处理保留计数量词的斯科特标准型,避免复杂约简。
  • 将数据复杂度从二次降低为线性,提升计算效率。
  • 首次证明模计数扩展片段可域提升,适合大规模推理场景。

加权一阶逻辑模型计数(WFOMC)是提升概率推断中的核心任务:要求对有限域上某个一阶句子的所有模型求加权和。已有研究识别出若干一阶逻辑的域可提升片段,即在域大小上多项式时间可解的语法类。其中,带计数量词的二元片段 $ℍ^2$ 是目前已知最丰富的可提升片段之一。然而,现有 $ℍ^2$ 算法通过多阶段约简消除计数量词,引入基数约束,导致域规模增大时产生显著实际开销。本文提出 IncrementalWFOMC3,一种针对 $ℍ^2$ 及其模计数扩展 $ℍ^2_{\text{mod}}$ 的提升式算法。该算法不依赖约简技术,直接在保留计数量词的斯科特标准型上进行推断。这一直接处理带来两个主要成果:首先,我们推导出 $ℍ^2$ 中 WFOMC 的更紧数据复杂度界,将多项式次数从二次降至线性;其次,证明 $ℍ^2_{\text{mod}}$ 是域可提升的,将可解性从 $ℍ^2$ 扩展至支持原生模计数的更强片段。最后,实证评估显示,IncrementalWFOMC3 在运行时间上相比现有 WFOMC 算法和最先进的命题模型计数器提升数个数量级,且具备更好可扩展性。

原文摘要 · Abstract (English)

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.

模型计数逻辑推理算法优化

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。