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.