Feedback Vertex Set and Feedback Arc Set
Lax799700.Feedback · concepts/Lax799700/Feedback.lean · lax-799700
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The two feedback problems of Karp on directed graphs, the adjacency relation of a structure being an arbitrary binary relation. FeedbackVertexSet asks for at most vertices whose removal leaves an acyclic digraph, the cardinality of the marked set of a marked graph. FeedbackArcSet asks for at most arcs; a set of arcs can have quadratically many elements, so its threshold moves one arity up, to the vocabulary of graphs with a marked binary relation, the number being the cardinality of the marked set of pairs. Self-loops are cycles, as they should be. Acyclicity (AcyclicRel) is a transitive-closure condition, not first-order, but it is equivalent to the existence of a strict partial order containing every surviving arc; guessing that order is what puts both problems in NP, and what makes the reductions provable without manipulating cycles. Hardness is by first-order reductions, of Feedback Vertex Set from Vertex Cover and of Feedback Arc Set from Feedback Vertex Set.
Concept map
Evidence
This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.
1 feedbackArcSet_iff proven
2 feedbackArcSet_NP_complete proven
3 feedbackVertexSet_iff proven
4 feedbackVertexSet_NP_complete proven
5 hasSmallFeedbackArcSet_iso proven
6 hasSmallFeedbackSet_iso proven
Lean source view on GitHub
| 1 | import Mathlib.Data.Fintype.EquivFin |
| 2 | import Mathlib.Data.Set.Card |
| 3 | import Mathlib.SetTheory.Cardinal.Finite |
| 4 | import Mathlib.Logic.Equiv.Prod |
| 5 | import Mathlib.ModelTheory.Semantics |
| 6 | import Mathlib.ModelTheory.Complexity |
| 7 | import Mathlib.Tactic.FinCases |
| 8 | import Mathlib.ModelTheory.Syntax |
| 9 | import Lax799700.CliqueFamily |
| 10 | import Lax904597.Classes |
| 11 | import Lax799700.Problems |
| 12 | |
| 13 | /-! |
| 14 | --- |
| 15 | title: Feedback Vertex Set and Feedback Arc Set |
| 16 | type: theorem |
| 17 | --- |
| 18 | The two feedback problems of Karp on directed graphs, the adjacency |
| 19 | relation of a structure being an arbitrary binary relation. |
| 20 | FeedbackVertexSet asks for at most vertices whose removal leaves an |
| 21 | acyclic digraph, the cardinality of the marked set of a marked graph. |
| 22 | FeedbackArcSet asks for at most arcs; a set of arcs can have |
| 23 | quadratically many elements, so its threshold moves one arity up, to the |
| 24 | vocabulary of graphs with a marked binary relation, the number being the |
| 25 | cardinality of the marked set of pairs. Self-loops are cycles, as they |
| 26 | should be. Acyclicity (AcyclicRel) is a transitive-closure condition, |
| 27 | not first-order, but it is equivalent to the existence of a strict |
| 28 | partial order containing every surviving arc; guessing that order is |
| 29 | what puts both problems in NP, and what makes the reductions provable |
| 30 | without manipulating cycles. Hardness is by first-order reductions, of |
| 31 | Feedback Vertex Set from Vertex Cover and of Feedback Arc Set from |
| 32 | Feedback Vertex Set. |
| 33 | |
| 34 | -/ |
| 35 | |
| 36 | namespace Lax799700.Feedback |
| 37 | |
| 38 | open Lax799700.CliqueFamily |
| 39 | |
| 40 | open FirstOrder |
| 41 | |
| 42 | open FirstOrder.Language |
| 43 | |
| 44 | /-- The relation symbols of the language. -/ |
| 45 | inductive markedArcGraphRel : ℕ → Type where |
| 46 | /-- `adj a b`: there is an arc from `a` to `b`. -/ |
| 47 | | adj : markedArcGraphRel 2 |
| 48 | /-- `marked a b`: the pair `(a, b)` belongs to the marked relation. -/ |
| 49 | | marked : markedArcGraphRel 2 |
| 50 | deriving DecidableEq |
| 51 | |
| 52 | /-- The relational language of arc-marked digraphs: a digraph together with a |
| 53 | marked binary relation, whose cardinality (as a set of pairs) serves as |
| 54 | threshold. -/ |
| 55 | def markedArcGraph : FirstOrder.Language := |
| 56 | ⟨fun _ => Empty, markedArcGraphRel⟩ |
| 57 | |
| 58 | instance instIsRelationalMarkedArcGraph : FirstOrder.Language.IsRelational markedArcGraph := fun _ => |
| 59 | (inferInstance : IsEmpty Empty) |
| 60 | |
| 61 | /-- `adj a b`: there is an arc from `a` to `b`. -/ |
| 62 | abbrev magAdj : markedArcGraph.Relations 2 := |
| 63 | .adj |
| 64 | |
| 65 | /-- `marked a b`: the pair `(a, b)` belongs to the marked relation. -/ |
| 66 | abbrev magMarked : markedArcGraph.Relations 2 := |
| 67 | .marked |
| 68 | |
| 69 | open FirstOrder |
| 70 | |
| 71 | open Language Structure |
| 72 | |
| 73 | section Acyclicity |
| 74 | |
| 75 | variable {A : Type} |
| 76 | |
| 77 | /-- A relation is acyclic if no element is reachable from itself along a |
| 78 | nonempty path. -/ |
| 79 | def AcyclicRel (R : A → A → Prop) : Prop := |
| 80 | ∀ x, ¬Relation.TransGen R x x |
| 81 | |
| 82 | end Acyclicity |
| 83 | |
| 84 | section Generic |
| 85 | |
| 86 | variable {A : Type} |
| 87 | |
| 88 | /-- An arc surviving the removal of the `Cp`-vertices: both endpoints are |
| 89 | outside `Cp` and the arc is present. -/ |
| 90 | def SurvivingArc (Adjp : A → A → Prop) (Cp : A → Prop) (a b : A) : Prop := |
| 91 | ¬Cp a ∧ ¬Cp b ∧ Adjp a b |
| 92 | |
| 93 | /-- An arc surviving the removal of the `Fp`-arcs: the arc is present and not |
| 94 | removed. -/ |
| 95 | def UncutArc (Adjp : A → A → Prop) (Fp : A → A → Prop) (a b : A) : Prop := |
| 96 | Adjp a b ∧ ¬Fp a b |
| 97 | |
| 98 | /-- Some set of vertices whose removal makes the digraph acyclic is at most as |
| 99 | large as the number encoded by the `Kp`-marked elements: “some feedback vertex |
| 100 | set is at most as large as the marked set”. -/ |
| 101 | def FeedbackOn (Adjp : A → A → Prop) (Kp : A → Prop) : Prop := |
| 102 | ∃ C : A → Prop, AcyclicRel (SurvivingArc Adjp C) ∧ {x | C x}.ncard ≤ {x | Kp x}.ncard |
| 103 | |
| 104 | /-- Some set of arcs whose removal makes the digraph acyclic is at most as |
| 105 | large as the number encoded by the `Kp`-marked pairs: “some feedback arc set |
| 106 | is at most as large as the marked relation”. -/ |
| 107 | def FeedbackArcOn (Adjp : A → A → Prop) (Kp : A → A → Prop) : Prop := |
| 108 | ∃ F : A → A → Prop, AcyclicRel (UncutArc Adjp F) ∧ |
| 109 | {p : A × A | F p.1 p.2}.ncard ≤ {p : A × A | Kp p.1 p.2}.ncard |
| 110 | |
| 111 | end Generic |
| 112 | |
| 113 | section Problems |
| 114 | |
| 115 | section Shorthands |
| 116 | |
| 117 | variable {A : Type} [markedArcGraph.Structure A] |
| 118 | |
| 119 | /-- `adj a b`: there is an arc from `a` to `b`. -/ |
| 120 | def MAGAdj {A : Type} [markedArcGraph.Structure A] (a0 : A) (a1 : A) : Prop := |
| 121 | FirstOrder.Language.Structure.RelMap magAdj ![a0, a1] |
| 122 | |
| 123 | /-- `marked a b`: the pair `(a, b)` belongs to the marked relation. -/ |
| 124 | def MAGMarked {A : Type} [markedArcGraph.Structure A] (a0 : A) (a1 : A) : Prop := |
| 125 | FirstOrder.Language.Structure.RelMap magMarked ![a0, a1] |
| 126 | |
| 127 | end Shorthands |
| 128 | |
| 129 | /-- A marked graph has a feedback vertex set at most as large as its marked |
| 130 | set. (Finiteness of the universe is part of the property: cardinality |
| 131 | thresholds are only meaningful on finite structures.) -/ |
| 132 | def HasSmallFeedbackSet (A : Type) [markedGraph.Structure A] : Prop := |
| 133 | Finite A ∧ FeedbackOn (MGAdj (A := A)) (MGMarked (A := A)) |
| 134 | |
| 135 | /-- An arc-marked digraph has a feedback arc set at most as large as its |
| 136 | marked relation. -/ |
| 137 | def HasSmallFeedbackArcSet (A : Type) [markedArcGraph.Structure A] : Prop := |
| 138 | Finite A ∧ FeedbackArcOn (MAGAdj (A := A)) (MAGMarked (A := A)) |
| 139 | |
| 140 | end Problems |
| 141 | |
| 142 | open Lax904597.Problems Lax904597.Classes Lax799700.Problems |
| 143 | |
| 144 | /-- The property `HasSmallFeedbackSet` is isomorphism-invariant. -/ |
| 145 | axiom hasSmallFeedbackSet_iso : ∀ {A B : Type} [Lax799700.CliqueFamily.markedGraph.Structure A] [Lax799700.CliqueFamily.markedGraph.Structure B], |
| 146 | (A ≃[Lax799700.CliqueFamily.markedGraph] B) → (HasSmallFeedbackSet A ↔ HasSmallFeedbackSet B) |
| 147 | |
| 148 | /-- The problem FeedbackVertexSet: does the structure satisfy `HasSmallFeedbackSet`? -/ |
| 149 | def FeedbackVertexSet : DecisionProblem Lax799700.CliqueFamily.markedGraph := |
| 150 | DecisionProblem.ofPred HasSmallFeedbackSet |
| 151 | |
| 152 | /-- The yes-instances of FeedbackVertexSet are exactly the structures |
| 153 | satisfying `HasSmallFeedbackSet`. -/ |
| 154 | axiom feedbackVertexSet_iff : ∀ (A : Type) [Lax799700.CliqueFamily.markedGraph.Structure A], FeedbackVertexSet A ↔ HasSmallFeedbackSet A |
| 155 | |
| 156 | /-- FeedbackVertexSet is NP-complete. -/ |
| 157 | axiom feedbackVertexSet_NP_complete : NP.Complete FeedbackVertexSet |
| 158 | |
| 159 | /-- The property `HasSmallFeedbackArcSet` is isomorphism-invariant. -/ |
| 160 | axiom hasSmallFeedbackArcSet_iso : ∀ {A B : Type} [Lax799700.Feedback.markedArcGraph.Structure A] [Lax799700.Feedback.markedArcGraph.Structure B], |
| 161 | (A ≃[Lax799700.Feedback.markedArcGraph] B) → (HasSmallFeedbackArcSet A ↔ HasSmallFeedbackArcSet B) |
| 162 | |
| 163 | /-- The problem FeedbackArcSet: does the structure satisfy `HasSmallFeedbackArcSet`? -/ |
| 164 | def FeedbackArcSet : DecisionProblem Lax799700.Feedback.markedArcGraph := |
| 165 | DecisionProblem.ofPred HasSmallFeedbackArcSet |
| 166 | |
| 167 | /-- The yes-instances of FeedbackArcSet are exactly the structures satisfying |
| 168 | `HasSmallFeedbackArcSet`. -/ |
| 169 | axiom feedbackArcSet_iff : ∀ (A : Type) [Lax799700.Feedback.markedArcGraph.Structure A], FeedbackArcSet A ↔ HasSmallFeedbackArcSet A |
| 170 | |
| 171 | /-- FeedbackArcSet is NP-complete. -/ |
| 172 | axiom feedbackArcSet_NP_complete : NP.Complete FeedbackArcSet |
| 173 | |
| 174 | end Lax799700.Feedback |
| 175 |
Used by
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments