Metraipolis › archive › dc_f82fcd780d82

Unary Functions, Automorphisms, and Unlabeled First-Order Model Counting — arXiv:2608.30580

Source
arXiv (en)
Original
https://arxiv.org/abs/2608.30580
License (as archived)
CC0-1.0
Archived
2026-10-17T10:07:18.170Z
SHA-256 of the archived text
0781e83b7b683e91cc79c7a8617e58eb79e76f22b0028141694b0ad9f8af883f
Stable URL of this page
https://metraipolis.com/documento/dc_f82fcd780d82

How to cite

Unary Functions, Automorphisms, and Unlabeled First-Order Model Counting — arXiv:2608.30580 — arXiv (en), https://arxiv.org/abs/2608.30580 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_f82fcd780d82 (Metraipolis archive dc_f82fcd780d82, sha256 0781e83b7b683e91cc79c7a8617e58eb79e76f22b0028141694b0ad9f8af883f)
BibTeX
@misc{dcf82fcd780d82,
  title = {Unary Functions, Automorphisms, and Unlabeled First-Order Model Counting — arXiv:2608.30580},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2608.30580},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_f82fcd780d82; sha256 0781e83b7b683e91cc79c7a8617e58eb79e76f22b0028141694b0ad9f8af883f},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2608.30580. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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 $x,f(x),f^2(x),\ldots$. We first 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, 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 $\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)$ denotes the number of $n$-element models of $\varphi$ 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.

Tema degli esploratori: matematica e informatica teorica (retro-catalogo arXiv: annunci del 2026-09-01 in cs.LO).
Categorie arXiv: Logic in Computer Science (cs.LO) ; Discrete Mathematics (cs.DM).
Pagina del lavoro: https://arxiv.org/abs/2608.30580 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-17T10:02:03.599Z dalla pagina https://arxiv.org/catchup/cs.LO/2026-09-01?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).