发表机构
Faculty of Electrical Engineering, Czech Technical University in Prague（布拉格捷克理工大学电气工程学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该文研究含一元函数的一阶逻辑模型计数复杂性，证明含1个一元函数的C¹₌[f]模型计数可多项式时间计算，含2个变量或2个一元函数时为#P₁-完全，还建立了无标签与有标签模型计数的精确归约关系。
AI 中文摘要
每个固定的一阶句子φ确定一个枚举序列n↦FOMC(φ,n)，其统计该句子在有标签域[n]上的模型数量。我们研究当逻辑规范使用真正的一元函数符号（从而包含嵌套项x,f(x),f²(x),…）时这些序列的复杂性。首先证明，对于每个固定句子φ∈C¹₌[f]（含1个一元函数和任意有限关系词汇），FOMC(φ,n)可在n的多项式时间内计算。相比之下，允许第二个变量或第二个一元函数已会导致难解性：无量词时，FO²₌[f]中存在一个固定句子，其模型计数函数为#P₁-完全；含1个变量和2个一元函数时，FO¹₌[f,g]中存在一个无常数的全称固定句子（除f、g外仅用一元谓词），其模型计数函数同样为#P₁-完全。我们还精确关联有标签与无标签枚举：对每个关系句子φ，构造扩展φ_aut，其中一元函数记录自同构，满足FOMC(φ_aut,n)=n!·UFOMC(φ,n)，这里UFOMC(φ,n)表示φ的n元模型的同构类数量，因此自同构标记实现了同域大小下从无标签到有标签模型计数的单查询精确归约。在最大元数不超过k（k≥2）的关系词汇上，消除辅助函数可实现从无标签FOᵏ₌和Cᵏ模型计数到有标签FOᵏ⁺¹₌和Cᵏ⁺¹模型计数的单查询归约。
英文摘要
Every fixed first-order sentence $φ$ determines an enumerative sequence $n\mapsto\mathrm{FOMC}(φ,n)$, counting its models on the labeled domain $[n]$. We study the complexity of these sequences when logical specifications may use genuine unary function symbols and hence nested terms $x,f(x),f^2(x),\ldots$. We first prove that, for every fixed sentence $φ\in\mathrm{C}^1_{=}[f]$, with one unary function and an arbitrary finite relational vocabulary, $\mathrm{FOMC}(φ,n)$ is computable in time polynomial in $n$. By contrast, permitting either a second variable or a second unary function already yields hardness. Without counting quantifiers, there is a fixed sentence in $\mathrm{FO}^2_{=}[f]$ whose model-counting function is $\#\mathrm{P}_1$-complete. With one variable and two unary functions, there is a fixed constant-free universal sentence in $\mathrm{FO}^1_{=}[f,g]$, using only unary predicates besides $f$ and $g$, whose model-counting function is again $\#\mathrm{P}_1$-complete. We also relate labeled and unlabeled enumeration exactly. For every relational sentence $φ$, we construct an extension $φ_{\mathrm{aut}}$ in which a unary function records an automorphism and $\mathrm{FOMC}(φ_{\mathrm{aut}},n)=n!\cdot\mathrm{UFOMC}(φ,n)$, where $\mathrm{UFOMC}(φ,n)$ denotes the number of $n$-element models of $φ$ up to isomorphism. Thus automorphism marking gives a one-query exact reduction from unlabeled to labeled model counting at the same domain size. Over relational vocabularies of maximum arity at most $k$, where $k\geq2$, eliminating the auxiliary function yields single-query reductions from unlabeled $\mathrm{FO}^k_{=}$ and $\mathrm{C}^k$ model counting to labeled $\mathrm{FO}^{k+1}_{=}$ and $\mathrm{C}^{k+1}$ model counting, respectively.
Comments61 pages
