Top

Theory of Computing Systems

Published in:

Open Access 13-07-2016

On Symmetric Circuits and Fixed-Point Logics

Authors: Matthew Anderson, Anuj Dawar

Published in: Theory of Computing Systems | Issue 3/2017

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Patentsearch

Off

Abstract

We study properties of relational structures, such as graphs, that are decided by families of Boolean circuits. Circuits that decide such properties are necessarily invariant to permutations of the elements of the input structures. We focus on families of circuits that are symmetric, i.e., circuits whose invariance is witnessed by automorphisms of the circuit induced by the permutation of the input structure. We show that the expressive power of such families is closely tied to definability in logic. In particular, we show that the queries defined on structures by uniform families of symmetric Boolean circuits with majority gates are exactly those definable in fixed-point logic with counting. This shows that inexpressibility results in the latter logic lead to lower bounds against polynomial-size families of symmetric circuits.

This research was supported by EPSRC grant EP/H026835. An extended abstract of this paper appeared in STACS 2014 [1].

Open Access

This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

1 Introduction

A property of graphs on n vertices can be seen as a Boolean function which takes as inputs the $\binom {n}{2}$ potential edges (each of which can be 0 or 1) and outputs either 0 or 1. For the function to really determine a property of the graph, as opposed to a function of a particular presentation of it, the function must be invariant under re-ordering the vertices of the graph. That is, permuting the $\binom {n}{2}$ inputs according to some permutation of [n] leaves the value of the function unchanged. We call such Boolean functions invariant. Note that this does not require the Boolean function to be invariant under all permutations of its inputs, which would mean that it was entirely determined by the number of inputs that are set to 1.

The interest in invariant functions arises in the context of characterising the properties of finite relational structures (such as finite graphs) that are decidable in polynomial time. It is a long-standing open problem in descriptive complexity to give a characterisation of the polynomial-time properties of finite relational structures (or, indeed, just graphs) as the classes of structures definable in some suitable logic (see, for instance, [11, Chapter 11]). It is known that fixed-point logic FP and its extension with counting FPC are strictly less expressive than deterministic polynomial time P [4].

It is easy to see that every polynomial-time property of graphs is decided by a polynomial-time uniform family of polynomial-size circuits that are invariant in the sense above. On the other hand, when a property of graphs is expressed in a formal logic, it gives rise to a family of circuits that is explicitly invariant or symmetric. By this we mean that its invariance is witnessed by the automorphisms of the circuit itself. For instance, any sentence of FP translates into a polynomial-size family of symmetric Boolean circuits, while any sentence of FPC translates into a polynomial-size family of symmetric Boolean circuits with majority gates.

Concretely, a circuit C _n consists of a directed acyclic graph whose internal gates are marked by operations from a basis (e.g., the standard Boolean basis ${\mathbb {B}}_{\text {std}} := \{\text {AND, OR, NAND}\}$ or the majority basis ${\mathbb {B}}_{\text {maj}} = {\mathbb {B}}_{\text {std}} \cup {\{{\text {MAJ}}\}}$) and input gates which are marked with pairs of vertices representing potential edges of an n-vertex input graph. Such a circuit is symmetric if C _n has an automorphism π induced by each permutation σ of the n vertices, i.e., π moves the input gates of C _n according to σ and preserves operations and wiring of the internal gates of C _n. Clearly, any symmetric circuit is invariant.

Are symmetric circuits a weaker model of computation than invariant circuits? We aim at characterising the properties that can be decided by uniform families of polynomial-size symmetric circuits. Our main result shows that, indeed, any property that is decided by a uniform family of polynomial-size symmetric majority circuits can be expressed in FPC.

Theorem 1

A graph property is decided by a polynomial-time uniform family of polynomial-size symmetric majority circuits if, and only if, it is defined by a fixed-point with counting sentence.

A consequence of this result is that inexpressibility results that have been proved for FPC can be translated into lower bound results for symmetric circuits. For instance, it follows (using [6]) that there is no polynomial-size family of symmetric majority circuits deciding 3-colourability or Hamiltonicity of graphs.

We also achieve a characterisation similar to Theorem 1 of symmetric Boolean circuits.

Theorem 2

A graph property is decided by a polynomial-time uniform family of polynomial-size symmetric Boolean circuits if, and only if, it is defined by a fixed-point sentence interpreted in $\mathcal {G} \oplus {\langle {[n], \le }\rangle }$ , i.e., the structure that is the disjoint union of an n-vertex graph $\mathcal {G}$ with a linear order of length n.

Note that symmetric majority circuits can be transformed into symmetric Boolean circuits. But, since FP, even interpreted over $\mathcal {G} \oplus {\langle {[n], \le }\rangle }$, is strictly less expressive than FPC, our results imply that any such translation must involve a super-polynomial blow-up in size. Similarly, our results imply with [4] that invariant Boolean circuits cannot be transformed into symmetric circuits (even with majority gates) without a super-polynomial blow-up in size. On the other hand, it is clear that symmetric majority circuits can still be translated into invariant Boolean circuits with only a polynomial blow-up.

Support

The main technical tool in establishing the translation from uniform families of symmetric circuits to sentences in fixed-point logics is a support theorem (stated informally below) that establishes properties of the stabiliser groups of gates in symmetric circuits.

We say that a set $X \subseteq [n]$ supports a gate g in a symmetric circuit C on an n-element input structure if every automorphism of C that is generated by a permutation of [n] fixing X also fixes g. It is not difficult to see that for a family of symmetric circuits obtained from a given first-order formula ϕ there is a constant k such that all gates in all circuits of the family have a support of size at most k. To be precise, the gates in such a circuit correspond to sub-formulas ψ of ϕ along with an assignment of values from [n] to the free variables of ψ. The set of elements of [n] appearing in such an assignment forms a support of the gate and its size is bounded by the number of free variables of ψ. Using the fact that any formula of FP is equivalent, on structures of size n, to a first-order formula with a constant bound k on the number of variables and, similarly, that any formula of FPC is equivalent to a first-order formula with majority quantifiers (see [16]) and a constant bound on the number of variables, we see that the resulting circuits have supports of constant bounded size. Our main technical result is that the existence of supports of bounded size holds, in fact, for all polynomial-size families of symmetric circuits. In its general form, we show the following theorem in Section 3 via an involved combinatorial argument.

Theorem 3 (Informal Support Thm)

Let C be a symmetric circuit with s gates over a graph of size n. If n is sufficiently large and s is sub-exponential in n, then every gate in C has a support of size $O\left (\frac {\log s}{\log n}\right ).$

In the typical instantiation of the Support Theorem the circuit C contains a polynomial number of gates s=poly(n) and hence the theorem implies that every gate has a support that is bounded in size by a constant. The proof of the Support Theorem mainly relies on the structural properties of symmetric circuits and is largely independent of the semantics of such circuits; this means it may be of independent interest for other circuit bases and in other settings.

Symmetric Circuits and FP

In Section 4 we show that each polynomial-size family ${\mathcal {C}}$ of symmetric circuits can be translated into a formula of fixed-point logic. If the family ${\mathcal {C}}$ is polynomial-time uniform, by the Immerman-Vardi Theorem [14, 19] there is an FP-definable interpretation of the circuit C _n in the ordered structure 〈[n],≤〉. We show that the support of a gate is computable in polynomial time, and hence we can also interpret the support of each gate in 〈[n],≤〉. The circuit C _n can be evaluated on an input graph (say) ${\mathcal {G}}$ by fixing a bijection between [n] and the set U of vertices of ${\mathcal {G}}$. We associate with each gate g of C _n the set of those bijections that cause g to evaluate to 1 on ${\mathcal {G}}$. This set of bijections admits a compact (i.e., polynomial-size) representation as the set of injective maps from the support of g to U. We show that these compact representations can be inductively defined by formulas of FP, or FPC if the circuit also admits majority gates.

Thus, we obtain that uniform families of polynomial-size symmetric Boolean circuits can be translated into formulas of FP interpreted in ${\mathcal {G}}$ combined with a disjoint linear order ${\langle {[|{\mathcal {G}}|],\le }\rangle }$, while families containing majority gates can be simulated by sentences of FPC. The reverse containment follows using classical techniques. As a consequence we obtain the equivalences of Theorems 1 & 2, and a number of more general results as this sequence of arguments naturally extends to: (i) inputs given as an arbitrary relational structure, (ii) outputs defining arbitrary relational queries, and (iii) (non-uniform) families of polynomial-size circuits, provided the logic is allowed additional advice on the disjoint linear order.

Related Work

We note that the term “symmetric circuit” is used by Denenberg et al. in [10] to mean what we call invariant circuits. They give a characterisation of first-order definability in terms of a restricted invariance condition, namely circuits that are invariant and whose relativisation to subsets of the universe remains invariant. Our definition of symmetric circuits follows that in [17] where Otto describes it as the “natural and straightforward combinatorial condition to guarantee generic or isomorphism-invariant performance.” He then combines it with a size restriction on the orbits of gates along with a strong uniformity condition, which he calls “coherence”, to give an exact characterisation of definability in infinitary logic. A key element in his construction is the proof that if the orbits of gates in such a circuit are polynomially bounded in size then they have supports of bounded size. We remove the assumption of coherence from this argument and show that constant size supports exist in any polynomial-size symmetric circuit. This requires a generalisation of what Otto calls a “base” to supporting partitions. See Section 6 for more discussion of connections with Otto’s work. Clote and Kranakis [5] show that Boolean functions on binary strings that are close to being invariant under all permutations can be computed by constant-depth threshold circuits (here “close” means that the index of the invariance group in the symmetric group is bounded by a polynomial in the input length of the Boolean function).

2 Preliminaries

Let [n] denote the set of positive integers {1,…,n}. Let Sym_S denote the group of all permutations of the set S. When S=[n], we write Sym_n for Sym_[n].

2.1 Vocabularies, Structures, and Logics

A relational vocabulary (always denoted by τ) is a finite sequence of relation symbols $(R_{1}^{r_{1}},\ldots ,R_{k}^{r_{k}})$ where for each i∈[k] the relation symbol R _i has an associated arity $r_{i} \in {\mathbb {N}}$. A τ-structure ${\mathcal {A}}$ is a tuple ${\langle {A,R_{1}^{{\mathcal {A}}},\ldots ,R_{k}^{{\mathcal {A}}}}\rangle }$ consisting of (i) a non-empty set U called the universe of ${\mathcal {A}}$, and (ii) relations $R_{i}^{{\mathcal {A}}} \subseteq U^{r_{i}}$ for i∈[k]. Members of the universe U are called elements of ${\mathcal {A}}$. A multi-sorted structure is one whose universe is given as a disjoint union of several distinct sets called sorts. Define the size of a structure $|{\mathcal {A}}|$ to be the cardinality of its universe. All structures considered in this paper are finite, i.e., their universes have finite cardinality. Let fin[τ] denote the set of all finite τ-structures.

First-Order and Fixed-Point Logics

Let FO(τ) denote first-order logic with respect to the vocabulary τ. The logic FO(τ) is the set of formulas whose atoms are formed using the relation symbols in τ, an equality symbol =, an infinite sequence of variables (x,y,z…), and that are closed under the Boolean connectives ( ∧ and ∨), negation ( ¬), and universal and existential quantification ( ∀ and ∃). Let fixed-point logic FP(τ) denote the extension of FO(τ) to include an inflationary fixed-point operator ifp (see [7] for a definition). Assume standard syntax and semantics for FO and FP (see the textbook [11] for more background). For a formula ϕ write ϕ(x) to indicate that x is the tuple of the free variables of ϕ. For a logic $\mathcal {L}$, a formula $\phi (x) \in \mathcal {L}(\tau )$ with k free variables, ${\mathcal {A}} \in {\text {fin}}[\tau ]$, and tuple a∈A ^k write ${\mathcal {A}} \models _{\mathcal {L}} \phi [a]$ to express that the tuple a makes the formula ϕ true in the structure ${\mathcal {A}}$ with respect to the logic $\mathcal {L}$. We usually drop the subscript $\mathcal {L}$ and write ${\mathcal {A}} \models \phi [a]$ when no confusion would arise.

Logics with Disjoint Advice

Let τ _arb be a relational vocabulary without a binary relation symbol ≤. Let $\Upsilon : {\mathbb {N}} \rightarrow {\text {fin}}[{\tau _{\text {arb}}} \uplus {\{{\le ^{2}}\}}]$ be an advice function, where for $n \in {\mathbb {N}}$, Υ(n) has universe {0,1,…,n} naturally ordered by ≤. For a logic $\mathcal {L}$, typically FO or FP, let $({\mathcal {L} +\mathrm {\Upsilon }})(\tau )$ denote the set of formulas of $\mathcal {L}(\tau ^{\prime })$ where $\tau ^{\prime } := \tau \uplus {\tau _{\text {arb}}} \uplus {\{{\le ^{2}}\}}$ and τ is a vocabulary disjoint from τ _arb⊎{≤²}. For a structure ${\mathcal {A}} \in {\text {fin}}[\tau ]$ define the semantics of $\phi \in ({\mathcal {L} +\mathrm {\Upsilon }})(\tau )$ to be ${\mathcal {A}} \models _{({\mathcal {L} +\mathrm {\Upsilon }})} \phi \text { iff} {\mathcal {A}}^{\Upsilon } \models _{\mathcal {L}} \phi , $where ${\mathcal {A}}^{\Upsilon } := {\mathcal {A}} \oplus \Upsilon (|{\mathcal {A}}|)$ is the multi-sorted $\tau ^{\prime }$-structure formed by taking the disjoint union of ${\mathcal {A}}$ with a structure coding a linear order of corresponding cardinality endowed with interpretations of the relations in τ _arb. The universe of the multi-sorted structure ${\mathcal {A}}^{\Upsilon }$ is written as U⊎{0,1,…,|U|}; refer to U as the point sort of ${\mathcal {A}}^{\Upsilon }$ and to {0,1,…,|U|} as the number sort of ${\mathcal {A}}^{\Upsilon }$. We are primarily interested in the special case when τ _arb is empty and hence $\Upsilon (|{\mathcal {A}}|) = {\langle {{\{{0,1,\ldots ,|U|}\}},\le }\rangle }$ is simply a linear order. Denote formulas of this logic by $({\mathcal {L} +\mathrm {\le }})(\tau )$ and extended structures by ${\mathcal {A}}^{\le }$ to emphasise the disjoint linear order.

Let FPC(τ) denote the extension of (FP+≤)(τ) with a counting operator # _x where x is a point or number variable. For a structure ${\mathcal {A}} \in {\text {fin}}[\tau ]$ and a formula ϕ(x)∈FPC(τ), # _x ϕ(x) is a term denoting the element in the number sort corresponding to $|\{{{a \in {\mathcal {A}}}\;|\;{{\mathcal {A}} \models \phi [a]\}}}|$. See [11, Section 8.4.2] for more details. Finally, we consider the extension of fixed-point logic with both advice functions and counting quantifiers (FPC+Υ)(τ).

Using k-tuples of number variables, it is possible in FP+≤ and FPC to represent numbers up to n ^k and perform arithmetic operations on them (see [15, 1.32–1.33]). We omit details but use such constructions freely.

2.2 Symmetric and Uniform Circuits

A Boolean basis (always denoted by $\mathbb {B}$) is a finite set of Boolean functions from {0,1}^∗ to {0,1}. We consider only bases containing symmetric functions, i.e., for all $f \in \mathbb {B}$, f(x)=f(y) for all $n \in {\mathbb {N}}$ and x,y∈{0,1}ⁿ with the same number of ones. The standard Boolean basis ${\mathbb {B}}_{\text {std}}$ consists of unbounded fan-in AND, OR, and NAND operators.¹ The majority basis ${\mathbb {B}}_{\text {maj}}$ extends the standard basis with an operator MAJ which is one iff the number of ones in the input is at least the number of zeroes.

Definition 1 (Circuits on Structures)

A Boolean $(\mathbb {B},\tau )$-circuit C _n computing a q-ary query Q is a structure 〈G,W,Ω,Σ,Λ〉.

G is a set called the gates of C _n. The size of C _n is |C _n|:=|G|.
$W \subseteq G \times G$ is a binary relation called the wires of the circuit. We require that (G,W) forms a directed acyclic graph. Call the gates with no incoming wires input gates, and all other gates internal gates. Gates h with (h,g)∈W are called the children of g.
Ω is an injective function from [n]^q to G. The gates in the image of Ω are called the output gates. When q=0, Ω is a constant function mapping to a single output gate.
Σ is a function from G to $\mathbb {B} \uplus \tau \uplus {\{{0,1}\}}$ which maps input gates into τ⊎{0,1} with |Σ⁻¹(0)|,|Σ⁻¹(1)|≤1 and internal gates into $\mathbb {B}$. Call the input gates marked with a relation from τ relational gates and the input gates marked with 0 or 1 constant gates.
Λ is a sequence of injective functions (Λ_R)_R∈τ where for each R∈τ, Λ_R maps each relational gate g with R=Σ(g) to the tuple Λ_R(g)∈[n]^r where r is the arity of R. Where no ambiguity arises, we write Λ(g) for Λ_R(g).

We write C=C _n to emphasise that C accepts input structures of size n. The variable n will always be used to represent this quantity, we often drop the subscript for clarity.

Let C=C _n be a Boolean $(\mathbb {B},\tau )$-circuit, ${\mathcal {A}} \in {\text {fin}}[\tau ]$ with $|{\mathcal {A}}| = n$, and $\gamma : U \rightarrow [n]$ be a bijection. Let $\gamma {\mathcal {A}}$ denote the τ-structure over the universe [n] obtained by relabeling the universe of ${\mathcal {A}}$ according to γ. Recursively evaluate C on $\gamma {\mathcal {A}}$ by determining a value $C[\gamma {\mathcal {A}}](g)$ for each gate g: (i) a constant gate evaluates to the bit given by Σ(g), (ii) a relational gate evaluates to 1 iff $\gamma {\mathcal {A}} \models \Sigma (g)(\Lambda (g))$, and (iii) an internal gate evaluates to the result of applying the Boolean operation Σ(g) to the values for g’s children. C defines the q-ary query $Q \subseteq {\mathcal {A}}^{q}$ where a∈Q iff $C[\gamma {\mathcal {A}}](\Omega (\gamma a)) = 1$.

Definition 2 (Invariant Circuit)

Let C be a $(\mathbb {B},\tau )$-circuit computing a q-ary query on structures of size n. The circuit C is invariant if for every ${\mathcal {A}} \in {\text {fin}}[\tau ]$ with $|{\mathcal {A}}| = n$, $a \in {\mathcal {A}}^{q}$, and bijections γ ₁,γ ₂ from A to [n], $C[\gamma _{1}{\mathcal {A}}](\Omega (\gamma _{1}a)) = C[\gamma _{2}{\mathcal {A}}](\Omega (\gamma _{2}a)).$

Invariance indicates that C computes a property of τ-structures which is invariant to presentations of the structure. A family ${\mathcal {C}} = (C_{n})_{n \in {\mathbb {N}}}$ of invariant $(\mathbb {B},\tau )$-circuits naturally computes a q-ary query on τ-structures. When q=0 the family computes a Boolean property of structures (i.e. a decision problem). We now discuss a structural property of circuits called symmetry that implies invariance.

Symmetric Circuits

Permuting a circuit’s universe may induce automorphisms of the circuit.

Definition 3 (Automorphism)

Let C=〈G,W,Ω,Σ,Λ〉 be a $(\mathbb {B},\tau )$-circuit computing a q-ary query on structures of size n. Let σ∈Symn and $\pi : G \rightarrow G$ be a bijection such that

for all gates g,h∈G, W(g,h) iff W(π(g),π(h)),
for all output tuples x∈[n]^q, πΩ(x)=Ω(σ(x)),
for all gates g∈G, Σ(g)=Σ(π(g)), and
for each relational gate g∈G, σΛ(g)=Λ(π(g)).

We say that π is an automorphism of C, and that σ induces the automorphism π of C. We label the group of C’s automorphisms Aut_n(C).

Note that a permutation σ may induce more than one automorphism of the circuit.

The principal goal of this paper is to understand the computational power of circuit classes with the following type of structural symmetry.

Definition 4 (Symmetric)

A circuit C on structures of size n is called symmetric if for every permutation σ∈Sym_n, σ induces an automorphism of C.

It is not difficult to see that, for a symmetric circuit C, there is a homomorphism $h: {\text {Sym}_{n}} \rightarrow \text {Aut}_{n}({C})$ such that h(σ) is an automorphism induced by σ. As long as some element of [n] appears in the label of some input gate of C, by symmetry every element of [n] appears and it follows that h is an injective homomorphism. Henceforth we assume that this is always the case as otherwise C has no relational inputs and computes a constant function. Circuits where the homomorphism is not also surjective introduce artifacts into our arguments. To avoid this we require the circuits we consider to be rigid.

Definition 5 (Rigid)

Let C=〈G,W,Ω,Σ,Λ〉 be a $(\mathbb {B},\tau )$-circuit. Call C rigid if there do not exist distinct internal gates $g,g^{\prime } \in G$ with $\Sigma (g) = \Sigma (g^{\prime })$, $\Omega ^{-1}(g) = \Omega ^{-1}(g^{\prime })$, and for every $g^{\prime \prime } \in G$, $W(g^{\prime \prime },g)$ iff $W(g^{\prime \prime },g^{\prime })$ and $W(g,g^{\prime \prime })$ iff $W(g^{\prime },g^{\prime \prime })$.

To show that for rigid symmetric circuits C, any injective homomorphism from Sym_n to Aut_n(C) is surjective, it suffices to show that each σ∈Sym_n induces a unique automorphism in Aut_n(C).

Proposition 1

Let C be a rigid circuit on structures of size n, and σ∈Sym _n . If σ induces an automorphism of C, that automorphism is unique.

We defer the proof of this proposition to Section 4.1 where we also show that symmetric circuits can be transformed into equivalent rigid symmetric circuits in polynomial time, and hence show that rigidity can be assumed of circuits without loss of generality in our setting. For a rigid symmetric circuit C, the group of automorphisms of C is exactly Sym_n acting faithfully. We shall therefore abuse notation and use these interchangeably. In particular, we shall write σ g to denote the image of a gate g in C under the action of the automorphism induced by a permutation σ in Sym_n.

An examination of the definitions suffices to show that symmetry implies invariance. In symmetric circuits it is useful to consider those permutations which induce automorphisms that fix gates. Let $\mathcal {P}$ be a partition of a set [n]. Let the pointwise stabiliser of $\mathcal {P}$ be

$${\text{Stab}_{n}(\mathcal{P})} := {\{{ \sigma \in {\text{Sym}_{n}}}\;|\;{\forall P \in \mathcal{P}, \sigma P = P\}}}, $$

and similarly define the setwise stabiliser

$${\text{SetStab}_{n}({\mathcal{P}})} := {\{{ \sigma \in {\text{Sym}_{n}}}\;|\;{\forall P \in \mathcal{P}, \sigma P \in \mathcal{P}\}}}. $$

For a gate g in a rigid symmetric circuit C, let the stabiliser of g be Stab_n(g):={σ∈Sym_n | σ(g)=g}, and let the orbit of g under the automorphism group Aut_n(C) of C be Orb(g):={π g | π∈Aut_n(C)}.

Uniform Circuits

One natural class of circuits are those with polynomial-size descriptions that can be generated by a deterministic polynomial-time Turing machine.

Definition 6 ( P-Uniform Polynomial-Size Circuits)

A polynomial-size $(\mathbb {B},\tau )$-circuit family ${\mathcal {C}} = (C_{n})_{n \in {\mathbb {N}}}$ computing a q-ary query is P-uniform if there exists an integer t≥q and function $\Upsilon : {\mathbb {N}} \rightarrow {\{{0,1}\}}^{*}$, computable by a determininistic polynomial-time Turing machine M, which takes an integer n to a binary string Υ(n) such that |Υ(n)|=poly(n), and Υ(n) describes² the circuit C _n whose gates are indexed by t-tuples of {0,1,…,n}, inputs are labeled by tuples from [n], and outputs are labeled by q-tuples of [n].

Note that such uniform families explicitly have polynomial size. For more background on circuit uniformity, c.f., e.g., the text [20]. It follows from the Immerman-Vardi Theorem [14, 19] that any P-uniform family ${\mathcal {C}} = (C_{n})_{n \in {\mathbb {N}}}$ of polynomial-size circuits is definable by an FP interpretation in the sense that there is a sequence of formulas $(\phi _{G}, \phi _{W}, \phi _{\Omega },(\phi _{s})_{s \in \mathbb {B} \uplus \tau \uplus {\{{0,1}\}}}, (\phi _{\Lambda _{R}})_{R\in \tau })$ which, interpreted in the structure 〈[n],≤〉, describes the circuit C _n=〈G,W,Ω,Σ,Λ〉, with

$G \subseteq [n]^{t}$ such that g∈G iff 〈[n],≤〉⊧ϕ _G[g].
For all $g,g^{\prime } \in G$ and $W(g,g^{\prime })$ iff ${\langle {[n],\le }\rangle } \models \phi _{W}[g,g^{\prime }]$.
For all g∈G and a∈[n]^q, Ω(a)=g iff 〈[n],≤〉⊧ϕ _Ω[a,g].
For all g∈G and $s \in \mathbb {B} \uplus \tau \uplus {\{{0,1}\}}$, Σ(g)=s iff 〈[n],≤〉⊧ϕ _s[g].
For all relational gates g∈G and a∈[n]^r, Λ_R(g)=a iff 〈[n],≤〉⊧ϕ _Λ[g,a], where r is the arity of R=Σ(g).

More generally, if we do not know how to efficiently compute Υ for a polynomial-size circuit family ${\mathcal {C}} = (C_{n})_{n \in {\mathbb {N}}}$, there is still an (FP+Υ)-definable interpretation of C _n in ${\mathcal {A}}^{\Upsilon }$.

Circuits need not compute invariant queries as their computation may implicitly depend on the order associated with [n]. To obtain invariance for such circuits we assert symmetry. The next section proves a natural property of symmetric circuits that ultimately implies that symmetric P-uniform circuits of polynomial size coincide with FP definitions on the standard and majority bases.

3 Symmetry and Support

In this section we analyse the structural properties of symmetric circuits. We begin with a formal definition of support.

Definition 7 (Support)

Let C be a rigid symmetric circuit on structures of size n and let g be a gate in C. A set $X \subseteq [n]$ supports g if, for any permutation σ∈Sym_n such that σ x=x for all x∈X, we have σ g=g (i.e., σ∈Stab_n(g)).³

We show how to associate supports of constant size in a canonical way to all gates in any rigid symmetric circuit of polynomial size. Indeed, our result is more general as it associates moderately growing supports to gates in circuits of sub-exponential size. As a preliminary to the proof, we introduce, in Section 3.1, the more general notion of a supporting partition for a permutation group. We show how to associate a canonical such supporting partition with any permutation group G and obtain bounds on the size of such a partition based on the index of G in the symmetric group. These results are then used, in Section 3.2, to bound the size of partitions supporting stabiliser groups of gates based on the size of the circuit, proving our main technical result—the Support Theorem.

3.1 Supporting Partitions

The notion of a supporting partition generalises the notion of a support of a gate by replacing the set with a partition and the stabiliser group of the gate with an arbitrary permutation group.

Definition 8 (Supporting Partition)

Let $G \subseteq {\text {Sym}_{n}}$ be a group and $\mathcal {P}$ a partition of [n]. We say that ${\mathcal {P}}$ is a supporting partition of G if ${\text {Stab}_{n}}{\mathcal {P}} \subseteq G$.

For intuition consider two extremes. When G has supporting partition $\mathcal {P} = {\{{[n]}\}}$, it indicates G=Sym_n. Saying that G has supporting partition $\mathcal {P} = {\{{\{1\},\{2\},\ldots ,\{n}}\}\}$ indicates only that G contains the identity permutation, which is always true.

A natural partial order on partitions is the coarseness relation, i.e., $\mathcal {P}^{\prime }$ is as coarse as $\mathcal {P}$, denoted $\mathcal {P}^{\prime } \supseteq \mathcal {P}$, if every part in $\mathcal {P}$ is contained in some part of $\mathcal {P}^{\prime }$. For two partitions $\mathcal {P}$ and $\mathcal {P}^{\prime }$, there is a most refined partition that is as coarse as either partition:

Definition 9

Let $\mathcal {P},\mathcal {P}^{\prime }$ be partitions of [n]. Define a binary relation ∼ on [n]: x ₁∼x ₂ iff there exists $P \in \mathcal {P}$ or $P \in \mathcal {P}^{\prime }$ such that x ₁,x ₂∈P. Let ${\mathcal {E}}(\mathcal {P},\mathcal {P}^{\prime })$ denote the partition of [n] corresponding to the equivalence classes of [n] under the transitive closure of ∼.⁴

Now it is easy to show that ${\mathcal {E}}$ preserves supporting partitions (the proof is similar to that of (*) on page 379 of [17]).

Proposition 2

Let $G \subseteq {\text {Sym}_{n}}$ be a group and $\mathcal {P},\mathcal {P}^{\prime }$ be supporting partitions of G. Then ${\mathcal {E}}(\mathcal {P},\mathcal {P}^{\prime })$ is also a supporting partition of G.

Proof

Let ${\mathcal {E}} := {\mathcal {E}}(\mathcal {P},\mathcal {P}^{\prime }) = {\{{E_{1},\ldots ,E_{m}}\}}$. Suppose $\sigma \in {\text {Stab}({\mathcal {E}})}$ and we now show that σ∈ G. Because the parts E _i are disjoint write σ as σ ₁⋯σ _m where σ _i∈Sym_E _i (i.e., it permutes only the elements of E _i). Indeed each σ _i may be written as a sequence of transpositions of elements in E _i. Thus it suffices to show that each transposition $(x x^{\prime })$ with $x,x^{\prime } \in E_{i}$ can be written as a sequence of permutations in ${\text {Stab}(\mathcal {P})} \cup {\text {Stab}(\mathcal {P}^{\prime })} \subseteq G$. Since $x,x^{\prime } \in E_{i}$ there is a sequence of elements of x ₁,…,x _ℓ with x ₁=x, $x_{\ell } = x^{\prime }$ and x _j∼x _j+1 for j∈[ℓ−1] witnessing the path from x to $x^{\prime }$. By the definition of ∼, for each j∈[ℓ−1] there is $P \in \mathcal {P}$ or $P \in \mathcal {P}^{\prime }$ such that x _j,x _j+1∈P and therefore (x _j x _j+1) is a transposition in ${\text {Stab}(\mathcal {P})} \cup {\text {Stab}(\mathcal {P}^{\prime })}$. Conclude that the transposition $(xx^{\prime }) = (x_{1}x_{\ell }) = (x_{1}x_{2})(x_{2}x_{3})\cdots (x_{\ell -2}x_{\ell -1})(x_{\ell -1}x_{\ell })(x_{\ell -2}x_{\ell -1})\cdots (x_{1}x_{2})$ is a sequence of transpositions from ${\text {Stab}(\mathcal {P})} \cup {\text {Stab}(\mathcal {P}^{\prime })}$ and the proof is complete.

This implies that each permutation group has a unique coarsest partition that supports it.

Lemma 1

Each permutation group $G\subseteq {\text {Sym}_{n}}$ has a unique coarsest supporting partition.

Proof

Suppose G has two distinct coarsest partitions $\mathcal {P},\mathcal {P}^{\prime }$ of [n] that support it, then Proposition 2 implies that the coarser partition ${\mathcal {E}}(\mathcal {P},\mathcal {P}^{\prime })$ also supports G. This is a contradiction assuming ${\mathcal {E}}(\mathcal {P},\mathcal {P}^{\prime })$ is not either $\mathcal {P}$ or $\mathcal {P}^{\prime }$.

We write S P(G) for the unique coarsest partition supporting G. For a partition $\mathcal {P}$ of [n] we write $|\mathcal {P}|$ to denote its size, i.e., the number of parts $\mathcal {P}$ contains, and for a permutation σ∈Sym_n, we write $\sigma \mathcal {P}$ for the partition ${\{{\sigma P}\;|\;{P \in \mathcal {P}\}}}$. Note that this commutes with the operation ${\mathcal {E}}$, so $\sigma {\mathcal {E}}(\mathcal {P},\mathcal {P}^{\prime }) = {\mathcal {E}}(\sigma \mathcal {P},\sigma \mathcal {P}^{\prime })$. The next lemma shows how supporting partitions are affected by the conjugacy action of Sym_n.

Lemma 2

If $\mathcal {P}$ is a partition supporting a group G, then for any σ∈Sym _n , $\sigma \mathcal {P}$ supports the group σGσ ⁻¹.

Proof

Let $\pi \in {\text {Stab}_{n}(\sigma \mathcal {P})}$ and let P be a part in $\mathcal {P}$, then:

$$(\sigma^{-1}\pi\sigma)P = (\sigma^{-1}\pi)(\sigma P) = \sigma^{-1}\sigma P = P, $$

where the second equality follows from the fact that π fixes σ P. Thus, σ ⁻¹ π σ fixes $\mathcal {P}$ pointwise, therefore σ ⁻¹ π σ∈G and hence π∈σ G σ ⁻¹.

This indicates how the unique coarsest supporting partition of a group translates under conjugation.

Lemma 3

For any $G \subseteq {\text {Sym}_{n}}$ and any σ∈Sym _n, σS P(G)=S P(σGσ⁻¹).

Proof

Immediate from Lemma 2 and the fact that the action of ${\mathcal {E}}$ commutes with σ.

We conclude that any group G is sandwiched between the pointwise and setwise stabilisers of S P(G).

Lemma 4

For any group $G \subseteq {\text {Sym}_{n}}$ , we have

$${\text{Stab}}_{n}(\mathsf{SP}(G)) \subseteq G \subseteq {\text{SetStab}_{n}({\mathsf{SP}(G)})}. $$

Proof

The first inclusion is by definition of supporting partitions. For the second, note that if σ∈G, then σ G σ ⁻¹=G. Then, by Lemma 3, σ S P(G)=S P(G).

Note that these bounds need not be tight. For example, if G is the alternating group on n (or, indeed, any transitive, primitive proper subgroup of Sym_n), then S P(G) is the partition of [n] into singletons, i.e., S P(G)={{x ₁},{x ₂},…,{x _n}}. In this case, Stab_n(S P(G)) is the trivial group while SetStab_n(S P(G)) is all of Sym_n.

We now use the bounds given by Lemma 4, in conjunction with bounds on G to obtain size bounds on S P(G). Recall that the index of G in Sym_n, denoted [Sym_n:G] is the number of cosets of G in Sym_n or, equivalently, $\frac {|{\text {Sym}_{n}}|}{|G|}$. The next lemma says that if $\mathcal {P}$ is a partition of [n] where the index of ${\text {SetStab}_{n}({\mathcal {P}})}$ in Sym_n is sufficiently small then the number of parts in $\mathcal {P}$ is either very small or very big.

Lemma 5

For any 𝜖 and n such that 0<𝜖<1 and $\log n \geq \frac {4}{\epsilon }$ , if $\mathcal {P}$ is a partition of [n] with k parts, $s := {[{\text {Sym}_{n}}:{\text {SetStab}_{n}({\mathcal {P}})}]}$ and $n \leq s \leq 2^{n^{1-\epsilon }}$ , then $\min {\{{k,n-k}\}} \le \frac {8}{\epsilon } \frac {\log s}{\log n}$.

Proof

Let p ₁≤p ₂≤…≤p _k be the respective sizes of the parts in $\mathcal {P}$. Thus,

$$ \hfill s = \frac{n!}{|{\text{SetStab}_{n}({\mathcal{P}})}|} \ge \frac{1}{k!}\frac{n!}{p_{1}! p_{2}! \cdots p_{k}!}.\hfill $$

(1)

Observe that, if p _i>1, then p ₁!p ₂!⋯p _k!≤p ₁!p ₂!⋯(p _i−1)!⋯(p _k+1)!. By repeatedly applying this, we see that in the lower bound on s given by (1), we can replace p ₁!p ₂!⋯p _k! by (n−(k−1))!. Let $k^{\prime } := \min {\{{k,n-k}\}}$ and we have

$$\begin{array}{@{}rcl@{}} s &\ge& \frac{n!}{k! (n-(k-1))!} = \frac{1}{n+1}\binom{n+1}{k} \ge \frac{1}{n+1}\binom{n}{k}\\ &=& \frac{1}{n+1}\binom{n}{k^{\prime}} \ge \frac{1}{n+1}\left(\frac{n}{k^{\prime}}\right)^{k^{\prime}} \end{array} $$

where the second equality follows because $\binom {n}{k} = \binom {n}{n-k} = \binom {n}{k^{\prime }}$, and the final inequality follows from a simple combinatorial bound. Take the logarithm of both sides of the above equation to get $\log s \ge k^{\prime } (\log n - \log k^{\prime }) - \log (n+1)$. Using the fact that s≥n≥2 ($\log n \ge \frac {4}{\epsilon } \ge 4$) then implies that

$$ \hfill 4\log s \ge k^{\prime} (\log n - \log k^{\prime}), \hfill $$

(2)

The definition of $k^{\prime }$ implies that $k^{\prime } \le \frac {n}{2}$ and $\log n - \log k^{\prime } \ge 1$. Plugging this into (2) gives that $4\log s \ge k^{\prime }.$ Take the logarithm of this inequality and apply the upper bound on s to determine that $(1-\epsilon )\log n + 2 \ge \log k^{\prime }.$ Inserting this inequality back into (2) gives $4 \log s \ge k^{\prime } (\epsilon \log n - 2).$ Since $\frac {\epsilon }{2}\log n \ge 2$, conclude that $k^{\prime } \le \frac {8}{\epsilon }\frac {\log s}{\log n}$.

We use a similar argument to establish that, under the assumptions of the previous lemma, when the number of parts in $\mathcal {P}$ is less than $\frac {n}{2}$ the largest part is very big. The intuition is that the number of elements in any union of the parts must either be very small or very big, in the same sense as before, because otherwise it violates the bound on the orbit size. Then, because we assume there are few parts, one part must be large and the rest small.

Lemma 6

For any 𝜖 and n such that 0<𝜖<1 and $\log n \geq \frac {8}{\epsilon ^{2}}$ , if $\mathcal {P}$ is a partition of [n] with $|{\mathcal {P}}| \leq \frac {n}{2}$ , $s := {[{\text {Sym}_{n}}:{\text {SetStab}_{n}({\mathcal {P}})}]}$ and $n \leq s \leq 2^{n^{1-\epsilon }}$ , then $\mathcal {P}$ contains a part P with at least $n - \frac {33}{\epsilon } \cdot \frac {\log s}{\log n}$ elements.

Proof

The initial setup is the same as in the proof of Lemma 5. Let p ₁≤p ₂≤…≤p _k be the respective sizes of the parts in $\mathcal {P}$ and let $S := \sum _{i = 1}^{k-1}p_{i}$. Our aim is to show that $S \leq \frac {33}{\epsilon } \cdot \frac {\log s}{\log n}$. Denote the size of the second largest part by p:=p _k−1. We have

$$ \hfill s = \frac{n!}{|{\text{SetStab}_{n}({\mathcal{P}})}|} \ge \frac{1}{k!}\frac{n!}{p_{1}!p_{2}! \cdots p_{k}!}.\hfill $$

(3)

Let $\ell \in {\mathbb {N}}$ be such that

$$ \hfill \ell \le k-1, \text{ and } k-1 + \ell (p-1) \le \sum\limits_{i = 1}^{k-1}p_{i} = S. \hfill $$

(4)

Provided $\mathcal {P}$ contains more than one part both ℓ∈{0,1} satisfy (4). We may assume that p>1 otherwise $S \le |{\mathcal {P}}|$ and we are done by Lemma 5. For any ℓ≥1 satisfying (4), redistributing weight from a p _i to p _j with i<j in a way similar to the proof of Lemma 5 gives the following,

$$\begin{array}{@{}rcl@{}} s &\ge& \frac{1}{k!}\frac{n!}{ \underbrace{1!\cdots1!}_{k-1-\ell \text{ times}} \underbrace{p!\cdots p!}_{\ell \text{ times}}(n-(k-1-\ell + \ell p))!} \ge \frac{n!}{ (p!)^{\ell} (n-\ell(p-1) + 1)!}\\ &\ge& \frac{(\frac{n}{e})^{n}}{(e \sqrt{p}(\frac{p}{e})^{p})^{\ell} (e \sqrt{n} (\frac{n}{e})^{n-\ell(p-1)+1})}=\frac{n^{\ell(p-1)-3/2}}{p^{\ell(p+1/2)}} \underbrace{\frac{e^{\ell p} e^{n-\ell(p-1)+1}}{e^{\ell+1} e^{n}}}_{=1} \end{array} $$

where the third inequality follows from Stirling’s Formula, i.e., that for any x≥2, $(\frac {x}{e})^{x} \le x! \le \sqrt {2\pi x}(\frac {x}{e})^{x} e^{\frac {1}{12x}} \le e \sqrt {x} (\frac {x}{e})^{x}$. Take the logarithm of the above equation to determine that

$$ \log s \ge \left[\ell(p-1)-\frac{3}{2}\right] \log n - \ell \left(p +\frac{1}{2}\right) \log p$$

(5)

$$\begin{array}{@{}rcl@{}}&=& \ell \left(p + \frac{1}{2}\right) (\log n - \log p) - \frac{3}{2}(\ell+1)\log n \\ &\ge& \ell p(\log n - \log p) - \frac{3}{2}\ell \log n - \frac{3}{2}\log n, \end{array}$$

(6)

$$ \frac{5}{2} \log s \ge \ell \left[p (\log n - \log p) - \frac{3}{2} \log n\right] \ge p (\log n - \log p) - \frac{3}{2}\log n,\\ 4\log s \ge p (\log n - \log p) \ge p, $$

(7)

where (6) follows from (5) since s≥n and ℓ≥1, and (7) follows from (6) because p is the size of the second largest part of $\mathcal {P}$ and hence $p \le \frac {n}{2}$ and $(\log n - \log p) \ge 1$. Take the logarithm of (7) and use the bound on s to determine that $\log p \le \log \log s + 2 \le (1-\epsilon ) \log n + 2$. Plug this bound into (6) to get that $\frac {5}{2} \log s \ge \ell p (\epsilon \log n - 2) - \frac {3}{2} \ell \log n$. Using $\frac {\epsilon }{2} \log n \ge 2$ and dividing by $\log n$, $\frac {5}{2}\frac {\log s}{\log n} \ge \ell (\frac {p\epsilon }{2} - \frac {3}{2})$.

If $\frac {p \epsilon }{4} \ge \frac {3}{2}$, then $\frac {10}{\epsilon } \frac {\log s}{\log n} \ge \ell p$. For the largest value of ℓ, k−1+(ℓ+1)(p−1)≥S, and hence k−1+2ℓ p≥S. Thus Lemma 5 implies that $S \le \frac {8 + 20}{\epsilon }\frac {\log s}{\log n}$. Otherwise $p < \frac {6}{\epsilon }$ and hence $\log p \le 3 - \log \epsilon $. Plugging this into (6) and using $\log n \ge \frac {8}{\epsilon ^{2}} \ge 2(3 - \log \epsilon ) \ge 2\log p$ gives

$$ \frac{5}{2} \log s \ge \ell \frac{p-3}{2} \log n. $$

(8)

If p≥5, then we can recover

$$\frac{5}{2\epsilon} \frac{\log s}{\log n} \ge \frac{5}{2}\frac{\log s}{\log n} \ge \ell \frac{p - 3}{2} \ge \ell \frac{p}{5} $$

from (8) and conclude $S \le \frac {8 + 25}{\epsilon }\frac {\log s}{\log n}$ analogously to before. Otherwise p≤4, and $S \le p (k-1) \le 4 \cdot \frac {8}{\epsilon }\frac {\log s}{\log n}$ by Lemma 5. Since in each case we concluded that $S \le \frac {33}{\epsilon }\frac {\log s}{\log n}$ the proof is complete.

3.2 Support Theorem

Let g be a gate in a rigid symmetric circuit C on structures of size n. From now on we abuse notation and write S P(g) for S P(Stab_n(g)). Note that, if P is any part in S P(g), then [n]∖P is a support of g in the sense of Definition 7. We write ∥S P(g)∥ to denote the smallest value of |[n]∖P| over all parts P in S P(g). Also, let S P(C) denote the maximum of ∥S P(g)∥ over all gates g in C.

The orbit-stabiliser theorem implies that |Orb(g)|=[Sym_n:Stab_n(g)]. Using Lemma 4, we have that ${\text {Stab}_{n}(g)} \subseteq {\text {SetStab}_{n}({\mathsf {SP}(g)})}$ and thus, if s is an upper bound on |Orb(g)|, s≥[Sym_n:Stab_n(g)]≥[Sym_n:SetStab_n(S P(g))]. Then, by Lemma 6, g has a support of small size provided that (i) s is sub-exponential, and (ii) S P(g) has fewer than n/2 parts. Thus, to prove our main technical theorem, which formalises Theorem 3 from the introduction, it suffices to show that if s is sufficiently sub-exponential, (ii) holds.

Theorem 4 (Support Theorem)

For any 𝜖 and n with $\frac {2}{3} \le \epsilon \le 1$ and $n > 2^{\frac {96}{\epsilon ^{2}}}$ , if C is a rigid symmetric circuit on structures of size n and $s := \max _{g \in C} |\text {Orb}(g)| \le 2^{n^{1-\epsilon }}$ , then, $\mathsf {SP}(C) \le \frac {33}{\epsilon } \frac {\log s}{\log n}.$

Proof

Suppose 1≤s<n. C cannot have relational inputs, because each relational gate must have an orbit of size at least n, so each gate of C computes a constant Boolean function. In this case the inputs to C must be constant gates, which are fixed under all permutations because they are the only gates with their label, i.e., 0 or 1. We have |S P(g)|=|{[n]}|=1 for each input gate g. This property extends inductively to the rest of C because C is rigid. Therefore the coarsest supporting partition of every gate g in C must be {[n]}, and hence 0=∥S P(g)∥=S P(C). Therefore assume s≥n.

To conclude the theorem from Lemma 6 it suffices to argue that for all gates g, $|{\mathsf {SP}(g)}| \le \frac {n}{2}$. Suppose g is a constant gate, then, as we argued before, $|{\mathsf {SP}(g)}| = |{{\{{[n]}\}}}| = 1 < \frac {n}{2}$. If g is a relational gate, then it is fixed by any permutation that fixes all elements appearing in the tuple Λ(g) and moved by all others. Thus, S P(g) must contain singleton parts for each element of [n] in the tuple Λ(g) and a part containing everything else. For the sake of contradiction suppose that $|{\mathsf {SP}(g)}| > \frac {n}{2}$ (i.e., the arity of the relation is large with respect to n), and therefore that S P(g) contains more than $\frac {n}{2}$ singleton parts. By the orbit-stabiliser theorem the orbit of g can be bounded as $|\text {Orb}(g)| = \frac {n!}{(n-|\Lambda (g)|)!} \ge \frac {n!}{(\frac {n}{2})!}$. This is contradiction with the stated bound on s, because $s \ge |\text {Orb}(g)| \ge \frac {n!}{(\frac {n}{2})!} \ge 2^{\frac {n}{4}} > 2^{n^{1-\epsilon }}$.

It remains to consider internal gates. For the sake of contradiction let g be a topologically first internal gate such that S P(g) has more than $\frac {n}{2}$ parts. Define $k^{\prime } := \left \lceil \frac {8}{\epsilon }\frac {\log s}{\log n}\right \rceil $. Note that the assumptions on s,n,and 𝜖 imply that $k^{\prime } \le \frac {1}{4} n^{1 - \epsilon } < \frac {n}{2}.$ Lemma 5 implies that $n-|{\mathsf {SP}(g)}| \le k^{\prime }$.

Let H denote the children of g. Because g is a topologically first gate with $|{\mathsf {SP}(g)}| > \frac {n}{2}$, for all h∈H, S P(h) has at most $\frac {n}{2}$ parts. As before, we argue a contradiction with the upper bound on s. This is done by demonstrating that there is a set of gate-automorphism pairs S={(h,σ) | h∈H,σ∈Sym_n} that are: (i) useful – the automorphism moves the gate out of the set of g’s children, i.e., σ h∉H, and (ii) independent – each child and its image under the automorphism are fixed points of the other automorphisms in the set, i.e., for all $(h,\sigma ), (h^{\prime }, \sigma ^{\prime }) \in S$, $\sigma ^{\prime } h = h$ and $\sigma ^{\prime } \sigma h = \sigma h$. Note that sets which are useful and independent contain tuples whose gate and automorphism parts are all distinct. The set S describes elements in the orbit of H with respect to Sym_n.

Claim 1

Let S be useful and independent, then |Orb(H)|≥2^|S|.

Proof

Let R be any subset of S. Derive an automorphism from R: $\sigma _{R} := \prod _{(h,\sigma ) \in R} \sigma $ (since automorphisms need not commute fix an arbitrary ordering of S).

Let R and Q be distinct subsets of S where without loss of generality |R|≥|Q|. Pick any (h,σ)∈R∖Q≠∅. Because S is independent σ _R h=σ h and σ _Q σ h=σ h. Since S is useful, σ h∉H. Thus σ h∈σ _R H, but σ h∉σ _Q H. Hence σ _R H≠σ _Q H. Therefore each subset of S can be identified with a distinct element in Orb(H) and hence |Orb(H)|≥2^|S|.

Thus to reach a contradiction it suffices to construct a sufficiently large set S of gate-automorphism pairs. To this end, divide [n] into $\lfloor \frac {n}{k^{\prime }+2}\rfloor $ disjoint sets S _i of size $k^{\prime }+2$ and ignore the elements left over. It follows that for each i there is a permutation σ _i which fixes [n]∖S _i pointwise but moves g, as otherwise it implies $|{\mathsf {SP}(g)}| \le n - (k^{\prime }+2)+1 = n - k^{\prime } -1$ which directly contradicts the bound of $n - |{\mathsf {SP}(g)}| \le k^{\prime }$. Since g is moved by each σ _i and C is rigid, there must be an associated child h _i∈H with σ _i h _i∉H. Thus let (h _i,σ _i) be the gate-automorphism pair for S _i, these pairs are useful. Let Q _i be the union of all the parts of S P(h _i) except the largest part together with all the parts of S P(σ _i h _i) except the largest part. Consider a σ _j which fixes Q _i pointwise, then, by the construction of Q _i, $\sigma _{j} \in {\text {Stab}_{n}(\mathsf {SP}(h_{i}))} \cap {\text {Stab}_{n}(\mathsf {SP}(\sigma _{i} h_{i}))}$. This implies σ _j fixes both h _i and σ _i h _i.

Define a directed graph K on the sets S _i as follows. Include an edge from S _i to S _j, with i≠j, if $Q_{i} \cap S_{j} \neq \emptyset $. An edge in K indicates a potential lack of independence between (h _i,σ _i) and (h _j,σ _j), and on the other hand if there are no edges between S _i and S _j, the associated pairs are independent (as, for example, $Q_{i} \cap S_{j} = \emptyset $ implies $Q_{i} \subseteq [n] {\backslash } S_{j}$ so that σ _i fixes Q _i pointwise). Thus it remains to argue that K has a large independent set. This is possible because the out-degree of S _i in K is bounded by

$$|Q_{i}| \le \|{\mathsf{SP}(h_{i})}\| + \|{\mathsf{SP}(\sigma_{i} h_{i})}\| \le 2\cdot \frac{33}{\epsilon}\frac{\log s}{\log n} $$

as the sets S _i are disjoint and Lemma 6 can be applied to h _i. Thus the average total degree (in-degree + out-degree) of K is at most $2|Q_{i}| \le 18k^{\prime }$. Greedily select a maximal independent set in K by repeatedly selecting the S _i with the lowest total degree and eliminating it and its neighbours. This action does not affect the bound on the average total degree of K and hence determines an independent set I in K of size at least

$$\frac{\lfloor\frac{n}{k^{\prime}+2}\rfloor}{18 k^{\prime}+1} \ge \frac{n-(k^{\prime}+2)}{(18k^{\prime}+1 k^{\prime}+2)} \ge \frac{\frac{n}{2}-1}{18k^{\prime2}+37k^{\prime}+2} \ge \frac{\frac{7}{16}n}{18k^{\prime2}+37k^{\prime}+2} \ge \frac{n}{(12 k^{\prime})^{2}} $$

where the first inequality follows by expanding the floored expression, the second follows because $k^{\prime } < \frac {n}{2}$, the third follows from the lower bound on n, and the last follows because $k^{\prime } \ge 1$ as it is the ceiling of a positive non-zero quantity by definition.

Take S:={(h _i,σ _i) | S _i∈I}. By the argument above S is useful and independent. By the above claim, conclude that $s \ge |\text {Orb}(g)| \ge |\text {Orb}(H)| \ge 2^{|S|} \ge 2^{\frac {n}{(12k^{\prime })^{2}}}.$ For $\epsilon \ge \frac {2}{3}$, $s \le 2^{n^{1-\epsilon }}$, and $\frac {\epsilon }{96} \log n > 1$ the following is a contradiction $\log s \ge n \cdot (\frac {96}{\epsilon }\frac {\log s}{\log n})^{-2} > n \cdot (n^{1-\epsilon })^{-2} = n^{2\epsilon -1} \ge n^{1-\epsilon }.$ Thus $|{\mathsf {SP}(g)}| \le \frac {n}{2}$ for all g∈C and the proof is complete by Lemma 6.

Observe that when s is polynomial in n the support of a rigid symmetric circuit family is asymptotically constant. This is the case for polynomial-size families.

Corollary 1

Let ${\mathcal {C}}$ be a polynomial-size rigid symmetric circuit family, then $\mathsf {SP}(\mathcal {C}) = O(1)$.

4 Translating Symmetric Circuits to Formulas

In this section, we deploy the support theorem to show that P-uniform families of polynomial-size symmetric circuits can be translated into formulas of fixed-point logic. As a first step, we argue in Section 4.1 that we can restrict our attention to rigid circuits, by showing that every symmetric circuit can be converted, in polynomial time, into an equivalent rigid symmetric circuit. In Section 4.2 we show that there are polynomial-time algorithms that will determine whether a circuit is symmetric and, if so, compute for every gate its coarsest supporting partition and therefore its canonical support. In Section 4.3 we give an inductive construction of a relation that associates to each gate g of C a set of tuples that when assigned to the support of g result in g being evaluated to true. This construction is turned into a definition in fixed-point logic in Section 4.4.

4.1 Rigid Circuits

We first argue that rigid circuits uniquely induce automorphisms.

Proof Proof of Proposition 1

Let σ∈Sym_n induce the automorphisms $\pi , \pi ^{\prime }$ of C. We show $\pi g = \pi ^{\prime } g$ for all gates g in C, and hence $\pi = \pi ^{\prime }$.

Observe that if g is an output gate, the image of g under any automorphism induced by σ must be Ω(σΩ⁻¹(g)), because Ω is a function, and hence $\pi g = \pi ^{\prime } g$ is unique and completely determined by σ. Therefore assume that g is not an output gate. We proceed by induction on the height of g to show that $\pi g = \pi ^{\prime } g$.

In the base case g is an input gate. If g is a constant gate, g is the only constant gate of its type and hence all automorphisms of C must fix it. If g is a relational gate, g is the only relational gate with its type Σ(g) and label Λ(g) and it must map to the similarly unique gate with type Σ(g) and tuple σΛ(g) and hence $\pi g = \pi ^{\prime } g$.

In the induction step g is an internal gate. By rigidity of C, g is unique for its children and type. Moreover, by induction the children of g map in the same way under π and $\pi ^{\prime }$, and hence the image of g must be the same in both automorphisms. Thus $\pi g = \pi ^{\prime } g$ for all gates of C.

To see that any symmetric circuit can be transformed in polynomial time into an equivalent rigid symmetric circuit, observe that we can proceed inductively from the input gates, identifying gates whenever they have the same label and the same set of children. This allows us to establish the following lemma.

Lemma 7

Let C=〈G,W,Ω,Σ,Λ〉 be a $(\mathbb {B},\tau )$ -circuit on structures of size n. There is a deterministic algorithm which runs in time poly(|C|) and outputs a rigid $(\mathbb {B},\tau )$ -circuit $C^{\prime }$ with gates $G^{\prime } = G$ such that for any g∈G, any input τ-structure ${\mathcal {A}}$ and any bijection γ from A to [n], $C[\gamma {\mathcal {A}}](g) = C^{\prime }[\gamma {\mathcal {A}}](g)$ . Moreover, $C^{\prime }$ is symmetric if C is.

Proof

Partition the internal gates of G into equivalence classes where gates in the same class share the same operation, and have the same output markings and children. If C is rigid every class has size one, otherwise there is at least one class containing two gates.

Let E be a minimum height equivalence class containing at least two gates (here, the height of a gate is the length of a longest path from it to an input). Order the gates in E: g ₁,g ₂,…,g _|E|. For each gate f∈G∖E, let c _f denote the number of wires from E to f, and note that c _f≤|E|. For all gates in E remove all outgoing wires. For all gates E∖{g ₁}: (i) remove all input wires, and (ii) set their operation to AND. For each i, 1≤i≤|E|−1, add a wire from g _i to g _i+1. For each f∈G∖E and i∈[|E|], add a wire from g _i to f if c _f≥i. This completes the transformation of the gates in E.

We now argue that this does not affect the result computed at any gate g. First observe that no output gates appear in E, because Ω is injective and hence each output gate must be the sole member of its equivalence class. All gates in E originally had identical sets of children and labels and hence they must have evaluated to the same value. The modifications made do not change this property as g ₁ computes the value it originally would have, then passes this value to the other gates in E, along a chain of single input AND gates. The modifications to the outgoing wires of E insure that each gate that originally took input from E has the same number of inputs from E (each with the same value) in the modified circuit. Taken together this means that the result computed at any gate in the modified circuit is the same as that computed at that gate in C.

We next argue that the local modification of E makes strict progress towards producing a rigid circuit $C^{\prime }$. The local modification of E can only change equivalence classes above E because the changes to the output wires of E are the only thing that can possibly affect other equivalence classes. After the modification all gates in E must be in singleton equivalence classes because each gate in E is designed to have a unique set of children.

Applying the above local modification simultaneously to all topologically minimal non-singleton equivalence classes of C, until none remain, produces a rigid circuit $C^{\prime }$ that computes the same query as C, because, as we have just argued, equivalence classes cannot grow as a result of this local modification. Moreover, this must happen after at most |C| many local modifications, because the number of equivalence classes is at most |C|.

We now show that this transformation preserves symmetry. Suppose C is symmetric. Fix any permutation σ∈Sym_n. Let π be an automorphism induced by σ on C. Observe that any induced automorphism on C must map equivalence classes to equivalence classes because labels and children are preserved. It is easy to translate π into an induced automorphism of $C^{\prime }$. Let E and $E^{\prime }$ be two topologically-minimal equivalence classes such that $\pi E = E^{\prime }$ where g ₁,…,g _|E| and $g_{1}^{\prime },\ldots ,g_{|E^{\prime }|}^{\prime }$ are the ordering of the gates in E and $E^{\prime }$ in $C^{\prime }$, respectively. It can be argued by induction that mapping g _i to $g_{i}^{\prime }$ for all $1 \le i \le |E|=|E^{\prime }|$ preserves all labels and wires and hence is an induced automorphism of σ in $C^{\prime }$. Since σ is arbitrary, we conclude that the resulting circuit is symmetric.

The construction of equivalence classes and, indeed, the overall construction of $C^{\prime }$ can be easily implemented in time polynomial in |C| when given the circuit in a reasonable binary encoding. Finally, as gates are only being rewired and relabeled, $G = G^{\prime }$.

4.2 Computing Supports

By Lemma 7, we know that there is a polynomial-time algorithm that converts a circuit into an equivalent rigid circuit while preserving symmetry. In this subsection we show how to, in polynomial time, check whether the resulting circuit is symmetric, and if it is, compute the support of each gate. To this end we first describe an algorithm for determining induced automorphisms of a rigid circuit.

Lemma 8

Let C be a rigid $(\mathbb {B},\tau )$ -circuit on structures of size n and σ∈Sym _n . There is a deterministic algorithm which runs in time poly(|C|) and outputs for each gate g∈G its image under the automorphism π induced by σ, if it exists.

Proof

Process the gates of C recursively building up a mapping π. Compute the mapping for the children of a gate g before determining the mapping for g. If at any point an image for g cannot be located, halt and output that there is no induced automorphism.

Let g be a constant gate, then g is fixed under every automorphism. Let g be a relational gate, then there is at most one gate $g^{\prime }$ in C with $\Sigma (g) = \Sigma (g^{\prime })$, $\sigma \Lambda (g) = \Lambda (g^{\prime })$, and $\sigma \Omega ^{-1}(g) = \Omega ^{-1}(g^{\prime })$. If $g^{\prime }$ exists, set π g to $g^{\prime }$, otherwise halt with failure. Similarly, when g is an internal gate use Σ, Ω, and the action of π on the children of G (via W) to determine a unique image of g, if it exists.

By Proposition 1 if σ induces an automorphism of C, it is unique and will be discovered by the above algorithm. This algorithm clearly runs in time polynomial in |C|.

Using the preceding lemma we can determine whether a given rigid circuit is symmetric by computing the set of automorphisms induced by transpositions of the universe. If an induced automorphism fails to exist the circuit cannot be symmetric. Otherwise, it must be symmetric because such transpositions generate the symmetric group. If the circuit is symmetric, the coarsest supporting partitions and orbits of each gate can be determined by examining the transitive closure of the action of the automorphisms induced by transpositions on the universe and the gates, respectively.

Lemma 9

Let C be a rigid $(\mathbb {B},\tau )$ -circuit for structures of size n. There is a deterministic algorithm which runs in time poly(|C|) and decides whether C is symmetric. If C is symmetric the algorithm also outputs the orbits and coarsest supporting partitions of every gate.

Proof

For all transpositions (u v)∈Sym_n run the algorithm of Lemma 8 to determine the unique automorphism π _{(u
v)} of C induced by (u v), if it exists. Output that C is symmetric iff every induced automorphism π _{(u
v)} exists. This is correct because the set of transpositions generates all of Sym_n, and therefore the automorphisms π _{(u
v)} generate all induced automorphisms of C.

If C is symmetric, these induced automorphisms also indicate the supporting partitions and orbits of each gate g. Let $\mathcal {P}_{(uv)} := {\{{\{u,v}}\}\} \cup _{w \in [n] {\backslash } \{u,v}\} \{\{w\}\}$ be a partition of [n]. Note that π _{(u
v)} fixes g iff $\mathcal {P}_{(uv)}$ supports g. Let $\mathcal {P}$ be the partition determined by combining the partitions $\mathcal {P}_{(uv)}$ which support g using $\mathcal {E}$. Proposition 2 implies that $\mathcal {P}$ supports g. Suppose $\mathcal {P}$ is not the coarsest partition supporting g. Then, there exists u,v∈[n] which are not in the same part of $\mathcal {P}$ but in the same part of some partition supporting g. But by the definition of $\mathcal {P}$, π _{(u
v)} cannot fix g—a contradiction. Therefore $\mathcal {P}$ is the coarsest partition supporting g.

To compute the orbit of a gate g: Start with S ₀:={g}, and for i≥0, compute $S_{i+1} := S_{i} \cup _{(uv) \in {\text {Sym}_{[n]}}} \pi _{(uv)} S_{i}$. Let S be the least fixed point of this process. We argue that S=Orb(g). $S \subseteq \text {Orb}(g)$, because it consists of gates reachable from g via a sequence of induced automorphisms of C. $S \supseteq \text {Orb}(g)$, because the set of automorphisms induced by transpositions generate the group of all induced automorphisms. (This algorithm for orbit finding is well-known, c.f., e.g., [12].)

Since there are only $\binom {n}{2}$ transpositions, and we can determine whether there is an induced automorphism for each transposition in time poly(|C|), we can determine whether C is symmetric in time poly(|C|). If C is symmetric the computation of the supports and orbits of all gates also is computed in time poly(|C|) because each output is completely determined by the equivalence classes induced by the relations defined by the induced automorphisms π _{(u
v)}. Therefore the overall algorithm runs in time poly(|C|).

4.3 Succinctly Evaluating Symmetric Circuits

Let ${\mathcal {C}} = (C_{n})_{n \in {\mathbb {N}}}$ be a family of polynomial-size rigid symmetric circuits computing a q-ary query. Let n ₀ be a constant sufficient to apply the Support Theorem to C _n for n≥n ₀ and fix such an n. By Theorem 4, there is a constant bound k so that for each gate g in C _n the union of all but the largest part of the coarsest partition supporting g, S P(g), has at most k elements. Moreover, this union is a support of g in the sense of Definition 7. We call it the canonical support of g and denote it by sp(g).

Consider a structure ${\mathcal {A}}$ with universe U of size n. In this subsection we show that how a gate g evaluates in C _n with respect to ${\mathcal {A}}$ depends only on the injective partial mapping of U to the elements in the canonical support of g (and not a complete bijection $\gamma : U \rightarrow [n]$). This allows us to succinctly encode the bijections which make a gate true (first as injective partial functions and then as tuples). This ultimately lets us build a fixed-point formula for evaluating C _n—indeed, all symmetric circuits—in the next subsection.

For any set $X \subseteq [n]$, let ${U}^{\underline {X}}$ denote the set of injective functions from X to U. For $X, Y \subseteq [n]$ and $\alpha \in {U}^{\underline {X}}, \beta \in {U}^{\underline {Y}}$, we say α and β are consistent, denoted α∼β, if for all $z \in X \cap Y, \alpha (z) = \beta (z)$, and for all x∈X∖Y and y∈Y∖X, α(x)≠β(y). Recall that any bijection $\gamma : U \rightarrow [n]$ determines an evaluation of the circuit C _n on the input structure ${\mathcal {A}}$ which assigns to each gate g the Boolean value $C_{n}[\gamma {\mathcal {A}}](g)$. (Note that $\gamma ^{-1} \in {U}^{\underline {[n]}}$.) Let g be a gate and let $\Gamma (g) := {\{{\gamma }\;|\;{C_{n}[\gamma {\mathcal {A}}](g) = 1}\}}$ denote the set of those bijections which make g evaluate to 1. The following lemma proves that the membership of γ in Γ(g) (moreover, the number of 1s input to g) depends only on what γ maps sp(g) to.

Lemma 10

Let g be a gate in C _n with children H. Let $\alpha \in {U}^{\underline {{\text {sp}(g)}}}$ , then for all $\gamma _{1}, \gamma _{2} : U \rightarrow [n]$ with $\gamma _{1}^{-1} \sim \alpha $ and $\gamma _{2}^{-1} \sim \alpha $,

γ ₁ ∈Γ(g) iff γ ₂ ∈Γ(g).

|{h∈H | γ ₁ ∈Γ(h)}|=|{h∈H|γ ₂ ∈Γ(h)}|.

Proof

There is a unique permutation π∈Sym_n such that π γ ₁=γ ₂. Moreover, π fixes spg pointwise, since $\gamma _{1}^{-1}$ and $\gamma _{2}^{-1}$ are consistent with α. Since C _n is rigid and symmetric, π is an automorphism of C _n, and we have that $C_{n}[\gamma _{1}{\mathcal {A}}](g) = C_{n}[(\pi \gamma _{1}){\mathcal {A}}](\pi g)$. Since π fixes sp(g) pointwise, we have π g=g and therefore $C_{n}[\gamma _{1}{\mathcal {A}}](g) = C_{n}[(\pi \gamma _{1}){\mathcal {A}}](g) = C_{n}[\gamma _{2}{\mathcal {A}}](g)$, proving part 1. Similarly, for any child h∈H we have that $C_{n}[\gamma _{1}{\mathcal {A}}](h) = C_{n}[(\pi \gamma _{1}){\mathcal {A}}](\pi h) = C_{n}[\gamma _{2}{\mathcal {A}}](\pi h)$. Since π fixes g, π fixes H setwise. As this establishes a bijection between the children H that evaluate to 1 for γ ₁ and γ ₂, we conclude part 2.

We associate with each gate g a set of injective functions $\text {EV}_{g} \subseteq {U}^{\underline {{\text {sp}(g)}}}$ defined by $\text {EV}_{g} := {\{{\alpha \in {U}^{\underline {{\text {sp}(g)}}}}\;|\;{\exists \gamma \in \Gamma (g) \wedge \alpha \sim \gamma ^{-1}}\}}$ and note that, using Lemma 10, this completely determines Γ(g). We can use the following lemma to recursively construct EV_g for all gates in C.

Lemma 11

Let g be a gate in C with children H. Let $\alpha \in {U}^{\underline {{\text {sp}(g)}}}$ , then for all $\gamma : U \rightarrow [n]$ with γ ⁻¹ ∼α,

$$ \hfill |{\{{ h \in H}\;|\;{\gamma \in \Gamma(h)}\}}| = \sum\limits_{h \in H} \frac{|A_{h} \cap \text{EV}_{h}|}{|A_{h}|}, \hfill $$

(9)

where for h∈H, $A_{h} := {\{{\beta \in {U}^{\underline {{\text {sp}(h)}}}}\;|\;{\alpha \sim \beta }\}}$.

Proof

Write χ _Γ(h) for the characteristic (or indicator) function of Γ(h). We have,

$$\begin{array}{@{}rcl@{}} |{\{{ h \in H}\;|\;{\gamma \in \Gamma(h)}\}}|&\cdot& |{\{{\delta \in {U}^{\underline{[n]}}}\;|\;{\delta \sim \alpha}\}}|\\ &=& \sum\limits_{{\{{\delta \in {U}^{\underline{[n]}}}\;|\;{ \delta \sim \alpha}\}}} |{\{{h \in H}\;|\;{\delta^{-1} \in \Gamma(h)}\}}|\\ &=& \sum\limits_{h \in H} \sum\limits_{{\{{\delta \in {U}^{\underline{[n]}}}\;|\;{ \delta \sim \alpha}\}}} \chi_{\Gamma(h)}(\delta^{-1})\\ &=& \sum\limits_{h \in H} \sum\limits_{\beta \in A_{h}} \sum\limits_{{\{{\delta \in {U}^{\underline{[n]}}}\;|\;{ \delta \sim \alpha \wedge \delta \sim \beta}\}}} \chi_{\Gamma(h)}(\delta^{-1})\\ &=& \sum\limits_{h \in H} \sum\limits_{\beta \in A_{h}} |{\{{\beta \in \text{EV}_{h}}\}}| \cdot |{\{{\delta \in {U}^{\underline{[n]}}}\;|\;{ \delta \sim \alpha \wedge \delta \sim \beta}\}}|\\ \end{array} $$

(10)

where the first equality follows from Lemma 10 Part 2, the second by linearity of addition (note that |{δ ⁻¹∈Γ(h)}|∈{0,1}), the third by the definitions of ∼ and A _h, and the fourth by the definition of EV_h. Observe that as β ranges over A _h, the sets ${\{{\delta \in {U}^{\underline {[n]}}}\;|\;{ \delta \sim \alpha \wedge \delta \sim \beta }\}}$ are pairwise disjoint and all have the same size. Thus, $|A_{h}|\cdot |{\{{\delta \in {U}^{\underline {[n]}}}\;|\;{ \delta \sim \alpha \wedge \delta \sim \beta }\}}| = |{\{{\delta \in {U}^{\underline {[n]}}}\;|\;{ \delta \sim \alpha }\}}|$, and we conclude that

$$|{\{{ h \in H}\;|\;{\gamma \in \Gamma(h)}\}}| = \sum\limits_{h \in H} \sum\limits_{\beta \in A_{h}} \frac{|{\{{\beta \in \text{EV}_{h}}\}}|}{|A_{h}|} = \sum\limits_{h\in H} \frac{|A_{h} \cap \text{EV}_{h}|}{|A_{h}|}. $$

Note that implicit in the lemma is that the r.h.s. side of (9) is integral.

Since [n] is linearly ordered, $X \subseteq [n]$ inherits this order and we write X for the ordered |X|-tuple consisting of the elements of X in the inherited order. For $\alpha \in {U}^{\underline {\mathbf {X}}}$ we write ${\alpha } \in {U}^{\underline {\mathbf {X}}}$ to indicate the |X|-tuple resulting from applying α to each component of X in order. Observe that this transformation is invertible. This allows us to succinctly encode such injective functions as tuples over U and, further, to write relational analogs of the sets of injective functions we considered before, e.g., E V _g:={α | α∈EV_g}, and A _h={α | α∈A _h}. Using Lemma 11 it is easy to recursively define E V _g over C _n.

Let g be a constant input gate, then sp(g) is empty. If Σ(g)=0, then Γ(g)=∅ and E V _g=∅. Otherwise Σ(g)=1, then Γ(g) is all bijections and E V _g={〈〉}, i.e., the set containing the empty tuple.
Let g be a relational gate with Σ(g)=R∈τ, then sp(g) is the set of elements in the tuple Λ_R(g). By definition we have
$${\mathbf{EV}}_{g} = {\{{{\alpha} \in {U}^{\underline{{{\mathbf{sp}}(g)}}}\;|\;{\alpha (\Lambda_{R}(g)) \in R^{{\mathcal{A}}}}\}}}. $$
Let Σ(g)=AND and consider ${\alpha } \in {U}^{\underline {{{\mathbf {sp}}(g)}}}$. By Lemma 11, α∈E V _g iff ${\mathbf {A}_{h}} \subseteq {\mathbf {EV}}_{h}$ for every child h of g, i.e., for every child h and every $\beta \in {U}^{\underline {{\text {sp}(h)}}}$ with α∼β, we have β∈E V _h.
Let Σ(g)=OR and consider ${\alpha } \in {U}^{\underline {{{\mathbf {sp}}(g)}}}$. By Lemma 11, α∈E V _g iff there is a child h of g where ${\mathbf {A}_{h}} \cap {\mathbf {EV}}_{h}$ is non-empty, i.e., for some child h of g and some $\beta \in {U}^{\underline {{\mathbf {sp}(h)}}}$ with α∼β, we have β∈E V _h.
Let Σ(g)=NAND and consider ${\alpha } \in {U}^{\underline {{{\text {sp}}(g)}}}$. By Lemma 11, α∈E V _g iff there is a child h of g where ${\mathbf {A}_{h}} \not \subseteq {\mathbf {EV}}_{h}$, i.e., for some child h and some $\beta \in {U}^{\underline {{\mathbf {sp}(h)}}}$ with α∼β, we have β∉E V _h.
Let Σ(g)=MAJ and consider ${\alpha } \in {U}^{\underline {{{\mathbf {sp}}(g)}}}$. Let H be the set of children of g. Then Lemma 11 implies that α∈E V _g if, and only if,
$$ \hfill \sum\limits_{h \in H} \frac{| \mathbf{A}_{h} \cap {\mathbf{EV}}_{h}|}{|\mathbf{A}_{h}|} \ge \frac{|H|}{2}. \hfill $$

(11)

From EV we can recover the q-ary query Q computed by C _n=〈G,W,Ω,Σ,Λ〉 on the input structure ${\mathcal {A}}$ because the support of an output gate g∈G is exactly the set of elements in the marking of g by Λ_Ω. In particular:

$$Q = {\{{\bar a \in U^{q}}\;|\;{\exists g \in G, \alpha \in {\mathbf{EV}}_{g}\text{ such that} \Lambda_{\Omega}(\alpha^{-1}(\bar a)) = g}\}}. $$

For Boolean properties q=0, and Q={〈〉} indicates that ${\mathcal {A}}$ has the property and Q=∅ indicates that it does not.

4.4 Translating to Formulas of FP

Let ${\mathcal {C}} = (C_{n})_{n \in {\mathbb {N}}}$ be a P-uniform family of polynomial-size symmetric $(\mathbb {B},\tau )$ circuits, where $\mathbb {B}$ is either $\mathbb {B}_{\text {std}}$ or $\mathbb {B}_{\text {maj}}$. Our aim is to show that there is a formula Q of FP, or FPC in the case of $\mathbb {B}_{\text {maj}}$, in the vocabulary τ⊎{≤} such that for any n and τ-structure ${\mathcal {A}}$ over a universe U with |U|=n, the q-ary query defined by C _n on input ${\mathcal {A}}$ is defined by the formula Q when interpreted in the structure ${\mathcal {A}}^{\le } := {\mathcal {A}} \uplus {\langle {[n],\le }\rangle }$.

Since ${\mathcal {C}}$ is P-uniform, by the Immerman-Vardi theorem and Lemma 7, we have an FP interpretation defining a rigid symmetric circuit equivalent to C _n—that we also call C _n—over the number sort of ${\mathcal {A}}^{\le }$, i.e., a sequence $\Phi := (\phi _{G}, \phi _{W}, \phi _{\Omega },(\phi _{s})_{s \in \mathbb {B} \uplus \tau \uplus {\{{0,1}\}}}, (\phi _{\Lambda _{R}})_{R\in \tau })$ of formulas of FP(≤) that define the circuit when interpreted in 〈[n],≤〉. Note that C _n is defined over the universe [n]. Let t be the arity of the interpretation, i.e., ϕ _G defines a t-ary relation $G \subseteq [n]^{t}$. If n is less than n ₀, the length threshold for applying the support theorem, C _n can trivially be evaluated by a FP formula which quantifies over all (constantly-many) bijections from the point sort of ${\mathcal {A}}^{\le }$ to the number sort of ${\mathcal {A}}^{\le }$ and then directly evaluates the circuit with respect to the bijection. Thus we only need to consider the case when n≥n ₀, and are able to use the recursive construction of $\vec {\text {EV}}_{}$ from the Section 4.3 along with a constant bound k on the size of the gate supports in C _n.

A small technical difficulty arises from the fact that we want to define the relation $\vec {\text {EV}}_{g}$ inductively, but these are actually relations of varying arities, depending on the size of sp(g). For the sake of a uniform definition, we extend $\vec {\text {EV}}_{g}$ to a k-ary relation for all g by padding it with all possible values to obtain tuples of length k. If |sp(g)|=ℓ≤k, define

$$\overline{\text{EV}}_{g} = {\{{(a_{1}\cdots a_{k})}\;|\;{(a_{1}\cdots a_{\ell}) \in {\mathbf{EV}}_{g} \text{ and} a_{i} \neq a_{j} \text{ for} i \neq j}\}}. $$

Define the relation $V \subseteq [n]^{t} \times U^{k}$ by $V(g,\bar a)$ if, and only if, $\bar a \in \overline {\text {EV}}_{g}$. Our aim is to show that the relation V is definable by a formula of FP. Throughout this subsection we use μ and ν to indicate t-tuples of number variables which denote gate indexes in [n]^t, and use the k-tuples of point variables $\bar x = (x_{1},\ldots ,x_{k})$ and $\bar y = (y_{1},\ldots , y_{k})$ to denote injective functions that have been turned into tuples and then padded.

By Lemma 9 and invoking the Immerman-Vardi theorem again, we have a formula SUPP such that 〈[n],≤〉⊧SUPP[g,u] if, and only if, 〈[n],≤〉⊧ϕ _G[g] (i.e., g is a gate of C _n as defined by the interpretation Φ) and u is in sp(g). We use SUPP to define some additional auxiliary formulas. First we define, for each i with 1≤i≤k a formula SUPP_i such that 〈[n],≤〉⊧SUPP_i[g,u] if, and only if, u is the i ^{t
h} element of sp(g). These formulas can be defined inductively as follows, where η is a number variable

$$\begin{array}{rcl} \textsc{supp}_{1}(\mu,\eta) & := & \textsc{supp}(\mu,\eta) \land \forall \chi (\chi < \eta) \implies \neg\textsc{supp}(\mu,\chi) \\ \textsc{supp}_{i+1}(\mu,\eta) & := & \textsc{supp}(\mu,\eta) \land \exists \chi_{1} (\chi_{1} < \eta \land \textsc{supp}_{i}(\mu,\chi_{1}) \\ & & \land \forall \chi_{2} [(\chi_{1} < \chi_{2} < \eta) \implies \neg\textsc{supp}(\mu,\chi_{2})]) . \end{array} $$

We now define a formula $\textsc {agree}(\mu ,\nu ,\bar {x},\bar {y})$ so that for a structure ${\mathcal {A}}$, ${\mathcal {A}}^{\leq } \models \textsc {agree}[g,h,\bar {a},\bar {b}]$ if, and only if, α∼β for $\vec \alpha \in {U}^{\underline {{{\text {sp}}(g)}}}$, $\vec \beta \in {U}^{\underline {{{\text {sp}}(h)}}}$ that are the restrictions of the k-tuples $\bar {a}$ and $\bar {b}$ to the length of sp(g) and sp(h) respectively.

$$\begin{array}{lr} \textsc{agree}(\mu,\nu,\bar{x},\bar{y}) := & \end{array} $$

$$\begin{array}{ll} \displaystyle \bigwedge_{1\leq i,j, \leq k} & (\forall \eta (\textsc{supp}_{i}(\mu,\eta) \land \textsc{supp}_{j}(\nu,\eta)) \implies x_{i} = y_{j}) \land \\ & (\forall \eta_{1} \eta_{2} (\textsc{supp}_{i}(\mu,\eta_{1}) \land \textsc{supp}_{j}(\nu,\eta_{2}) \land x_{i} = y_{j}) \implies \eta_{1} = \eta_{2}) \end{array} $$

With these, we now define a series of formulas $(\theta _{s})_{s \in \mathbb {B} \uplus \tau \uplus {\{{0,1}\}}}(\mu ,x)$ corresponding to the various cases of the construction of the relation E V _g from Section 4.3. In these, V is a relational variable for the relation being inductively defined.

$$\begin{array}{rcll} \theta_{0}(\mu,\bar{x}) & := & \text{false} \\ \theta_{1}(\mu,\bar{x}) & := & \displaystyle \bigwedge_{1\leq i<j \leq k} x_{i} \neq x_{j} \\ \theta_{R}(\mu,\bar{x}) & := & \displaystyle \bigwedge_{1\leq i<j \leq k} x_{i} \neq x_{j} \land \exists z_{1}\cdots z_{r} \exists \eta_{1}\cdots \eta_{r} R(z_{1},\ldots,z_{r}) \land \phi_{\Lambda_{R}}(\mu,\eta) \land \\ & & \hspace{23ex} \displaystyle \bigwedge_{1\leq i \leq r} \bigwedge_{1\leq j \leq k} (\textsc{supp}_{j}(\mu,\eta_{i}) \implies z_{i} = x_{j}) \\ \theta_{\text{OR}}(\mu,\bar{x}) & := & \displaystyle \bigwedge_{1\leq i<j \leq k} x_{i} \neq x_{j} \land \exists \nu \exists \bar{y} (W(\nu,\mu) \land \textsc{agree}(\mu,\nu,\bar{x},\bar{y}) \land V(\nu,\bar{y})) \\ \theta_{\text{AND}}(\mu,\bar{x}) & := & \displaystyle \bigwedge_{1\leq i<j \leq k} x_{i} \neq x_{j} \land \forall \nu \forall \bar{y} ((W(\nu,\mu) \land \textsc{agree}(\mu,\nu,\bar{x},\bar{y})) \implies V(\nu,\bar{y})) \\ \theta_{\text{NAND}}(\mu,\bar{x}) & := & \displaystyle \bigwedge_{1\leq i<j \leq k} x_{i} \neq x_{j} \land \exists \nu \exists \bar{y} (W(\nu,\mu) \land \textsc{agree}(\mu,\nu,\bar{x},\bar{y}) \land \neg V(\nu,\bar{y})) \end{array} $$

To define 𝜃 _MAJ we start with some observations. We wish to formalise (11), but there are a few complications. The k- a r y relation $\overline {\text {EV}}_{h}$ we are defining inductively is the result of padding E V _h with all tuples of k−|sp(h)| distinct elements. Thus the number of elements in $\overline {\text {EV}}_{h}$ is $|{\mathbf {EV}}_{h}|\cdot \frac {(n-|{\text {sp}(h)}|)!}{(n-k)!}$. Similarly, for any fixed g, h and $\bar a$, if we write $\bar {A}_{h}$ for the set of tuples $\bar b$ satisfying $\textsc {agree}(g,h,\bar a,\bar b)$, then $|\bar {A}_{h}| = |\mathbf {A}_{h}|\cdot \frac {(n-|{\text {sp}(h)}|)!}{(n-k)!}$. Finally, the tuples in $\bar {A}_{h} \cap \overline {\text {EV}}_{h}$ are exactly those obtained by padding tuples in $\mathbf {A}_{h} \cap {\mathbf {EV}}_{h}$ to length k and there are therefore $|\mathbf {A}_{h} \cap {\mathbf {EV}}_{h}|\cdot \frac {(n-|{\text {sp}(h)}|)!}{(n-k)!}$ many of these. Thus, $\frac {|\vec A_{h} \cap \vec {\text {EV}}_{h}|}{|\vec A_{h}|} = \frac {| \bar {A}_{h} \cap \overline {\text {EV}}_{h}|}{|\bar {A}_{h}|}$ and it suffices to compute the latter. Observe that $|\vec A_{h}|$ and $|\bar {A}_{h}|$ are completely determined by |sp(g)|, |sp(h)| and $|{\text {sp}(g)} \cap {\text {sp}(h)}|$. We avoid dealing explicitly with fractions by noting that for any gate h, the sum $\sum _{h^{\prime } \in \text {Orb}(h)} \frac {| \vec {A}_{h^{\prime }} \cap \vec {\text {EV}}_{h^{\prime }} |}{|\vec {A}_{h^{\prime }}|}$ is an integer (by an argument analogous to Lemma 11). Since $|\bar {A}_{h^{\prime }}|$ is the same for all $h^{\prime } \in \text {Orb}(h)$, it suffices to compute the sum of $| \bar {A}_{h^{\prime }} \cap \overline {\text {EV}}_{h^{\prime }} |$ for all $h^{\prime }$ with a fixed size of $|\bar {A}_{h}|$ and then divide the sum by $|\bar {A}_{h}|$. This is what we use to compute the sum on the l.h.s. of (11).

For any fixed i and j with 0≤i≤j≤k, define the formula OVERLAP_{i
j}(μ,ν) so that ${\mathcal {A}}^{\leq } \models \textsc {overlap}_{ij}[g,h]$ iff |sp(h)|=j and $|{\text {sp}(g)}\cap {\text {sp}(h)}| = i$. This formula can be defined in FO.

Using k-tuples of number variables in FPC we can represent natural numbers less than n ^k. We assume, without giving a detailed construction of the formulas involved, that we can define arithmetic operations on these numbers. In particular, we assume we have for each i,j as above a formula ASIZE_{i
j}(μ,ξ), with ξ a k-tuple of number variables, such that ${\mathcal {A}}^{\leq } \models \textsc {asize}_{ij}[g,e]$ iff $e = |\bar {A}_{h}|$ for any gate h with |sp(h)|=j and $|{\text {sp}(g)}\cap {\text {sp}(h)}| = i$.

Using this, we define the formula $\textsc {num}_{ij}(\mu ,\bar {x},\xi )$, with ξ a k-tuple of number variables, so that ${\mathcal {A}}^{\leq } \models \textsc {num}_{ij}[g,\bar a,e]$ iff e is the number of gates h with ${\mathcal {A}}^{\leq } \models \textsc {overlap}_{ij}[g,h]$ which are made true by some bijection that assigns the tuple $\bar a$ to sp(g). This formula is given by

$$\begin{array}{lr} \textsc{num}_{ij}(\mu,\bar{x},\xi) := & \end{array} $$

$$\begin{array}{ll} \exists \xi_{1} \xi_{2} & \textsc{asize}_{ij}(\mu,\xi_{1}) \land \\ & \xi_{2} = \#_{\nu \bar y}(W(\nu,\mu) \land \textsc{overlap}_{ij}(\mu,\nu) \land V(\nu,\bar{y}) \land \textsc{agree}(\mu,\nu,\bar{x},\bar{y}) ) \land \\ & \xi \cdot \xi_{1} = \xi_{2}. \end{array} $$

Now we can define the required formula 𝜃 _MAJ by

$$\theta_{\text{MAJ}}(\mu,\bar{x}) := $$

$$\displaystyle \bigwedge_{1\leq i<j \leq k} x_{i} \neq x_{j} \land \exists \xi (2\cdot \xi \geq \#_{\nu} W(\nu,\mu)) \land \xi = \sum\limits_{0\leq i \leq j \leq k} {\{{\xi^{\prime}}\;|\;{\textsc{num}_{ij}(\mu,\bar{x},\xi^{\prime})}\}}, $$

where the sum inside the formula is to be understood as shorthand for taking the sum over the bounded number of possible values of i and j.

Now, we can define the relation $V \subseteq [n]^{t} \times U^{k}$ given by $V(g,\bar a)$ if, and only if, $\bar a \in \overline {\text {EV}}_{g}$ by the following formula

$$\theta(\mu,\bar x) := [{\text{ifp}}_{V,\nu \bar y} \displaystyle \bigvee_{s \in \mathbb{B} \uplus \tau \uplus {\{{0,1}\}}} (\phi_{s}(\mu) \land \theta_{s}(\nu,\bar y))](\mu,\bar x). $$

The overall q-ary output query computed by the circuit is given by the following formula derived from the final construction in the last subsection

$$Q(z_{1},\ldots,z_{q}) := $$

$$\begin{array}{l} \exists \mu\bar x \nu_{1} \cdots \nu_{q} \eta_{1} \cdots \eta_{k} [ \theta(\mu, \bar x) \wedge \phi_{\Omega}(\nu_{1},\ldots,\nu_{q}, \mu) \wedge \\ \hspace{22ex} \bigwedge_{1 \le i \le k} (\textsc{supp}_{i}(\mu,\eta_{i}) \vee \forall \eta [\neg \textsc{supp}_{i}(\mu,\eta)]) \wedge \\ \hspace{22ex} \bigwedge_{1 \le i \le k} \bigwedge_{1 \le j \le q} ([\textsc{supp}_{i}(\mu,\eta_{i}) \wedge x_{i} = z_{j}] \!\implies\! \nu_{j} \!= \eta_{i}) \wedge \\ \hspace{22ex}\bigwedge_{1 \le j \le q} \bigvee_{1 \le i \le k} (x_{i} = z_{j} \wedge \textsc{supp}_{i}(\mu,\eta_{i}))] \end{array} $$

where the purpose of the last three lines is to invert the injective function encoded in $\bar {x}$ and then apply it to z _i to produce ν _i; in particular: the second line puts the ordered support of μ into η ₁,…,η _k, the third line defines the map from z _i to ν _i, and the fourth line ensures that this map covered all coordinates of z _i.

Note that this is a formula of FP+≤ if $\mathbb {B}$ is the standard basis and a formula of FPC if $\mathbb {B}$ is the majority basis. Moreover, if the family ${\mathcal {C}} = (C_{n})_{n \in {\mathbb {N}}}$ of polynomial-size symmetric circuits is not uniform, but given by an advice function Υ, the construction gives us an equivalent formula of FP+Υ (for the standard basis) or FPC+Υ (for the majority basis). This may be formalised as follows.

Lemma 12

Any relational query defined by a P-uniform family of polynomial-size symmetric circuits over the standard basis is definable in FP+≤.

Any relational query defined by a P-uniform family of polynomial-size symmetric circuits over the majority basis is definable in FPC.

Any relational query defined by a P-uniform family of polynomial-size symmetric circuits over the standard basis is definable in FP+Υ, for some advice function Υ.

5 Consequences

Formulas of FP+≤ can be translated into P-uniform families of polynomial-size symmetric Boolean circuits by standard methods (see [16]) and similar translations hold for FPC and FP+Υ. This combined with Lemma 12 proves our main theorem.

Theorem 5 (Main)

The following pairs of classes define the same queries on structures:

Symmetric P-uniform polynomial-size Boolean circuits and FP+≤.

Symmetric P-uniform polynomial-size majority circuits and FPC.

Symmetric polynomial-size majority circuits and FPC+Υ.

One consequence is that properties of graphs which we know not to be definable in FPC are also not decidable by P-uniform families of polynomial-size symmetric circuits. The results of Cai-Fürer-Immerman [4] give graph properties that are polynomial-time decidable, but not definable in FPC. Furthermore, there are a number of NP-complete graph problems known not to be definable in FPC, including Hamiltonicity and 3-colourability (see [6]). This contrasts with a number of graph properties that have been shown to be definable in FPC, including graphs that have perfect matchings [2] and any proper minor-closed class of graphs (see [13]).

The proofs establishing that the above-mentioned properties are not definable in FPC actually show that these properties are not even definable in the infinitary logic with a bounded number of variables and counting ($C^{\omega }_{\infty \omega }$—see [16]). For our purposes, we can think of formulas of this infinitary logic as families $(\phi _{n})_{n\in {\mathbb {N}}}$ of formulas of first-order logic with counting quantifiers ( FOC) such that there is a $k \in {\mathbb {N}}$ so that no formula ϕ _n uses more than k variables. Such a family defines the class ${\mathcal {C}}$ of structures such that ${\mathcal {A}} \in {\mathcal {C}}$ iff $|{\mathcal {A}}| = n$ and ${\mathcal {A}} \models \phi _{n}$. It is not difficult to show that formulas of FPC+Υ can be translated into $C^{\omega }_{\infty \omega }$, using the fact that for any vocabulary τ there is a k such that any property of τ-structures with at most n elements can be expressed by a first-order formula with at most k variables (see [8]). This gives us the following.

Corollary 2

Hamiltonicity and 3-colourability of graphs are not decidable by polynomial-size families of symmetric majority circuits.

We can say more about the correspondence between the infinitary logic $C^{\omega }_{\infty \omega }$ and symmetric circuits. In the proof of the Support Theorem (Theorem 4), we only use the upper bound on the size of the circuits to bound the size of orbits of individual gates. This motivates the following definition (cp. Definition 12 below).

Definition 10

A family of symmetric $(\mathbb {B},\tau )$-circuits ${\mathcal {C}} = (C_{n})_{n \in {\mathbb {N}}}$ is orbit-polynomial if there is polynomial p such that for any gate g in C _n, the orbit of g in C _n under the action of Sym_n has size at most p(n).

Then the following strengthening of Corollary 1 is a direct consequence of the proof of Theorem 4.

Corollary 3

Let ${\mathcal {C}}$ be an orbit-polynomial rigid symmetric circuit family, then $\mathsf {SP}(\mathcal {C}) = O(1)$.

It is not hard to see that a formula of $C^{\omega }_{\infty \omega }$ can be translated into an orbit-polynomial family of symmetric majority circuits. This is by the standard translation of a formula ϕ _n of FOC into a circuit C _n with majority gates. This creates a gate for each pair (ψ,a) where ψ is a sub-formula of ϕ _n and a is a tuple from [n] that acts as an assignment to the free variables of ψ. The orbit of the gate (ψ,a) is the set of all gates (ψ,π a) for π∈Sym_n. Since the number of free variables of ψ and hence the length of a is bounded by a constant k, we see that all orbits have size at most n ^k. Moreover, a simple adaptation of the translation of Section 4.4 shows that any family of orbit-polynomial symmetric circuits can be translated into a formula of $C^{\omega }_{\infty \omega }$. This is obtained by translating each circuit C _n into a formula of FOC. Once n is fixed, we do not need fixed-points to define the relations $\overline {\text {EV}}_{g}$ as the recursion can be unfolded to give a first-order formula. Moreover, the maximum number of free variables occurring in any sub-formula is given by a function of the size of the supports sp(g). We avoid the fixed-points introduced by the use of the Immerman-Vardi theorem by invoking the fact that on ordered structures of a fixed signature τ and a fixed size n, we can express any property using a first-order formula with a constant number of variables (see [8]). Together these establish that the total number of variables required in our formulas is bounded by a constant. Taken all together, this establishes the following.

Theorem 6

A query is decidable by an orbit-polynomial family of symmetric majority circuits if and only if it is definable in $C^{\omega }_{\infty \omega }$.

6 Coherent and Locally Polynomial Circuits

In this section we discuss connections with the prior work of Otto [17]. Otto studies rigid symmetric Boolean circuits deciding Boolean properties of structures and provides uniformity conditions on such families that characterise bounded-variable fragments of finite and infinitary first-order logic. Otto defines two properties to establish his notion of uniformity. The first property is called coherence; informally, a circuit family $(C_{n})_{n \in {\mathbb {N}}}$ is coherent if C _n appears as a subcircuit of all but finitely many of the circuits at larger input lengths.

Definition 11 (Coherence)

Let ${\mathcal {C}} := (C_{n})_{n \in {\mathbb {N}}}$ be a family of rigid symmetric $(\mathbb {B}_{\text {std}},\tau )$-circuits computing a Boolean function. The circuit C _n embeds into the circuit C _m with m>n if there is a subcircuit of C _m which is isomorphic to C _n. An embedding is complete if its images are exactly those gates of C _m which are fixed by Sym[m]∖[n]. The circuit family $\mathcal {C}$ is coherent if for each $n \in \mathbb {N}$, C _n completely embeds into C _m for all large enough m>n.

The second property is locally polynomial; informally, a circuit family is locally polynomial if the size of the orbit of every wire is polynomially bounded.

Definition 12 (Locally Polynomial)

A rigid circuit family $(C_{n})_{n \in {\mathbb {N}}}$ is locally polynomial of degree k if there is a $k \in {\mathbb {N}}$ such that each C _n and every subset $S \subseteq [n]$, the size of the orbit of every wire with respect to the automorphisms of the circuit induced by Sym_S is at most |S|^k.

The main result of [17, Theorem 6] establishes an equivalence between coherent locally-polynomial (of degree k) families of rigid symmetric $(\mathbb {B}_{\text {std}},\tau )$-circuits computing Boolean functions on fin[τ] and infinitary first-order logic with k variables. It should be noted that in Otto’s definition of circuit families the individual circuits in the family may themselves be infinite, as the only size restriction is on the orbits of gates. The theorem also shows that if the circuit families are also constant depth they correspond to the fragment of first-order logic with k variables.

The common restriction of notions of uniformity we consider in this paper is that the circuits have size polynomial in their input length. If we restrict ourselves to locally-polynomial coherent symmetric families where the individual circuits are finite, we can use the Support Theorem (Corollary 1) to establish a direct connection with polynomial-size symmetric circuit families, formally stated in the following proposition.

Proposition 3

Let ${\mathcal {C}} := (C_{n})_{n \in {\mathbb {N}}}$ be a family of finite rigid symmetric Boolean circuits.

If ${\mathcal {C}}$ is a locally-polynomial coherent family, then ${\mathcal {C}}$ is polynomial size.

If ${\mathcal {C}}$ is polynomial size, then ${\mathcal {C}}$ is locally polynomial.

Proof

We prove the two parts separately.

Suppose to the contrary that C _n has s(n)=ω(poly(n)) gates. Because ${\mathcal {C}}$ is locally polynomial the Support Theorem gives a bound $k \in {\mathbb {N}}$ on the size of the support of gates in ${\mathcal {C}}$. Take $m \in {\mathbb {N}}$ such that C _m is a circuit such that C _k completely embeds into C _m and s(k)⋅m ^k<s(m), such m exists because ${\mathcal {C}}$ is coherent and s is super polynomial. By symmetry and averaging there are at least $\frac {s(m)}{m^{k}}$ gates of C _m whose supports are drawn from [k]. These gates are necessarily fixed by Sym_[m]∖[k]. Since the embedding is complete, C _k maps onto at least these gates. But this is a contradiction because $s(k) < \frac {s(m)}{m^{k}}$. Thus ${\mathcal {C}}$ has polynomially many gates.
If ${\mathcal {C}}$ has polynomially many gates then the Support Theorem immediately implies that the supports of all gates in ${\mathcal {C}}$ is bounded by some $k \in {\mathbb {N}}$. Therefore for every $S \subseteq [n]$ every wire in $C_{n} \in {\mathcal {C}}$ has its orbit size bounded by |S|^2k. This is exactly the definition of locally polynomial.

Since there are properties definable in an infinitary logic with finitely many variables that are not decidable by polynomial-size circuits, it follows from the above proposition that the use of infinite circuits is essential in Otto’s result.

Proposition 3 implies that all uniform circuit families we consider are locally polynomial. However, it does not establish an equivalence between a circuit family having polynomially many gates and being locally polynomial and coherent. Indeed there are Boolean circuit families uniformly definable in FO+≤ that are not coherent. To see this observe that such circuit families may include gates that are completely indexed by the number sort and hence are fixed under all automorphisms induced by permutations of the point sort. Moreover the number of such gates may increase as a function of input length. However, because coherence requires that complete embedding exist, the number of gates in each circuit of a coherent family that are not moved by any automorphism must be identical. Thus there are uniform circuits that are not coherent.

Consider weakening the definition of coherence to require only that an embedding exists but not that the embedding is complete, and call this partial coherence. One can show that any relation which can be computed by a Boolean circuit family uniformly definable in FO+≤ can also be computed by a partially coherent Boolean circuit family with the same uniformity by appropriately creating copies of circuits relativised for all shorter lengths. We omit any formal discussion of this construction.

7 Future Directions

One of our original motivations for studying symmetric majority circuits was the hope that they had the power of choiceless polynomial time with counting (CPTC) [3], and that, perhaps, techniques from circuit complexity could improve our understanding of the relationship between CPTC and the invariant queries definable in polynomial-time. However, because ${\text {FPC}} \subsetneq {\text {CPTC}}$ [9], our results indicate that symmetry is too much of restriction on P-uniform circuit families to recover CPTC.

A natural way to weaken the concept of symmetry is to require that induced automorphisms exist only for a certain subgroup of the symmetric group. This interpolates between our notion of symmetric circuits and circuits on linearly-ordered structures, with the latter case occurring when the subgroup is trivial. An easier first step may be to consider the action on structures with a finite number of disjoint sorts and require only that automorphisms be induced by permutations which preserve the sorts, e.g., structures interpreting Boolean matrices whose rows and columns are indexed by disjoint sets.

The Support Theorem is a fairly general statement about the structure of symmetric circuits and is largely agnostic to the particular semantics of the basis. To that end the Support Theorem may find application to circuits over bases not consider here. The Support Theorem can be applied to arithmetic circuits computing invariant properties of matrices over a field; e.g., the Permanent polynomial is invariant and one standard way to compute it is as a symmetric arithmetic circuit, i.e., Ryser’s formula [18].

Known inexpressibility results for FPC and $C^{\omega }_{\infty \omega }$ often give explicit lower bounds on the number of variables required to express a problem. It may be instructive to translate these into size lower bounds for symmetric circuits. One barrier to obtaining exponential lower bounds is that the Support Theorem has a subexponential bound built into it. Perhaps the form of the Support Theorem can be improved as the particular bound required on the orbit size does not appear to be fundamental to the conclusion of the Support Theorem. Inspired by the proof of Theorem 29 in [5], one approach might be to apply the O’Nan-Scott Theorem to more tightly characterise the stabilizer group of a gate.

Acknowledgments

The authors thank Dieter van Melkebeek for looking at an early draft of this paper, and Joanna Fawcett for useful comments.

Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

Open Access

previous article A Solution to Wiehagen’s Thesis

next article 2-Stack Sorting is Polynomial

This basis is universal in the sense that every Boolean function can be computed by some circuit with gates from this basis. Indeed the basis containing only NAND is universal as AND and OR operations can be computed using several NAND operations. We permit the use of AND and OR gates to make several constructions easier.

Formally one must define a particular way of encoding circuits via binary strings. However, since the details of the representation are largely irrelevant for our purposes we omit them.

Note that this definition of support is different than the group-theoretic support of a permutation, i.e., for a permutation π∈Sym_n,support(π):={x∈[n] | π x≠x}.

By interpreting partitions as equivalence relations one can can alternatively view ${\mathcal {E}}(\mathcal {P},\mathcal {P}^{\prime })$ as the relational join of $\mathcal {P}$ and $\mathcal {P}^{\prime }$.

Anderson, M., Dawar, A.: On symmetric circuits and fixed-point logics. In: 31st International Symposium on Theoretical Aspects of Computer Science, volume 25, pages 41–52 (2014)

Anderson, M., Dawar, A., Holm, B.: Maximum matching and linear programming in fixed-point logic with counting (2013)

Blass, A., Gurevich, Y., Shelah, S.: Choiceless polynomial time. Annals of Pure and Applied Logic 100, 141–187 (1999)MathSciNetCrossRefMATH

Cai, J-Y., Fürer, M., Immerman, N.: An optimal lower bound on the number of variables for graph identification. Combinatorica 12(4), 389–410 (1992)MathSciNetCrossRefMATH

Clote, P., Kranakis, E.: Boolean functions, invariance groups, and parallel complexity. SIAM J. Comput. 20(3), 553–590 (1991)MathSciNetCrossRefMATH

Dawar, A.: A restricted second order logic for finite structures. Inf. Comput. 143, 154–174 (1998)MathSciNetCrossRefMATH

Dawar, A., Gurevich, Y.: Fixed point logics. Bull. Symb. Log. 8, 65–88 (2002)MathSciNetCrossRefMATH

Dawar, A., Lindell, S., Weinstein, S.: First order logic, fixed point logic and linear order. In: Kleine-Büning, H. (ed.) Computer Science Logic ’95, volume 1092 of LNCS, pages 161–177. Springer-Verlag (1996)

Dawar, A., Richerby, D., Rossman, B.: Choiceless polynomial time, counting and the Cai–Fürer–Immerman graphs. Annals of Pure and Applied Logic 152(1), 31–50 (2008)MathSciNetCrossRefMATH

10.

Denenberg, L., Gurevich, Y., Shelah, S.: Definability by constant-depth polynomial-size circuits. Inf. Control. 70(2), 216–240 (1986)MathSciNetCrossRefMATH

11.

Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Springer (1999)

12.

Furst, M., Hopcroft, J., Luks, E.: Polynomial-time algorithms for permutation groups. In: Proceedings of the Twenty-First Annual ACM Symposium on Foundations of Computer Science, pages 36–41. IEEE (1980)

13.

Grohe, M.: Fixed-point definability and polynomial time on graphs with excluded minors. J. ACM 59(5), 27:1–27:64 (2012)MathSciNetCrossRefMATH

14.

Immerman, N.: Relational queries computable in polynomial time. Inf. Control. 68(1-3), 86–104 (1986)MathSciNetCrossRefMATH

15.

Immerman, N.: Descriptive Complexity Theory. Springer (1999)

16.

Otto, M.: Bounded Variable Logics and Counting: A Study in Finite Models, volume 9 of Lecture Notes in Logic. Springer-Verlag (1997)

17.

Otto, M.: The logic of explicitly presentation-invariant circuits. In: Dalen, D., Bezem, M. (eds.) Computer Science Logic, volume 1258 of Lecture Notes in Computer Science, pages 369–384. Springer Berlin Heidelberg (1997)

18.

Ryser, H.J.: Combinatorial Mathematics. Mathematical Association of America (1963)

19.

Vardi, M.: The complexity of relational query languages (1982)

20.

Vollmer, H.: Introduction to Circuit Complexity: A Uniform Approach. Springer-Verlag Berlin Heidelberg (1999)

Title: On Symmetric Circuits and Fixed-Point Logics
Authors: Matthew Anderson
Anuj Dawar
Publication date: 13-07-2016
Publisher: Springer US
Published in: Theory of Computing Systems / Issue 3/2017
Print ISSN: 1432-4350
Electronic ISSN: 1433-0490
DOI: https://doi.org/10.1007/s00224-016-9692-2

Springer Professional

On Symmetric Circuits and Fixed-Point Logics

Abstract

Open Access

1 Introduction

2 Preliminaries

2.1 Vocabularies, Structures, and Logics

2.2 Symmetric and Uniform Circuits

3 Symmetry and Support

3.1 Supporting Partitions

3.2 Support Theorem

4 Translating Symmetric Circuits to Formulas

4.1 Rigid Circuits

4.2 Computing Supports

4.3 Succinctly Evaluating Symmetric Circuits

4.4 Translating to Formulas of FP

5 Consequences

6 Coherent and Locally Polynomial Circuits

7 Future Directions

Acknowledgments

Open Access

Premium Partner

Springer Professional

Abstract

Open Access

1 Introduction

2 Preliminaries

2.1 Vocabularies, Structures, and Logics

2.2 Symmetric and Uniform Circuits

3 Symmetry and Support

3.1 Supporting Partitions

3.2 Support Theorem

4 Translating Symmetric Circuits to Formulas

4.1 Rigid Circuits

4.2 Computing Supports

4.3 Succinctly Evaluating Symmetric Circuits

4.4 Translating to Formulas of FP

5 Consequences

6 Coherent and Locally Polynomial Circuits

7 Future Directions

Acknowledgments

Open Access

Other articles of this Issue 3/2017

Higher Randomness and Forcing with Closed Sets

New Bounds and Extended Relations Between Prefix Arrays, Border Arrays, Undirected Graphs, and Indeterminate Strings

On Boolean Closed Full Trios and Rational Kripke Frames

2-Stack Sorting is Polynomial

Partition Expanders

Editor’s Note

Premium Partner