Directed cycles

A graph, given by a list of vertices and a list of edges, is read as a directed graph through its arcs (u, v) ∈ G.edges between declared vertices (Cslib.Complexity.Graph.DirAdj), as for the directed Hamiltonian problems. A directed cycle (Cslib.Complexity.Graph.IsDirCycle) is a nonempty list of distinct declared vertices whose consecutive vertices, read cyclically (Cycle.Chain), are joined by arcs; a vertex with a self-loop is a cycle of length one, and two vertices with arcs both ways form a cycle of length two. A graph is acyclic (Cslib.Complexity.Graph.IsDirAcyclic) when it has no directed cycle.

The feedback set problems remove vertices (Cslib.Complexity.Graph.deleteVerts) or arcs (Cslib.Complexity.Graph.deleteArcs) so as to leave an acyclic graph. Removing vertices leaves an acyclic graph exactly when every directed cycle passes through a removed vertex (Cslib.Complexity.Graph.isDirAcyclic_deleteVerts_iff).

Through Relation.acyclic_iff_forall_nodup_not_cycle_chain, a graph is acyclic exactly when its adjacency relation is Relation.Acyclic, and through Relation.acyclic_iff_exists_rank, exactly when its declared vertices can be numbered below their number so that every arc increases the number (Cslib.Complexity.Graph.isDirAcyclic_iff_exists_rank): a topological numbering. Such numberings, listed along the vertex list, are the NP certificates of the feedback set problems (Cslib.Complexity.mem_NP_of_colorOf).

Main definitions

• Cslib.Complexity.Graph.DirAdj, Cslib.Complexity.Graph.IsDirCycle, Cslib.Complexity.Graph.IsDirAcyclic.
• Cslib.Complexity.Graph.deleteVerts, Cslib.Complexity.Graph.deleteArcs.

Main results

• Cslib.Complexity.Graph.isDirCycle_iff: directed cycles as closed chains of the arc relation.
• Cslib.Complexity.Graph.isDirAcyclic_iff_acyclic: acyclicity of the adjacency relation.
• Cslib.Complexity.Graph.isDirAcyclic_iff_exists_rank, Cslib.Complexity.Graph.exists_rank_of_isDirAcyclic, Cslib.Complexity.Graph.isDirAcyclic_of_rank: acyclicity through topological numberings.
• Cslib.Complexity.Graph.isDirAcyclic_deleteVerts_iff: removed vertices meet every cycle.

References

• M. R. Garey and D. S. Johnson, Computers and Intractability
• R. M. Karp, Reducibility among combinatorial problems

def Cslib.Complexity.Graph.DirAdj (G : Graph) (u v : ℕ) : Prop

The arc relation of a directed graph: an arc (u, v) ∈ G.edges between declared vertices.

def Cslib.Complexity.Graph.IsDirCycle (G : Graph) (c : List ℕ) : Prop

c is a directed cycle of G: a nonempty list of distinct declared vertices whose consecutive vertices, read cyclically, are joined by arcs. A vertex with a self-loop is a cycle of length one.

def Cslib.Complexity.Graph.IsDirAcyclic (G : Graph) : Prop

G is acyclic: it has no directed cycle.

def Cslib.Complexity.Graph.deleteVerts (G : Graph) (R : Finset ℕ) : Graph

Remove the vertices of R: the remaining vertices are those not in R, and the arcs are kept, so that arcs at removed vertices join no declared vertices.

def Cslib.Complexity.Graph.deleteArcs (G : Graph) (S : Finset (ℕ × ℕ)) : Graph

Remove the arcs of S, keeping the vertices.

@[simp]

theorem Cslib.Complexity.Graph.mem_deleteVerts_vertices {G : Graph} {R : Finset ℕ} {v : ℕ} : v ∈ (G.deleteVerts R).vertices ↔ v ∈ G.vertices ∧ v ∉ R

@[simp]

theorem Cslib.Complexity.Graph.deleteVerts_edges (G : Graph) (R : Finset ℕ) : (G.deleteVerts R).edges = G.edges

@[simp]

theorem Cslib.Complexity.Graph.deleteArcs_vertices (G : Graph) (S : Finset (ℕ × ℕ)) : (G.deleteArcs S).vertices = G.vertices

@[simp]

theorem Cslib.Complexity.Graph.mem_deleteArcs_edges {G : Graph} {S : Finset (ℕ × ℕ)} {e : ℕ × ℕ} : e ∈ (G.deleteArcs S).edges ↔ e ∈ G.edges ∧ e ∉ S

theorem Cslib.Complexity.Graph.dirAdj_deleteVerts {G : Graph} {R : Finset ℕ} {u v : ℕ} : (G.deleteVerts R).DirAdj u v ↔ G.DirAdj u v ∧ u ∉ R ∧ v ∉ R

theorem Cslib.Complexity.Graph.dirAdj_deleteArcs {G : Graph} {S : Finset (ℕ × ℕ)} {u v : ℕ} : (G.deleteArcs S).DirAdj u v ↔ G.DirAdj u v ∧ (u, v) ∉ S

theorem Cslib.Complexity.Graph.isDirCycle_iff {G : Graph} {c : List ℕ} : G.IsDirCycle c ↔ c ≠ [] ∧ c.Nodup ∧ Cycle.Chain G.DirAdj ↑c

Directed cycles are the nonempty lists without repetitions that are closed chains of the arc relation between declared vertices.

theorem Cslib.Complexity.Graph.isDirAcyclic_iff_acyclic {G : Graph} : G.IsDirAcyclic ↔ Relation.Acyclic G.DirAdj

Acyclicity through walks: a graph is acyclic exactly when its adjacency relation is acyclic (Relation.Acyclic), that is, when no vertex reaches itself by a nonempty walk along arcs between declared vertices.

theorem Cslib.Complexity.Graph.exists_rank_of_isDirAcyclic {G : Graph} (h : G.IsDirAcyclic) : ∃ (f : ℕ → ℕ), (∀ v ∈ G.vertices, f v < G.vertices.toFinset.card) ∧ ∀ (u v : ℕ), G.DirAdj u v → f u < f v

An acyclic graph has a topological numbering: its declared vertices get numbers below the number of distinct declared vertices, and every arc between declared vertices increases the number.

theorem Cslib.Complexity.Graph.isDirAcyclic_of_rank {G : Graph} {f : ℕ → ℕ} (hf : ∀ (u v : ℕ), G.DirAdj u v → f u < f v) : G.IsDirAcyclic

A numbering that every arc between declared vertices increases shows that a graph is acyclic.

theorem Cslib.Complexity.Graph.isDirAcyclic_iff_exists_rank {G : Graph} : G.IsDirAcyclic ↔ ∃ (f : ℕ → ℕ), (∀ v ∈ G.vertices, f v < G.vertices.toFinset.card) ∧ ∀ (u v : ℕ), G.DirAdj u v → f u < f v

Acyclicity through topological numberings.

theorem Cslib.Complexity.Graph.isDirAcyclic_deleteVerts_iff {G : Graph} {R : Finset ℕ} : (G.deleteVerts R).IsDirAcyclic ↔ ∀ (c : List ℕ), G.IsDirCycle c → ∃ v ∈ c, v ∈ R

Feedback vertex sets meet every cycle: removing the vertices of R leaves an acyclic graph exactly when every directed cycle passes through a vertex of R.