Graph isomorphism and Arthur–Merlin proofs

DefinitionDirected graph isomorphism as a decision problem#✓fully proved

The decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a triple \((n, E_1, E_2)\) of a natural number \(n\) and two lists \(E_1\) and \(E_2\) of pairs of natural numbers for which there is a bijection \(f\) of \(\{0, \dots, n - 1\}\) such that for all \(a, b < n\), \((a, b) \in E_1\) if and only if \((f(a), f(b)) \in E_2\). Bitstrings that do not decode to such a triple are rejected.

Pairs in \(E_1\) or \(E_2\) with an entry at least \(n\) play no role.

noncomputable def graphIsoDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ℕ × List (ℕ × ℕ) × List (ℕ × ℕ)) x with
  | some i => decide (∃ f : Fin i.1 → Fin i.1, Function.Bijective f ∧
      ∀ a b : Fin i.1,
        ((a.val, b.val) ∈ i.2.1 ↔ ((f a).val, (f b).val) ∈ i.2.2))
  | none => false

Uses 9 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Decision problems

Used byGraph isomorphism is in NP and coAM

TheoremGraph isomorphism is in NP and coAM#●ready to prove

The directed graph isomorphism decision problem belongs to NP and to coAM.

public theorem_wanted graph_iso_in_np_coam :
    graphIsoDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧ graphIsoDec ∈ coAM

Sources

• O. Goldreich, "On the complexity of graph isomorphism" and the Goldreich-Micali-Wigderson interactive proof for graph non- isomorphism; see J. Köbler, U. Schöning, and J. Torán, The Graph Isomorphism Problem: Its Structural Complexity, Birkhäuser, 1993.

Uses 5

Statement usesThe class coAM · Directed graph isomorphism as a decision problem · Complexity classes · Decision problems · The complexity class NP

DefinitionDirected graph non-isomorphism as a decision problem#✓fully proved

The decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of triples \((n, E_1, E_2)\) of a natural number and two lists of pairs of natural numbers, to a triple for which there is no bijection \(f\) from \(\{0, \ldots, n - 1\}\) to itself such that, for all \(a, b < n\), \((a, b) \in E_1\) if and only if \((f(a), f(b)) \in E_2\). Bitstrings that do not decode are rejected.

Pairs in \(E_1\) or \(E_2\) with an entry at least \(n\) play no role, so \(E_1\) and \(E_2\) are read as directed graphs on the vertex set \(\{0, \ldots, n - 1\}\).

noncomputable def graphNonIsoDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ℕ × List (ℕ × ℕ) × List (ℕ × ℕ)) x with
  | some i => decide (¬ ∃ f : Fin i.1 → Fin i.1, Function.Bijective f ∧
      ∀ a b : Fin i.1,
        ((a.val, b.val) ∈ i.2.1 ↔ ((f a).val, (f b).val) ∈ i.2.2))
  | none => false

Uses 9 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Decision problems

Used byGraph non-isomorphism is in AM

TheoremGraph non-isomorphism is in AM#●ready to prove

The directed graph non-isomorphism decision problem belongs to the class \(\mathsf{AM}\) of decision problems decided by Arthur–Merlin protocols.

public theorem_wanted graph_noniso_in_am :
    graphNonIsoDec ∈ AM

Sources

• O. Goldreich, S. Micali, and A. Wigderson, "Proofs that yield nothing but their validity, or all languages in NP have zero-knowledge proof systems", Journal of the ACM 38 (1991), 691-729 (FOCS 1986); O. Goldwasser and M. Sipser, "Private coins versus public coins in interactive proof systems", Advances in Computing Research 5 (1989), 73-90.

Uses 4

Statement usesThe class \(\mathsf{AM}\) (Arthur–Merlin) · Directed graph non-isomorphism as a decision problem · Complexity classes · Decision problems

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.