Digraph Isomorphism, and the degree it defines

DIGRAPH ISOMORPHISM: are the two directed graphs of the instance isomorphic? The vocabulary is the pattern-and-host one of DescriptiveComplexity.Problems.SubgraphIso (FirstOrder.Language.twoGraphs, two marks and two binary relations – nothing asks them to be symmetric, which is what makes this the directed problem), and the yes-instances are the structures whose two marked subgraphs are isomorphic (DescriptiveComplexity.RelIsoOn); as everywhere in the catalog, elements outside both marks are junk that no condition mentions.

The undirected problem, which is what the literature calls graph isomorphism, is DescriptiveComplexity.GraphIso (DescriptiveComplexity.Problems.GraphIso); it reduces to this one by testing simplicity first-order. The converse reduction – the classical digraph-to-graph gadget – is what the degree below is still anchored on this problem for.

Two things make this problem worth its own file.

It is the library's first problem conjecturally neither in P nor NP-complete. Membership is a textbook Σ₁ – guess a binary relation, check first-order that it is a bijection of the pattern vertices onto the host vertices preserving adjacency in both directions – with no order, no counting and no threshold, so DescriptiveComplexity.digraphIso_mem_NP is cheap. No hardness result accompanies it, and none is expected: the problem is in NP, is not known to be in P, and is not known to be NP-complete (Babai 2016 gives a quasipolynomial algorithm; Köbler, Schöning and Torán 1993 is the structural account).

It is one half of the reason DescriptiveComplexity.ComplexityClass.below exists. “GI-complete” is the standard example of completeness for the degree of a problem rather than for a logically defined class. The degree itself (DescriptiveComplexity.GI) is defined on the undirected problem, in DescriptiveComplexity.Problems.GraphIso.Defs, since that is what the literature names GI; this problem is complete for it too (DescriptiveComplexity.digraphIso_GI_complete), the two being interreducible.

There is also a pleasant circularity worth noting: a decision problem in this library is by definition an isomorphism-invariant property of finite structures (DescriptiveComplexity.DecisionProblem), so isomorphism is the problem of deciding the very equivalence the framework quotients by. That reading is DescriptiveComplexity.relIsoOn_iff_equiv: the semantic condition is literally the existence of an equivalence between the two marked sets carrying one adjacency relation to the other.

The problem

def DescriptiveComplexity.HasDigraphIso (A : Type) [FirstOrder.Language.twoGraphs.Structure A] : Prop

The two marked graphs of the instance are isomorphic.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.hasDigraphIso_iso {A B : Type} [FirstOrder.Language.twoGraphs.Structure A] [FirstOrder.Language.twoGraphs.Structure B] (e : FirstOrder.Language.twoGraphs.Equiv A B) : HasDigraphIso A ↔ HasDigraphIso B

The graph-isomorphism property is isomorphism-invariant.

def DescriptiveComplexity.DigraphIso : DecisionProblem FirstOrder.Language.twoGraphs

DIGRAPH ISOMORPHISM, as a problem on pattern-and-host structures: are the two marked directed graphs isomorphic?

Equations

• DescriptiveComplexity.DigraphIso = { Holds := fun (A : Type) (inst : FirstOrder.Language.twoGraphs.Structure A) => DescriptiveComplexity.HasDigraphIso A, iso_invariant := ⋯ }

Membership

noncomputable def DescriptiveComplexity.digraphIsoKernel : subgraphSOLang.Sentence

The first-order kernel of the Σ₁ definition of Digraph Isomorphism: the guessed relation is a bijection of the pattern vertices onto the host vertices, preserving and reflecting adjacency.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.digraphIso_sigmaSODefinable : SigmaSODefinable 1 DigraphIso

Digraph Isomorphism is Σ₁-definable: existentially guess the map, then check first-order that it is a bijection of the pattern vertices onto the host vertices preserving adjacency in both directions. One binary relation variable, no order, no counting, no threshold.

theorem DescriptiveComplexity.digraphIso_mem_NP : NP.Mem DigraphIso

Digraph Isomorphism is in NP: it is Σ₁-definable.