PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Ondřej Kuželka

arXiv:2608.30580v1cs.LOcs.DM

TL;DR

The paper studies model-counting complexity for first-order specifications with genuine unary functions and the relationship between labeled and unlabeled enumeration. It proves polynomial-time counting in the one-variable, one-function setting, hardness when adding a second variable or function, and exact automorphism-marking reductions from unlabeled to labeled counting.

  • Problem

    The paper asks how extending relational model-counting frameworks with genuine unary functions and nested terms affects the complexity of enumerative sequences.

  • Method

    The paper analyzes functional-digraph decompositions for tractability, constructs computation tableaux for hardness, and uses unary functions or binary relations to encode automorphisms.

  • Results

    Fixed one-variable, one-function specifications are computable in polynomial time, whereas adding a second variable or unary function yields #P1-complete model counting.

  • Takeaways & Limitations

    The one-variable, one-function boundary is sharp: bounded orbit views enable tractability, while two variables or two functions support computation tableaux.

  • Takeaways & Limitations

    The paper leaves open the accepting-path complexity of many natural unlabeled counting functions, including the number of unlabeled graphs.

Abstract

from arXiv · show

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.

1 Introduction

The paper studies exact model-counting complexity when first-order specifications use genuine unary functions and nested terms. It establishes a narrow tractable boundary, hardness beyond that boundary, and an exact connection between unlabeled and labeled enumeration.

  • Unary functions: Nested function terms let one-variable formulas compare nonadjacent points of a forward orbit, unlike relational encodings of functionality.This gives the one-variable language bounded access to orbit structure.
  • Tractability: Fixed sentences in C^1_=[f] with one unary function and arbitrary finite relational vocabularies have model counts computable in polynomial time in n.Each sentence can inspect only a bounded portion of any forward orbit.
  • Hardness boundary: Allowing a second variable yields a fixed FO^2_=[f] sentence whose model-counting function is #P1-complete, even without counting quantifiers.The result marks a sharp complexity increase beyond the one-variable setting.
  • Hardness boundary: Allowing a second unary function likewise yields a fixed constant-free universal FO^1_=[f,g] sentence using only unary predicates besides the functions, with #P1-complete model counting.The two hardness proofs encode the same fixed linear-time nondeterministic computation by different means.
  • Unlabeled enumeration: Automorphism marking transforms each unlabeled relational model into labeled models paired with automorphisms, giving FOMC(φ_aut,n)=n!·UFOMC(φ,n).The varying automorphism factor cancels because each isomorphism class contributes exactly n! marked pairs.
  • Unlabeled enumeration: Eliminating the auxiliary function gives one-query reductions from unlabeled FO^k_= and C^k counting to labeled FO^{k+1}_= and C^{k+1} counting, followed by exact division by n!.For unary relational vocabularies, the construction stays inside C^2 and yields polynomial-time unlabeled model counting for fixed C^1_= [f].

2 Background

The background defines labeled and unlabeled first-order model counting, the relevant logical fragments, and the unary-input complexity class #P1. It also explains the orbit–stabilizer identity underlying automorphism marking.

  • Logical fragments: FO^k uses at most k reusable variables, while C^k adds constant-bounded counting quantifiers; [f] denotes one unary function symbol.Equality is especially relevant for nested terms in one-variable functional logic.
  • Labeled versus unlabeled: UFOMC(φ,n) counts isomorphism classes of n-element models, unlike FOMC, which counts labeled structures.For graphs on three vertices, the labeled count is 8 while the unlabeled count is 4.
  • Complexity: The class #P1 contains unary-input functions counting accepting paths of nondeterministic polynomial-time machines, and every fixed first-order model-counting function belongs to it.The input is 1^n, so polynomial time is measured in the enumerative parameter n.
  • Automorphism marking: An n-element structure has n!/|Aut(B)| labeled copies, and marking each copy with one automorphism makes every isomorphism class contribute exactly n! pairs.This is the orbit–stabilizer identity used later in the exact reduction.

3 A Tractable One-Variable Fragment

The entire one-variable fragment with counting quantifiers and one genuine unary function admits polynomial-time exact model counting, despite nested terms carrying bounded orbit information. This tractability is narrow: adding a second variable or unary function yields hardness, while the result supports polynomial-time enumeration of several functional-graph structures.

  • Tractability result: Every fixed sentence in C1_=[f] over an arbitrary finite relational vocabulary has a model-counting algorithm polynomial in the domain size.The proof reduces arbitrary relational occurrences to finitely many unary orbit traces and then counts functional digraph components using finite profiles and generating functions.
  • Expressive power: Nested function terms let one-variable formulas compare nonadjacent points on a forward orbit, a capability unavailable when f is represented only by a functional binary relation.This gives the fragment genuine but bounded access to orbit structure.
  • Proof strategy: The algorithm summarizes bounded segments x, f(x), ..., f^d(x) by finitely many forward profiles and computes rooted-tree and cycle generating functions through degree n.Counting thresholds are truncated at fixed bounds, and the resulting coefficient operations remain polynomial-time.
  • Examples: FOMC(γ,n) counts endofunctions with exactly floor(n/3) directed 3-cycles, and equals n! r! 3^c c! n^r when n=3c+r.The remaining r vertices choose their images arbitrarily.
  • Examples: FOMC(φ_k,n) counts labeled two-coloured rooted forests of height at most k satisfying a local colouring rule on every root-directed path of length two.Theorem 1 gives a polynomial-time algorithm for this sequence for every fixed k.
  • Boundary: The tractability boundary is narrow: allowing a second variable gives hardness in FO2_=[f], while a second unary function gives hardness in FO1_=[f,g].The one-variable, one-function restriction is therefore essential to the theorem.

4 Unlabeled Counting

The paper converts unlabeled model counting into labeled counting by marking automorphisms with a unary function, then removes that function relationally while controlling variable width.

  • Automorphism marking: A unary function marking a permutation and requiring relation preservation makes models correspond exactly to pairs of structures and their automorphisms.The graph case illustrates this correspondence directly.
  • Automorphism marking: Each isomorphism class contributes exactly n! expanded labeled models, because its labeled copies and automorphism choices cancel the stabilizer factor.For a class with automorphism group size a, there are n!/a labeled copies and a choices per copy.
  • Automorphism marking: Therefore UFOMC(φ,n) is obtained from one FOMC(φaut,n) query at the same domain size followed by exact division by n!.The construction changes the counted objects rather than selecting canonical representatives.
  • Eliminating the function symbol: Relational elimination represents the permutation by a binary graph relation and introduces staged auxiliary relations that encode one argument transformation at a time.The auxiliary relations are uniquely determined, so they add no multiplicity.
  • Eliminating the function symbol: For vocabularies of maximum arity k≥2, the relational construction yields single-query reductions from unlabeled FOk and Ck counting to labeled FOk+1 and Ck+1 counting.The added axioms use at most k+1 variables, while source equality atoms and counting quantifiers are preserved.
  • Eliminating the function symbol: For unary relational vocabularies, the construction stays inside C2 because automorphism preservation is equivalent to preserving 1-types.This gives polynomial-time computation of UFOMC for every fixed C1 sentence over a unary vocabulary.

5 Hardness with a Second Variable or a Second Unary Function

The paper shows that either a second variable or a second unary function destroys the tractability boundary of one-variable, one-function logic, yielding #P1-complete model counting.

  • A Second Variable: Allowing a second variable already yields a fixed FO2=[f] sentence whose model-counting function is #P1-complete.The construction adapts a tableau simulation and uses unary-function successor shifts to express local constraints with two variables.
  • A Second Variable: Its hardness reduction uses a normalized machine whose branches have a fixed polynomial number of transitions and bounded tape usage on unary inputs.These bounds are built into the machine normalization used by the tableau.
  • A Second Variable: The two-variable construction encodes computation using a cyclic coordinate system, compiled block indices, tableau predicates, and local transition constraints.The function f moves within blocks, while cycle wraps advance the compiled block index.
  • A Second Variable: The equality-elimination argument establishes only weighted equality-free FO2[f] hardness with polynomially many interpolation queries, not unweighted fixed-weight hardness.The weights are part of the oracle input, and coefficient extraction requires varying the interpolation weight.
  • A Second Unary Function: With one variable and two unary functions, a fixed constant-free universal FO1=[f,g] sentence using only unary predicates besides the functions also has #P1-complete model counting.The proof first uses a finite family of functions, then encodes that family with two functions and divides out explicit multiplicities.
  • A Second Unary Function: The one-variable construction represents computation on distinguished odd cycles, while universal closure permits independent π-components and additional even cycles that must be inverted away.A unary permutation S supplies time points; separate corrections remove component and extra-cycle structure.

6 Discussion

The paper draws a sharp boundary around one-variable logic with one unary function: this setting is tractable, while either a second variable or a second unary function yields hardness. Automorphism marking provides an exact bridge from unlabeled to labeled counting, but does not itself solve unlabeled counting efficiently.

  • Complexity boundary: One variable with one unary function remains tractable because bounded orbit views and functional-graph decompositions support polynomial-time counting.The relevant structures decompose into cycles with rooted in-trees, while fixed sentences inspect only bounded forward-orbit portions.
  • Complexity boundary: A second variable already yields #P1-complete counting without counting quantifiers.The two-variable encoding uses variables for time and tape position in a computation tableau.
  • Complexity boundary: A second unary function likewise yields #P1-complete counting in one-variable logic.The two-function construction represents time directly and recovers tape information through previous-visit functions, with a constant-factor domain expansion.
  • Labeled and unlabeled counting: Automorphism marking expresses the correction for isomorphism classes inside the logical specification, rather than by naively dividing arbitrary labeled counts by n!.For relational sentences, the marked count equals n! times the unlabeled count; eliminating the function requires one additional variable.
  • Labeled and unlabeled counting: The reduction from unlabeled to labeled counting is an oracle reduction, not a canonical-form construction, and open questions remain about directly polynomial-time unlabeled counting.The paper also notes that larger-fragment complexity may depend on function-term nesting and relation-atom occurrences.
  • Scope: The proofs establish ordinary model-counting results; extending the same ideas to symmetric weighted counting requires additional bookkeeping and is not pursued.

7 Related Work

The paper extends prior relational tractability and hardness results to genuine unary functions, using nested terms for local tableau updates and automorphism marking for a general labeled–unlabeled bridge.

  • Relational tractability: Earlier lifted-inference work established polynomial-time data complexity for weighted model counting of fixed relational FO2 sentences.
  • Relational tractability: Prior relational results covered functionality constraints, arbitrary-arity one-dimensional fragments, counting quantifiers, semantic axioms, linear orders, and graph-polynomial methods.
  • Unary functions: This paper proves exact unweighted counting for full one-variable counting logic C1=[f], including genuinely nested unary-function terms and arbitrary relation arities.
  • Hardness constructions: The FO2=[f] hardness proof adapts tableau encoding by using unary-function terms to express successor shifts with two variables.The related relational FO3 construction is also associated with an n! labeling factor that disappears under isomorphism quotienting.
  • Hardness constructions: The two-function proof draws on a history construction in which previous-visit information recovers the symbol read at a tape cell.
  • Labeled and unlabeled counting: Automorphism-marked extensions provide a uniform logical mechanism connecting quotient enumeration with fixed-sentence labeled model counting.For relational vocabularies of arity at most k, the resulting reductions increase the variable width by one.

8 Proofs

The proof section establishes the paper’s main theorems through a shared machine source and separate logical encodings, with bijectivity arguments collected separately.

  • Proof organization: The proofs cover Theorems 1, 4, and 5, beginning with a fixed source machine used in both hardness constructions.
  • Proof organization: The two hardness encodings are proved separately, while statements and proofs concerning bijectivity are collected in Appendix A.

8.1 Proof of the One-Variable Tractability Theorem

The one-variable tractability proof combines bounded forward-orbit profiles with finite-state generating-function calculations, then removes the unary-relation restriction while preserving polynomial-time exact enumeration.

  • Proof strategy: The proof first handles unary relation symbols and one unary function, then removes the relation-arity restriction to complete the theorem.
  • Proof strategy: The unary-relation case yields a model-counting function computable in polynomial time in the domain size.
  • Generating functions: Finite monoid algebras carry capped cardinality summaries through labeled product and set constructions.The algebra records finitely many capped counts, while formal power series encode labeled structures by size.
  • Profiles: A d-profile is a complete satisfiable quantifier-free description of the bounded forward segment x, f(x), …, f^d(x).Profiles record predicate types at each segment position and equalities between iterated function terms.
  • Generating functions: The capped-cardinality and tree-series lemmas reduce accepted model counting to finitely many coefficient computations.The relevant profile and monoid sets depend only on the fixed sentence.
  • Functional graphs: Cycle constructions account for origin choices and cyclic orientations when counting decorated functional-graph components.
  • Complexity bound: For fixed sentence parameters, coefficient vectors have polynomial bit length and all truncated series operations require polynomially many arithmetic operations.The proof bounds the relevant profile-decorated objects and concludes polynomial-time computation in the bit model.
  • Arbitrary relation arities: Higher-arity relation symbols are eliminated by canonical unary encodings, with fixed-depth translations and exact multiplicity corrections.The correction terms cancel constrained tuple bits, and exact division remains polynomial-time because exponents and bit lengths are polynomially bounded.

8.2 A Common Source Machine for the Hardness Proofs

The hardness proofs normalize one fixed unary-input nondeterministic machine so every computation branch has the same linear length and bounded tape usage. This preserves accepting branches exactly while making the machine suitable for tableau encodings.

  • Tape normalization: The machine uses a marked-left-end convention that preserves endpoint markers and forbids left moves while scanning them.This makes the semi-infinite tape boundary explicit in the transition system.
  • Complexity role: The normalized machine computes a #P1-hard accepting-branch function on unary inputs.For input 1n, accU(n) counts accepting branches, and the normalization retains this counting problem.
  • Branch normalization: A fixed machine U is constructed whose branches all have exactly (p + 2)n − 1 transitions.Preprocessing, simulation delays, and deterministic padding equalize branch lengths without introducing nondeterministic choices.
  • Branch normalization: Every branch of U corresponds to exactly one branch of the original machine U0 with the same acceptance status.The construction copies the unary input, simulates U0, records its outcome, and enters qacc exactly when the simulated branch accepts.
  • Tape normalization: Because each head moves at most one cell per transition, a fixed b ≥ max{a + 2, 3} bounds every head within the first bn cells.The bound follows from the uniform branch length and is used to obtain a finite tape-space representation.

8.3 Proof of the Two-Variable Hardness Theorem

The two-variable hardness proof encodes normalized machine computations on a cyclic successor structure. It proves that the resulting FO2=[f] tableau has exactly one model per accepting branch, apart from the n! choices of cyclic order.

  • Ordered cyclic successor: The FO2=[f] construction adapts a standard tableau encoding by forcing f to be a cyclic successor.Nested successor terms provide direct access to time and tape-coordinate shifts while all formulas use only x and y.
  • Ordered cyclic successor: Every finite nonempty model of CycSucc induces a strict linear order with named minimum and maximum, and f is its cyclic successor.The order and successor properties follow from the finite axioms without explicitly requiring transitivity.
  • Counting multiplicity: On [n], CycSucc has exactly n! models because choosing the linear order forces Min, Max, and f.This factorial multiplicity is later divided out in the hardness reduction.
  • Tableau encoding: The coordinate compilation represents states, selected transitions, tape labels, head markers, and local successor updates in a fixed FO2=[f] sentence.The finite schemes cover every time and tape coordinate, including block boundaries and endpoints, for every n ≥ 1.
  • Correctness and counting: The local simulation clauses hold exactly when the selected rule is enabled and the successor configuration results from applying it.Together with the final acceptance condition, this makes tableau interpretations correspond to accepting computation branches.
  • Correctness and counting: An oracle query to the model-counting function followed by exact division by n! computes accU(n), proving #P1-completeness.Membership in #P1 holds for every fixed first-order sentence, while the reduction supplies hardness.

8.4 Proof of the Two-Function Hardness Theorem

The two-function hardness proof uses a structured root cycle as a one-variable computational timeline. Unary predicates and functions enforce the timeline, prepare the unary input, simulate the machine, and establish a branch-to-model correspondence.

  • Structural encoding: Parity separation makes every root cycle odd and every satellite even, with a unique E-coloring on roots and two possible colorings on satellites.Alternation along S-edges enforces the parity distinction.
  • Structural encoding: A root cycle is isolated inside each π-component using active points and the squaring relation between d and S.Odd root cycles and even satellite cycles have incompatible cycle structures under squaring, forcing satellites to be inactive.
  • Timeline construction: For root lengths 4N + 1, h identifies canonical quarter- and half-cycle points, allowing the cycle to be cut into a linear interval.The identities q1 = S^N(c), q2 = S^2N(c), and b = S^4N(c) provide internal markers.
  • Timeline construction: The root is partitioned into build, rewind, and machine phases with lengths an, an, and 2an transitions.The enlarged root cycle therefore acts as the complete computational timeline.
  • Input preparation: The build and rewind phases deterministically prepare the input configuration for V on 1n, returning the input head to the marked first cell at q2.The preparation preserves the required blank work tapes and marked left endpoints.
  • Machine simulation: During the machine phase, selected transition predicates determine the machine actions, while read-consistency clauses verify that scanned symbols match prior writes.The construction uses previous-visit functions to connect current reads with the relevant earlier tape history.

8.4.4 Nearest-neighbour history in one variable

The nearest-neighbour construction stores enough unary-function history to reconstruct tape movement and contents without representing tape positions as domain elements. These histories are uniquely determined and support a bijection between computational expansions and accepting branches.

  • Previous-visit representation: Previous-visit pointers record the latest earlier visits to the cells immediately left and right of the current head.This replaces explicit tape-position elements with unary functions on time points.
  • One-variable verification: The construction enforces legal semi-infinite tape histories by preventing movement left of the first cell, matching the marked-left-end machine normalization.The logical boundary condition agrees with the source machine’s transition restriction.
  • Pointer recurrence: Nearest-neighbour recurrences update the pointers from the head’s current move, including nested lookups for newly adjacent cells.Right, left, and stay moves have separate recurrence behavior, with undefined pointers represented by a dummy value.
  • Pointer recurrence: The dummy-value convention totalizes partial previous-visit pointers by mapping an undefined pointer to the current time.This makes the semantic partial maps representable by total unary function symbols.
  • One-variable verification: All nested pointer lookups use one variable, and induction along the root interval uniquely determines the pointer functions from the head-movement sequence.The predicate Rτ is then uniquely determined by whether the right pointer is genuine.
  • Branch correspondence: For a root of size 4an + 1, computational expansions are in bijection with accepting branches of U on input 1n.The deterministic preparation, transition choices, pointer recurrences, and read clauses together yield the correspondence.

8.4.5 Exact root count

The section defines R_r as the count of one-component models whose entire domain is an active root cycle, then establishes an exact formula for R_m at m = 4an + 1.

  • R_r counts labeled Θ-models on r elements consisting of one π-component with no satellites, equivalently with the whole domain as the active root cycle.
  • At m = 4an + 1, Proposition 2 gives an exact root-count formula for R_m.The proposition applies for every n ≥ 1.
  • The count is obtained by choosing a directed m-cycle, its component root, and the uniquely forced structural predicates and functions.There are (m − 1)! directed m-cycles, m choices of root, and the remaining structure is uniquely determined before computational expansions are counted.
  • The next step recovers R_m despite Θ allowing arbitrary sets of components and even satellite cycles within components.

8.4.6 Two exact inversions

The section performs two exact inversions: first extracting one-component counts from all-model counts, then removing satellite cycles to recover active-root-cycle counts.

  • SET inversion across components: K_1, …, K_ℓ, the counts of models with exactly one π-component, are recovered sequentially from M_1, …, M_ℓ.The recurrence isolates the component containing distinguished label 1 and subtracts contributions from smaller components.
  • SET inversion across components: Θ decomposes into π-components because its functions preserve components, and universal one-variable clauses remain valid under restriction and disjoint union.This specific SET structure makes one-component models combine uniquely into arbitrary labeled models.
  • Removing the satellites: Satellite structures occupy an even number of labels and are determined by even-length cycles of S together with alternating E-assignments.There are no satellite structures on an odd number of labels.
  • Removing the satellites: The satellite count is evaluated by summing over permutation cycle types, with two alternating E-assignments for each satellite cycle.The cycle-type sum reduces to a factorial expression involving all permutations of the satellite labels.
  • Removing the satellites: R_ℓ is recovered from K_ℓ by comparing the identities for ℓ and ℓ − 2, which differ only in the final root term.

8.4.7 Exact compression to two unary functions

The section compresses a fixed finite family of unary functions into two while preserving model counts up to an explicit multiplicity, then uses this construction in the hardness reduction.

  • A fixed finite family of unary functions can be compressed to two functions while preserving model counts up to an explicit multiplier.
  • The construction partitions the target domain into r labeled layers and uses f to cycle between layers while g encodes all source functions.Source predicates are restricted to the base layer L_0.
  • No additional first-order variables are introduced, so the translated sentence remains in FO^1.Nested source terms are translated recursively through layer-dependent abbreviations.
  • Once the layer predicates and f are fixed, choosing the source functions on L_0 is equivalent to choosing a layer-preserving g.
  • The exact multiplicity combines ordered layer partitions, f-skeletons, and FOMC(Ψ,q), with zero count when r does not divide the target size.Equal layer sizes are necessary for the construction.

A Bijectivity and the Permutation Axiom

The section shows that one-variable formulas with unary predicates cannot define bijectivity internally, while polynomial-time counting remains possible under an external permutation axiom.

  • Internal bijectivity: There is no finite unary-predicate certificate that makes a fixed C^1_=[f] sentence equivalent to bijectivity for every finite endofunction.This is Proposition 3, the section’s central limitation result.
  • Internal bijectivity: The impossibility follows by rewiring a long directed cycle into a non-bijective function while preserving every bounded-depth unary profile and equality test.The rewired function has a transient path feeding into a cycle, yet agrees on all relevant d-profiles.
  • Internal bijectivity: The original and rewired structures satisfy the same one-variable sentence, although the rewired function is not bijective.
  • The permutation axiom: Bijectivity can instead be imposed externally by PERM(f), which uses two variables and is therefore outside C^1_=[f].On finite domains, PERM(f) says exactly that f is a permutation.
  • The permutation axiom: With this external axiom, FOMC(PERM(f) ∧ φ,n) is computable in polynomial time for every fixed φ ∈ C^1_=[f].The proof first handles unary relations using cycle-only generating functions, then applies monadic trace compression for arbitrary arities.
  • The permutation axiom: The monadic coefficient calculation supplies the base case, while arbitrary relation arities use a correction factor independent of the chosen bijection.Nullary relations are handled by enumerating their finitely many truth assignments.
  • The permutation axiom: C^1_=[f] can nevertheless define restricted permutation classes, such as permutations whose cycle lengths all divide a fixed q.
Loading 2608.30580v1…