Feedback arc sets

FeedbackArcSet is Karp's problem FEEDBACK ARC SET [Kar72], problem GT8 of Garey and Johnson: given a directed graph G and a number k, removing some set of at most k arcs of G leaves no directed cycle (Cslib.Complexity.Graph.IsDirAcyclic). Graphs are read as directed graphs on their declared vertices, 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.FeedbackArcSetInstance, encoded by Cslib.Complexity.encFeedbackArcSet).

NP membership uses a list of numbers as the witness, read along the vertex list (Cslib.Complexity.colorOf): the arcs between declared vertices that do not increase the number (FeedbackArcSet.backArcs) are removed, and there must be at most k distinct ones. Removing them leaves an acyclic graph, numbered by the witness; conversely, a topological numbering of the graph left by a feedback arc set (Cslib.Complexity.Graph.isDirAcyclic_iff_exists_rank) has all its back arcs in that set, and it can be taken below the number of declared vertices.

Hardness is a vertex-splitting reduction from FeedbackVertexSet (FeedbackVertexSet.toFeedbackArcSet): every vertex v becomes an arc 2v → 2v + 1, and every arc u → v becomes an arc 2u + 1 → 2v (FeedbackVertexSet.splitVertices), with the same k. Every walk passes through the arcs of the vertices it visits, so removing the arcs of a feedback vertex set leaves an acyclic graph; conversely, removing an arc 2v → 2v + 1 or 2v + 1 → 2w can be replaced by removing the vertex v.

Attribution: in Karp's reduction tree [Kar72], FEEDBACK NODE SET and FEEDBACK ARC SET are both reduced from NODE COVER. His FEEDBACK ARC SET reduction splits the vertices of the node-cover instance: ⟨u, 0⟩ → ⟨u, 1⟩ for every vertex u, and ⟨u, 1⟩ → ⟨v, 0⟩ and ⟨v, 1⟩ → ⟨u, 0⟩ for every edge {u, v}. Here the splitting is generalized to arbitrary directed graphs and factored through FeedbackVertexSet. For a loopless graph G, splitVertices (VertexCover.bidirect G) (the graph of VertexCover.toFeedbackVertexSet) is Karp's graph with ⟨u, i⟩ numbered 2u + i. This account of Karp's construction follows secondary descriptions; it has not been checked against the printed paper.

Main definitions

• Cslib.Complexity.FeedbackArcSetInstance, Cslib.Complexity.encFeedbackArcSet.
• Cslib.Complexity.FeedbackArcSet.
• Cslib.Complexity.FeedbackVertexSet.splitVertices, Cslib.Complexity.FeedbackVertexSet.toFeedbackArcSet.

Main results

• Cslib.Complexity.FeedbackArcSet.mem_NP: FeedbackArcSet ∈ NP encFeedbackArcSet.
• Cslib.Complexity.FeedbackVertexSet.toFeedbackArcSet_mem_iff, Cslib.Complexity.FeedbackVertexSet.computableInPolyTime_toFeedbackArcSet, Cslib.Complexity.polyTimeReducible_FeedbackVertexSet_FeedbackArcSet: the reduction.
• Cslib.Complexity.FeedbackArcSet_npHard, Cslib.Complexity.FeedbackArcSet_npComplete: FeedbackArcSet is NP-complete.

References

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

structure Cslib.Complexity.FeedbackArcSetInstance : Type

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

• graph : Graph

  The directed graph whose directed cycles must be hit.

• bound : ℕ

  The maximum number of arcs to remove.

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

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

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqFeedbackArcSetInstance : DecidableEq FeedbackArcSetInstance

def Cslib.Complexity.instDecidableEqFeedbackArcSetInstance.decEq (x✝ x✝¹ : FeedbackArcSetInstance) : Decidable (x✝ = x✝¹)

def Cslib.Complexity.instReprFeedbackArcSetInstance.repr : FeedbackArcSetInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instReprFeedbackArcSetInstance : Repr FeedbackArcSetInstance

@[instance_reducible]

instance Cslib.Complexity.instInhabitedFeedbackArcSetInstance : Inhabited FeedbackArcSetInstance

@[reducible, inline]

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

The tuple of the fields of encFeedbackArcSet.

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

theorem Cslib.Complexity.encFeedbackArcSet_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 encFeedbackArcSet budget

def Cslib.Complexity.encFeedbackArcSet : FeedbackArcSetInstance ↪ List Bool

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

theorem Cslib.Complexity.encFeedbackArcSet_bound_inO : Turing.MultiTapeTM.ComputableInO FeedbackArcSetInstance.bound encFeedbackArcSet Turing.MultiTapeTM.encNat (fun (a : FeedbackArcSetInstance) => (encFeedbackArcSet a).length) fun (a : FeedbackArcSetInstance) => (encFeedbackArcSet a).length

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

theorem Cslib.Complexity.encFeedbackArcSet_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 encFeedbackArcSet (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encFeedbackArcSet_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 encFeedbackArcSet

theorem Cslib.Complexity.encFeedbackArcSet_bound_deg : Turing.MultiTapeTM.ComputableInDegree FeedbackArcSetInstance.bound encFeedbackArcSet Turing.MultiTapeTM.encNat 1 1

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

theorem Cslib.Complexity.encFeedbackArcSet_graph_inO : Turing.MultiTapeTM.ComputableInO FeedbackArcSetInstance.graph encFeedbackArcSet encGraph (fun (a : FeedbackArcSetInstance) => (encFeedbackArcSet a).length) fun (a : FeedbackArcSetInstance) => (encFeedbackArcSet a).length

@[simp]

theorem Cslib.Complexity.encFeedbackArcSet_apply (a : FeedbackArcSetInstance) : encFeedbackArcSet a = encFeedbackArcSetFields (a.graph, a.bound)

theorem Cslib.Complexity.encFeedbackArcSet_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : FeedbackArcSetInstance) => (a.graph, a.bound)) encFeedbackArcSet encFeedbackArcSetFields 1 1

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

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

theorem Cslib.Complexity.encFeedbackArcSet_graph_deg : Turing.MultiTapeTM.ComputableInDegree FeedbackArcSetInstance.graph encFeedbackArcSet encGraph 1 1

def Cslib.Complexity.FeedbackArcSet : Set FeedbackArcSetInstance

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

theorem Cslib.Complexity.mem_FeedbackArcSet_iff {G : Graph} {k : ℕ} : { graph := G, bound := k } ∈ FeedbackArcSet ↔ ∃ (S : Finset (ℕ × ℕ)), (∀ e ∈ S, e ∈ G.edges) ∧ S.card ≤ k ∧ (G.deleteArcs S).IsDirAcyclic

Membership in NP

def Cslib.Complexity.FeedbackArcSet.backArcs (G : Graph) (ρ : List ℕ) : List (ℕ × ℕ)

The arcs between declared vertices that the listed numbering ρ does not increase.

theorem Cslib.Complexity.FeedbackArcSet.mem_backArcs {G : Graph} {ρ : List ℕ} {e : ℕ × ℕ} : e ∈ backArcs G ρ ↔ e ∈ G.edges ∧ e.1 ∈ G.vertices ∧ e.2 ∈ G.vertices ∧ colorOf G ρ e.2 ≤ colorOf G ρ e.1

theorem Cslib.Complexity.FeedbackArcSet.mem_NP : FeedbackArcSet ∈ NP encFeedbackArcSet

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

Reduction from feedback vertex sets

def Cslib.Complexity.FeedbackVertexSet.splitVertices (G : Graph) : Graph

Vertex splitting: every vertex v becomes the arc 2v → 2v + 1, and every arc u → v becomes the arc 2u + 1 → 2v.

theorem Cslib.Complexity.FeedbackVertexSet.dirAdj_splitVertices {G : Graph} {a b : ℕ} : (splitVertices G).DirAdj a b ↔ (∃ v ∈ G.vertices, a = 2 * v ∧ b = 2 * v + 1) ∨ ∃ (u : ℕ) (v : ℕ), G.DirAdj u v ∧ a = 2 * u + 1 ∧ b = 2 * v

The arcs of the split graph: the arc 2v → 2v + 1 of a declared vertex v, and the arc 2u + 1 → 2v of an arc u → v between declared vertices.

def Cslib.Complexity.FeedbackVertexSet.toFeedbackArcSet (x : FeedbackVertexSetInstance) : FeedbackArcSetInstance

The vertex-splitting reduction: the split graph with the same k.

theorem Cslib.Complexity.FeedbackVertexSet.toFeedbackArcSet_mem_iff (x : FeedbackVertexSetInstance) : toFeedbackArcSet x ∈ FeedbackArcSet ↔ x ∈ FeedbackVertexSet

Feedback vertex sets are feedback arc sets of the split graph.

theorem Cslib.Complexity.FeedbackVertexSet.computableInPolyTime_toFeedbackArcSet : Turing.MultiTapeTM.ComputableInPolyTime toFeedbackArcSet encFeedbackVertexSet encFeedbackArcSet

The vertex-splitting reduction is polynomial-time.

theorem Cslib.Complexity.polyTimeReducible_FeedbackVertexSet_FeedbackArcSet : PolyTimeReducible encFeedbackVertexSet encFeedbackArcSet FeedbackVertexSet FeedbackArcSet

FeedbackVertexSet reduces to FeedbackArcSet in polynomial time, by vertex splitting. Karp [Kar72] instead reduces NODE COVER to FEEDBACK ARC SET by splitting the vertices of the node-cover instance. This reduction generalizes his splitting to arbitrary directed graphs, and composing it with polyTimeReducible_VertexCover_FeedbackVertexSet recovers his graph.

theorem Cslib.Complexity.FeedbackArcSet_npHard : NPHard encFeedbackArcSet FeedbackArcSet

FeedbackArcSet is NP-hard.

theorem Cslib.Complexity.FeedbackArcSet_npComplete : NPComplete encFeedbackArcSet FeedbackArcSet

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