← 研踪 PaperTrailarXiv:2608.30580 · v2
Unary Functions, Automorphisms, and Unlabeled First-Order Model Counting
首次提交 2026-08-31 18:53
版本更新 2026-11-04 17:49
雷达观测 2026-11-05 11:10
摘要
Every fixed first-order sentence $\varphi$ determines an enumerative sequence $n\mapsto \mathrm{FOMC}(\varphi,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 such as $x,f(x),f^2(x),\ldots$. We prove that, for every fixed sentence $\varphi\in \mathrm{C}^1_{=}[f]$ with one unary function and an arbitrary finite relational vocabulary, $\mathrm{FOMC}(\varphi,n)$ is computable in time polynomial in $n$. By contrast, either a second variable or a second unary function yields hardness: there is a fixed sentence in $\mathrm{FO}^2_{=}[f]$ whose model-counting function is $\#\mathrm{P}_1$-complete, and there is a fixed constant-free universal sentence in $\mathrm{FO}^1_{=}[f,g]$, using only unary predicates besides $f$ and $g$, with the same property. We also relate labeled and unlabeled enumeration exactly. For every relational sentence $\varphi$, we construct an extension $\varphi_{\mathrm{aut}}$ in which a unary function records an automorphism and $\mathrm{FOMC}(\varphi_{\mathrm{aut}},n)=n! \cdot \mathrm{UFOMC}(\varphi,n)$, where $\mathrm{UFOMC}(\varphi,n)$ counts the $n$-element models of $\varphi$ up to isomorphism. This gives a one-query exact reduction from unlabeled to labeled model counting at the same domain size. If $\varphi$ belongs to $\mathrm{FO}^k_{=}$, respectively $\mathrm{C}^k$, and its relational vocabulary has maximum arity $r$, eliminating the auxiliary function yields a single-query reduction to labeled model counting in $\mathrm{FO}^{\max\{k,r+1\}}_{=}$, respectively $\mathrm{C}^{\max\{k,r+1\}}$.
作者备注：fixed typos, 61 pages
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v2 · 2026-11-04 17:49 · 最新观测版本
Unary Functions, Automorphisms, and Unlabeled First-Order Model Counting
Every fixed first-order sentence $\varphi$ determines an enumerative sequence $n\mapsto \mathrm{FOMC}(\varphi,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 such as $x,f(x),f^2(x),\ldots$. We prove that, for every fixed sentence $\varphi\in \mathrm{C}^1_{=}[f]$ with one unary function and an arbitrary finite relational vocabulary, $\mathrm{FOMC}(\varphi,n)$ is computable in time polynomial in $n$. By contrast, either a second variable or a second unary function yields hardness: there is a fixed sentence in $\mathrm{FO}^2_{=}[f]$ whose model-counting function is $\#\mathrm{P}_1$-complete, and there is a fixed constant-free universal sentence in $\mathrm{FO}^1_{=}[f,g]$, using only unary predicates besides $f$ and $g$, with the same property. We also relate labeled and unlabeled enumeration exactly. For every relational sentence $\varphi$, we construct an extension $\varphi_{\mathrm{aut}}$ in which a unary function records an automorphism and $\mathrm{FOMC}(\varphi_{\mathrm{aut}},n)=n! \cdot \mathrm{UFOMC}(\varphi,n)$, where $\mathrm{UFOMC}(\varphi,n)$ counts the $n$-element models of $\varphi$ up to isomorphism. This gives a one-query exact reduction from unlabeled to labeled model counting at the same domain size. If $\varphi$ belongs to $\mathrm{FO}^k_{=}$, respectively $\mathrm{C}^k$, and its relational vocabulary has maximum arity $r$, eliminating the auxiliary function yields a single-query reduction to labeled model counting in $\mathrm{FO}^{\max\{k,r+1\}}_{=}$, respectively $\mathrm{C}^{\max\{k,r+1\}}$.
查看此版本解读 →查看此版本原文 ↗