Unary Functions, Automorphisms, and Unlabeled First-Order Model Counting

Abstract

Every fixed first-order sentence $\phi$ determines an enumerative sequence $n\mapsto \mathrm{FOMC}(\phi ,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),\dots$. We first prove that, for every fixed sentence $\phi \in {\mathrm{C}}_{=}^1[f]$, with one unary function and an arbitrary finite relational vocabulary, $\mathrm{FOMC}(\phi ,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 $\phi$, we construct an extension ${\phi }_{\mathrm{aut}}$ in which a unary function records an automorphism and $\mathrm{FOMC}({\phi }_{\mathrm{aut}},n)=n!\cdot \mathrm{UFOMC}(\phi ,n)$, where $\mathrm{UFOMC}(\phi ,n)$ denotes the number of $n$-element models of $\phi$ 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\ge 2$, 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.

61 pages