Feedback vertex sets

FeedbackVertexSet is Karp's problem FEEDBACK NODE SET [Kar72], problem GT7 of Garey and Johnson for directed graphs: given a directed graph G and a number k, some set of at most k declared vertices meets every directed cycle; that is, removing it leaves an acyclic graph (Cslib.Complexity.mem_FeedbackVertexSet_iff_forall_isDirCycle). Graphs are read as directed graphs on their declared vertices (Cslib.Complexity.Graph.IsDirCycle), so a self-loop is a cycle of length one, and instances are encoded with the graph (encGraph) and k in binary (encNat) (Cslib.Complexity.FeedbackVertexSetInstance, encoded by Cslib.Complexity.encFeedbackVertexSet).

NP membership uses a list of numbers as the witness, read along the vertex list (Cslib.Complexity.colorOf): the vertices numbered 0 are removed, at most k of them, and every arc between remaining vertices must increase the number. Such a numbering exists exactly when removing the vertices numbered 0 leaves an acyclic graph, by topological numbering (Cslib.Complexity.Graph.isDirAcyclic_iff_exists_rank), and it can be taken at most the number of declared vertices.

Hardness is Karp's reduction from VertexCover (VertexCover.toFeedbackVertexSet): every edge between distinct vertices becomes two opposite arcs (VertexCover.bidirect), so the directed cycles of length two are the edges, every directed cycle contains an edge, and the feedback vertex sets are the vertex covers. Since VertexCover rejects targets above the number of distinct declared vertices, such targets are mapped to a fixed graph without feedback vertex set of size 0.

Main definitions

• Cslib.Complexity.FeedbackVertexSetInstance, Cslib.Complexity.encFeedbackVertexSet.
• Cslib.Complexity.FeedbackVertexSet.
• Cslib.Complexity.VertexCover.bidirect, Cslib.Complexity.VertexCover.toFeedbackVertexSet.

Main results

• Cslib.Complexity.mem_FeedbackVertexSet_iff_forall_isDirCycle: the removed vertices meet every directed cycle.
• Cslib.Complexity.FeedbackVertexSet.mem_NP: FeedbackVertexSet ∈ NP encFeedbackVertexSet.
• Cslib.Complexity.VertexCover.toFeedbackVertexSet_mem_iff, Cslib.Complexity.VertexCover.computableInPolyTime_toFeedbackVertexSet, Cslib.Complexity.polyTimeReducible_VertexCover_FeedbackVertexSet: Karp's reduction.
• Cslib.Complexity.FeedbackVertexSet_npHard, Cslib.Complexity.FeedbackVertexSet_npComplete: FeedbackVertexSet is NP-complete.

References

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

structure Cslib.Complexity.FeedbackVertexSetInstance : Type

An instance (graph, bound) of Feedback Vertex Set.

• graph : Graph

  The directed graph whose directed cycles must be hit.

• bound : ℕ

  The maximum number of vertices to remove.

theorem Cslib.Complexity.FeedbackVertexSetInstance.ext {x y : FeedbackVertexSetInstance} (graph : x.graph = y.graph) (bound : x.bound = y.bound) : x = y

theorem Cslib.Complexity.FeedbackVertexSetInstance.ext_iff {x y : FeedbackVertexSetInstance} : x = y ↔ x.graph = y.graph ∧ x.bound = y.bound

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqFeedbackVertexSetInstance : DecidableEq FeedbackVertexSetInstance

def Cslib.Complexity.instDecidableEqFeedbackVertexSetInstance.decEq (x✝ x✝¹ : FeedbackVertexSetInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instReprFeedbackVertexSetInstance : Repr FeedbackVertexSetInstance

def Cslib.Complexity.instReprFeedbackVertexSetInstance.repr : FeedbackVertexSetInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instInhabitedFeedbackVertexSetInstance : Inhabited FeedbackVertexSetInstance

@[reducible, inline]

abbrev Cslib.Complexity.encFeedbackVertexSetFields : Graph × ℕ ↪ List Bool

The tuple of the fields of encFeedbackVertexSet.

theorem Cslib.Complexity.encFeedbackVertexSet_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {T0 S0 x1 T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn encGraph T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { graph := x0 x, bound := x1 x }) encIn encFeedbackVertexSet (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

def Cslib.Complexity.encFeedbackVertexSet : FeedbackVertexSetInstance ↪ List Bool

Encoding of FeedbackVertexSetInstance as a pair (graph, bound).

@[simp]

theorem Cslib.Complexity.encFeedbackVertexSet_apply (a : FeedbackVertexSetInstance) : encFeedbackVertexSet a = encFeedbackVertexSetFields (a.graph, a.bound)

theorem Cslib.Complexity.encFeedbackVertexSet_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Graph} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn encGraph budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { graph := x0 x, bound := x1 x }) encIn encFeedbackVertexSet budget

theorem Cslib.Complexity.encFeedbackVertexSet_bound_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → FeedbackVertexSetInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encFeedbackVertexSet S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).bound) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.encFeedbackVertexSet_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Graph × ℕ) => { graph := p.1, bound := p.2 }) encFeedbackVertexSetFields encFeedbackVertexSet 1 1

theorem Cslib.Complexity.encFeedbackVertexSet_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : FeedbackVertexSetInstance) => (a.graph, a.bound)) encFeedbackVertexSet encFeedbackVertexSetFields 1 1

theorem Cslib.Complexity.encFeedbackVertexSet_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn encGraph) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { graph := x0 x, bound := x1 x }) encIn encFeedbackVertexSet

theorem Cslib.Complexity.encFeedbackVertexSet_graph_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → FeedbackVertexSetInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encFeedbackVertexSet → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph

theorem Cslib.Complexity.encFeedbackVertexSet_bound_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → FeedbackVertexSetInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encFeedbackVertexSet → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).bound) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encFeedbackVertexSet_bound_deg : Turing.MultiTapeTM.ComputableInDegree FeedbackVertexSetInstance.bound encFeedbackVertexSet Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encFeedbackVertexSet_graph_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → FeedbackVertexSetInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encFeedbackVertexSet S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph S✝

theorem Cslib.Complexity.encFeedbackVertexSet_graph_deg : Turing.MultiTapeTM.ComputableInDegree FeedbackVertexSetInstance.graph encFeedbackVertexSet encGraph 1 1

theorem Cslib.Complexity.encFeedbackVertexSet_bound_inO : Turing.MultiTapeTM.ComputableInO FeedbackVertexSetInstance.bound encFeedbackVertexSet Turing.MultiTapeTM.encNat (fun (a : FeedbackVertexSetInstance) => (encFeedbackVertexSet a).length) fun (a : FeedbackVertexSetInstance) => (encFeedbackVertexSet a).length

theorem Cslib.Complexity.encFeedbackVertexSet_graph_inO : Turing.MultiTapeTM.ComputableInO FeedbackVertexSetInstance.graph encFeedbackVertexSet encGraph (fun (a : FeedbackVertexSetInstance) => (encFeedbackVertexSet a).length) fun (a : FeedbackVertexSetInstance) => (encFeedbackVertexSet a).length

def Cslib.Complexity.FeedbackVertexSet : Set FeedbackVertexSetInstance

Feedback vertex set [Kar72] Garey and Johnson, Problem GT7: the directed graphs with a number k such that removing some set of at most k declared vertices leaves no directed cycle.

theorem Cslib.Complexity.mem_FeedbackVertexSet_iff {G : Graph} {k : ℕ} : { graph := G, bound := k } ∈ FeedbackVertexSet ↔ ∃ (R : Finset ℕ), (∀ v ∈ R, v ∈ G.vertices) ∧ R.card ≤ k ∧ (G.deleteVerts R).IsDirAcyclic

theorem Cslib.Complexity.mem_FeedbackVertexSet_iff_forall_isDirCycle {G : Graph} {k : ℕ} : { graph := G, bound := k } ∈ FeedbackVertexSet ↔ ∃ (R : Finset ℕ), (∀ v ∈ R, v ∈ G.vertices) ∧ R.card ≤ k ∧ ∀ (c : List ℕ), G.IsDirCycle c → ∃ v ∈ c, v ∈ R

Membership in FeedbackVertexSet through cycles: at most k declared vertices meet every directed cycle.

Membership in NP

theorem Cslib.Complexity.FeedbackVertexSet.mem_NP : FeedbackVertexSet ∈ NP encFeedbackVertexSet

FeedbackVertexSet belongs to NP, with a listed numbering as the witness.

Reduction from vertex covers

def Cslib.Complexity.VertexCover.bidirect (G : Graph) : Graph

Both arcs of every edge between distinct vertices: the directed graph whose cycles of length two are the edges.

theorem Cslib.Complexity.VertexCover.dirAdj_bidirect {G : Graph} {u v : ℕ} : (bidirect G).DirAdj u v ↔ u ∈ G.vertices ∧ v ∈ G.vertices ∧ G.toSimpleGraph.Adj u v

The arcs of bidirect G join the adjacent declared vertices of G.

def Cslib.Complexity.VertexCover.toFeedbackVertexSet (x : VertexCoverInstance) : FeedbackVertexSetInstance

Karp's reduction from VertexCover: keep the target and make every edge two opposite arcs, or produce a self-loop with target 0 when the target exceeds the number of distinct declared vertices.

theorem Cslib.Complexity.VertexCover.toFeedbackVertexSet_mem_iff (x : VertexCoverInstance) : toFeedbackVertexSet x ∈ FeedbackVertexSet ↔ x ∈ VertexCover

Vertex covers are feedback vertex sets of the bidirected graph.

theorem Cslib.Complexity.VertexCover.computableInPolyTime_toFeedbackVertexSet : Turing.MultiTapeTM.ComputableInPolyTime toFeedbackVertexSet encVertexCoverInstance encFeedbackVertexSet

Karp's reduction is polynomial-time: the number of distinct declared vertices is computed in unary and compared with the binary target.

theorem Cslib.Complexity.polyTimeReducible_VertexCover_FeedbackVertexSet : PolyTimeReducible encVertexCoverInstance encFeedbackVertexSet VertexCover FeedbackVertexSet

VertexCover reduces to FeedbackVertexSet in polynomial time [Kar72].

theorem Cslib.Complexity.FeedbackVertexSet_npHard : NPHard encFeedbackVertexSet FeedbackVertexSet

FeedbackVertexSet is NP-hard.

theorem Cslib.Complexity.FeedbackVertexSet_npComplete : NPComplete encFeedbackVertexSet FeedbackVertexSet

Feedback vertex set is NP-complete, for directed graphs with the target in binary [Kar72].