Graph isomorphism in quasipolynomial time

StructureGraph codes#✓fully proved

A graph code consists of a vertex count \(n \in \mathbb{N}\), with vertices \(0, \dots, n-1\), and a Boolean adjacency matrix \(A\) on these vertices that is symmetric (\(A_{ij} = A_{ji}\) for all \(i, j\)) and loop-free (\(A_{ii}\) is false for every \(i\)).

structure GraphCode where
  n : ℕ
  adj : Fin n → Fin n → Bool
  symm : ∀ i j, adj i j = adj j i
  irrefl : ∀ i, adj i i = false

Used by 4

Used byThe quasipolynomial graph isomorphism statement · Bit encoding of a graph code · Bit encoding of a pair of graph codes · Isomorphism of graph codes

DefinitionBinary digits of a natural number#✓fully proved

The binary digits of \(n \in \mathbb{N}\), most significant first, as a list of bits with the digit \(1\) read as true and \(0\) as false; for \(n = 0\) this is the single digit \(0\).

def natBits (n : ℕ) : List Bool :=
  (Nat.toDigits 2 n).map (fun d => decide (d = '1'))

Used by 1

Used byPrefix-free encoding of a natural number

DefinitionPrefix-free encoding of a natural number#✓fully proved

The prefix-free encoding of \(n \in \mathbb{N}\) consists of \(k\) true bits, where \(k\) is the number of binary digits of \(n\), then one false bit, then the binary digits of \(n\), most significant first.

def natToBits (n : ℕ) : List Bool :=
  List.replicate (natBits n).length true ++ [false] ++ natBits n

Uses 1 · Used by 1

Statement usesBinary digits of a natural number

Used byBit encoding of a graph code

DefinitionBit encoding of a graph code#✓fully proved

The bit encoding of a graph code with \(n\) vertices and adjacency matrix \(A\) is the prefix-free encoding of \(n\) followed by the \(n^2\) entries of \(A\), as bits, in row-major order: \(A_{0,0}, A_{0,1}, \dots, A_{0,n-1}, A_{1,0}, \dots, A_{n-1,n-1}\).

def encode (G : GraphCode) : List Bool :=
  natToBits G.n ++
    ((List.finRange G.n).map fun i =>
      (List.finRange G.n).map fun j => G.adj i j).flatten

Uses 2 · Used by 1

Statement usesGraph codes · Prefix-free encoding of a natural number

Used byBit encoding of a pair of graph codes

DefinitionBit encoding of a pair of graph codes#✓fully proved

The bit encoding of a pair \((G, H)\) of graph codes is the bit encoding of \(G\) followed by the bit encoding of \(H\).

def encodePair (p : GraphCode × GraphCode) : List Bool :=
  encode p.1 ++ encode p.2

Uses 2 · Used by 1

Statement usesGraph codes · Bit encoding of a graph code

Used byThe quasipolynomial graph isomorphism statement

DefinitionIsomorphism of graph codes#✓fully proved

Graph codes \(G\) and \(H\) with adjacency matrices \(A\) and \(B\) are isomorphic when they have the same vertex count \(n\) and there is a permutation \(\sigma\) of the vertices \(\{0, \dots, n-1\}\) such that \(A_{ij} = B_{\sigma(i)\sigma(j)}\) for all \(i, j\).

def Isomorphic (G H : GraphCode) : Prop :=
  ∃ h : G.n = H.n, ∃ σ : Equiv.Perm (Fin H.n), ∀ i j : Fin G.n,
    G.adj i j = H.adj (σ (Fin.cast h i)) (σ (Fin.cast h j))

Uses 1 · Used by 1

Statement usesGraph codes

Used byThe quasipolynomial graph isomorphism statement

DefinitionQuasipolynomial time bound#✓fully proved

For an exponent \(c \in \mathbb{N}\) and an input length \(n \in \mathbb{N}\), the quasipolynomial time bound is \(q_c(n) = 2^{(\lfloor \log_2(n+2) \rfloor + 2)^c}\).

def qpTime (c n : ℕ) : ℕ :=
  2 ^ ((Nat.log 2 (n + 2) + 2) ^ c)

Used by 1

Used byThe quasipolynomial graph isomorphism statement

DefinitionThe quasipolynomial graph isomorphism statement#✓fully proved

The proposition that graph isomorphism is decidable in quasipolynomial time: there are a function \(D\) from pairs of graph codes to Booleans, an exponent \(c \in \mathbb{N}\), and a deterministic multi-stack Turing machine with a time function \(t : \mathbb{N} \to \mathbb{N}\) that, on the bit encoding of every pair \((G, H)\), outputs the single bit \(D(G, H)\) within \(t(\ell)\) steps, where \(\ell\) is the length of the encoding, such that \(t(n) \le q_c(n)\) for every \(n \in \mathbb{N}\), where \(q_c\) is the quasipolynomial time bound with exponent \(c\), and \(D(G, H)\) is true if and only if \(G\) and \(H\) are isomorphic.

def conjecture : Prop :=
  ∃ decideGI : GraphCode × GraphCode → Bool, ∃ c : ℕ,
    ∃ h : Turing.TM2ComputableInTime encodePair Computability.encodeBool decideGI,
      (∀ n : ℕ, h.time n ≤ qpTime c n) ∧
      ∀ G H : GraphCode, decideGI (G, H) = true ↔ Isomorphic G H

Sources

• ALG-016.

Uses 4 · Used by 1

Statement usesGraph codes · Isomorphism of graph codes · Bit encoding of a pair of graph codes · Quasipolynomial time bound

Used byBabai's theorem: graph isomorphism in quasipolynomial time

TheoremBabai's theorem: graph isomorphism in quasipolynomial time#●ready to prove

The quasipolynomial graph isomorphism statement holds: there are a function \(D\) from pairs of graph codes to Booleans, an exponent \(c \in \mathbb{N}\), and a deterministic multi-stack Turing machine with a time function \(t : \mathbb{N} \to \mathbb{N}\) that, on the bit encoding of every pair \((G, H)\), outputs the single bit \(D(G, H)\) within \(t(\ell)\) steps, where \(\ell\) is the length of the encoding, such that \(t(n) \le 2^{(\lfloor \log_2(n+2) \rfloor + 2)^c}\) for every \(n \in \mathbb{N}\), and \(D(G, H)\) is true if and only if \(G\) and \(H\) are isomorphic.

Babai (STOC 2016) gave a deterministic quasipolynomial-time graph-isomorphism algorithm; the corrected proof retains that complexity.

public theorem_wanted conjecture_holds : conjecture

Sources

• Babai, L., Graph isomorphism in quasipolynomial time, Proc. 48th ACM Symp. Theory Comput. (STOC 2016), 684-697; arXiv:1512.03547, https://arxiv.org/abs/1512.03547.

Uses 1

Statement usesThe quasipolynomial graph isomorphism statement

8 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.