Unary Functions, Automorphisms, and Unlabeled First-Order Model Counting
2026-08-31 • Logic in Computer Science
Logic in Computer ScienceDiscrete Mathematics
AI summaryⓘ
The authors study how hard it is to count the number of ways a logical sentence with unary functions can be true on a set of size n. They show that if the sentence uses just one variable and one unary function, counting models can be done efficiently (in polynomial time). But if you add even one more variable or function, counting becomes computationally hard (specifically, #P_1-complete). They also find a neat way to connect counting models that are labeled versus those that are unlabeled using automorphisms, essentially transforming one problem into the other. This linking allows translating results between these two types of counting problems for more complex logical formulas as well.
first-order logicunary function symbolmodel counting#P_1-completenesslabeled vs unlabeled modelsautomorphismpolynomial-time computabilityFO^kC^kisomorphism
Authors
Ondřej Kuželka
Abstract
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.