Clique, Independent Set and Vertex Cover
Lax799700.CliqueFamily · concepts/Lax799700/CliqueFamily.lean · lax-799700
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The three classical threshold problems on graphs, as decision problems on marked graphs: a binary adjacency relation and a unary mark whose cardinality is the threshold of the textbook problems, in unary representation, order-free and isomorphism-invariant. Clique asks for a clique at least as large as the marked set, IndependentSet for an independent set at least as large, VertexCover for a vertex cover at most as large. Self-loops are ignored and adjacency is required in both directions, so the problems agree with their standard versions on simple graphs. Finiteness of the universe is part of the yes-instances, since cardinality thresholds only mean something on finite structures.
Clique is in NP by an existential second-order definition that guesses an injection of the marked set into a clique, and NP-hard by an ordered first-order reduction from SAT. Independent Set reduces to and from Clique by complementing the edges, and Vertex Cover to and from Independent Set by complementing the chosen set; these two first-order reductions give both their membership and their hardness.
Concept map
Evidence
This concept declares 9 statements. Each proof establishes one of them relative to its assumptions.
1 clique_iff proven
2 clique_NP_complete proven
3 hasLargeClique_iso proven
4 hasLargeIndependentSet_iso proven
5 hasSmallVertexCover_iso proven
6 indSet_iff proven
7 indSet_NP_complete proven
8 vertexCover_iff proven
9 vertexCover_NP_complete 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 Lax904597.Classes |
| 10 | import Lax799700.Problems |
| 11 | |
| 12 | /-! |
| 13 | --- |
| 14 | title: Clique, Independent Set and Vertex Cover |
| 15 | type: theorem |
| 16 | --- |
| 17 | The three classical threshold problems on graphs, as decision problems on |
| 18 | marked graphs: a binary adjacency relation and a unary mark whose |
| 19 | cardinality is the threshold of the textbook problems, in unary |
| 20 | representation, order-free and isomorphism-invariant. Clique asks for a |
| 21 | clique at least as large as the marked set, IndependentSet for an |
| 22 | independent set at least as large, VertexCover for a vertex cover at most |
| 23 | as large. Self-loops are ignored and adjacency is required in both |
| 24 | directions, so the problems agree with their standard versions on simple |
| 25 | graphs. Finiteness of the universe is part of the yes-instances, since |
| 26 | cardinality thresholds only mean something on finite structures. |
| 27 | |
| 28 | Clique is in NP by an existential second-order definition that guesses |
| 29 | an injection of the marked set into a clique, and NP-hard by an ordered |
| 30 | first-order reduction from SAT. Independent Set reduces to and from |
| 31 | Clique by complementing the edges, and Vertex Cover to and from |
| 32 | Independent Set by complementing the chosen set; these two first-order |
| 33 | reductions give both their membership and their hardness. |
| 34 | |
| 35 | -/ |
| 36 | |
| 37 | namespace Lax799700.CliqueFamily |
| 38 | |
| 39 | open FirstOrder |
| 40 | |
| 41 | open FirstOrder.Language |
| 42 | |
| 43 | /-- The relation symbols of the language. -/ |
| 44 | inductive markedGraphRel : ℕ → Type where |
| 45 | /-- `adj a b`: there is an edge from `a` to `b`. -/ |
| 46 | | adj : markedGraphRel 2 |
| 47 | /-- `marked a`: the element `a` belongs to the marked set. -/ |
| 48 | | marked : markedGraphRel 1 |
| 49 | deriving DecidableEq |
| 50 | |
| 51 | /-- The relational language of marked graphs: a graph together with a marked |
| 52 | subset of its vertices, whose cardinality serves as threshold. -/ |
| 53 | def markedGraph : FirstOrder.Language := |
| 54 | ⟨fun _ => Empty, markedGraphRel⟩ |
| 55 | |
| 56 | instance instIsRelationalMarkedGraph : FirstOrder.Language.IsRelational markedGraph := fun _ => |
| 57 | (inferInstance : IsEmpty Empty) |
| 58 | |
| 59 | /-- `adj a b`: there is an edge from `a` to `b`. -/ |
| 60 | abbrev mgAdj : markedGraph.Relations 2 := |
| 61 | .adj |
| 62 | |
| 63 | /-- `marked a`: the element `a` belongs to the marked set. -/ |
| 64 | abbrev mgMarked : markedGraph.Relations 1 := |
| 65 | .marked |
| 66 | |
| 67 | open FirstOrder |
| 68 | |
| 69 | open Language Structure |
| 70 | |
| 71 | section Generic |
| 72 | |
| 73 | variable {A : Type} |
| 74 | |
| 75 | /-- Some set that is pairwise `Adjp`-related (off the diagonal) is at least as |
| 76 | large as the number encoded by the `Kp`-marked elements: “some clique is at |
| 77 | least as large as the marked set”. -/ |
| 78 | def CliqueOn (Adjp : A → A → Prop) (Kp : A → Prop) : Prop := |
| 79 | ∃ S : A → Prop, (∀ x y, S x → S y → x ≠ y → Adjp x y) ∧ |
| 80 | {x | Kp x}.ncard ≤ {x | S x}.ncard |
| 81 | |
| 82 | /-- Some set that is pairwise non-`Adjp`-related (off the diagonal) is at least |
| 83 | as large as the number encoded by the `Kp`-marked elements: “some independent |
| 84 | set is at least as large as the marked set”. -/ |
| 85 | def IndepOn (Adjp : A → A → Prop) (Kp : A → Prop) : Prop := |
| 86 | CliqueOn (fun x y => ¬Adjp x y) Kp |
| 87 | |
| 88 | /-- Some set meeting every (off-diagonal) `Adjp`-edge is at most as large as |
| 89 | the number encoded by the `Kp`-marked elements: “some vertex cover is at most |
| 90 | as large as the marked set”. -/ |
| 91 | def CoverOn (Adjp : A → A → Prop) (Kp : A → Prop) : Prop := |
| 92 | ∃ C : A → Prop, (∀ x y, x ≠ y → Adjp x y → C x ∨ C y) ∧ |
| 93 | {x | C x}.ncard ≤ {x | Kp x}.ncard |
| 94 | |
| 95 | end Generic |
| 96 | |
| 97 | section Problems |
| 98 | |
| 99 | section Shorthands |
| 100 | |
| 101 | variable {A : Type} [markedGraph.Structure A] |
| 102 | |
| 103 | /-- `adj a b`: there is an edge from `a` to `b`. -/ |
| 104 | def MGAdj {A : Type} [markedGraph.Structure A] (a0 : A) (a1 : A) : Prop := |
| 105 | FirstOrder.Language.Structure.RelMap mgAdj ![a0, a1] |
| 106 | |
| 107 | /-- `marked a`: the element `a` belongs to the marked set. -/ |
| 108 | def MGMarked {A : Type} [markedGraph.Structure A] (a0 : A) : Prop := |
| 109 | FirstOrder.Language.Structure.RelMap mgMarked ![a0] |
| 110 | |
| 111 | end Shorthands |
| 112 | |
| 113 | variable (A : Type) [markedGraph.Structure A] |
| 114 | |
| 115 | /-- A marked graph contains a clique at least as large as its marked set. |
| 116 | (Finiteness of the universe is part of the property: cardinality thresholds |
| 117 | are only meaningful on finite structures.) -/ |
| 118 | def HasLargeClique : Prop := |
| 119 | Finite A ∧ CliqueOn (MGAdj (A := A)) (MGMarked (A := A)) |
| 120 | |
| 121 | /-- A marked graph contains an independent set at least as large as its |
| 122 | marked set. -/ |
| 123 | def HasLargeIndependentSet : Prop := |
| 124 | Finite A ∧ IndepOn (MGAdj (A := A)) (MGMarked (A := A)) |
| 125 | |
| 126 | /-- A marked graph contains a vertex cover at most as large as its marked |
| 127 | set. -/ |
| 128 | def HasSmallVertexCover : Prop := |
| 129 | Finite A ∧ CoverOn (MGAdj (A := A)) (MGMarked (A := A)) |
| 130 | |
| 131 | end Problems |
| 132 | |
| 133 | open Lax904597.Problems Lax904597.Classes Lax799700.Problems |
| 134 | |
| 135 | /-- The property `HasLargeClique` is isomorphism-invariant. -/ |
| 136 | axiom hasLargeClique_iso : ∀ {A B : Type} [Lax799700.CliqueFamily.markedGraph.Structure A] [Lax799700.CliqueFamily.markedGraph.Structure B], |
| 137 | (A ≃[Lax799700.CliqueFamily.markedGraph] B) → (HasLargeClique A ↔ HasLargeClique B) |
| 138 | |
| 139 | /-- The problem Clique: does the structure satisfy `HasLargeClique`? -/ |
| 140 | def Clique : DecisionProblem Lax799700.CliqueFamily.markedGraph := |
| 141 | DecisionProblem.ofPred HasLargeClique |
| 142 | |
| 143 | /-- The yes-instances of Clique are exactly the structures satisfying |
| 144 | `HasLargeClique`. -/ |
| 145 | axiom clique_iff : ∀ (A : Type) [Lax799700.CliqueFamily.markedGraph.Structure A], Clique A ↔ HasLargeClique A |
| 146 | |
| 147 | /-- Clique is NP-complete. -/ |
| 148 | axiom clique_NP_complete : NP.Complete Clique |
| 149 | |
| 150 | /-- The property `HasLargeIndependentSet` is isomorphism-invariant. -/ |
| 151 | axiom hasLargeIndependentSet_iso : ∀ {A B : Type} [Lax799700.CliqueFamily.markedGraph.Structure A] [Lax799700.CliqueFamily.markedGraph.Structure B], |
| 152 | (A ≃[Lax799700.CliqueFamily.markedGraph] B) → (HasLargeIndependentSet A ↔ HasLargeIndependentSet B) |
| 153 | |
| 154 | /-- The problem IndependentSet: does the structure satisfy `HasLargeIndependentSet`? -/ |
| 155 | def IndependentSet : DecisionProblem Lax799700.CliqueFamily.markedGraph := |
| 156 | DecisionProblem.ofPred HasLargeIndependentSet |
| 157 | |
| 158 | /-- The yes-instances of IndependentSet are exactly the structures satisfying |
| 159 | `HasLargeIndependentSet`. -/ |
| 160 | axiom indSet_iff : ∀ (A : Type) [Lax799700.CliqueFamily.markedGraph.Structure A], IndependentSet A ↔ HasLargeIndependentSet A |
| 161 | |
| 162 | /-- IndependentSet is NP-complete. -/ |
| 163 | axiom indSet_NP_complete : NP.Complete IndependentSet |
| 164 | |
| 165 | /-- The property `HasSmallVertexCover` is isomorphism-invariant. -/ |
| 166 | axiom hasSmallVertexCover_iso : ∀ {A B : Type} [Lax799700.CliqueFamily.markedGraph.Structure A] [Lax799700.CliqueFamily.markedGraph.Structure B], |
| 167 | (A ≃[Lax799700.CliqueFamily.markedGraph] B) → (HasSmallVertexCover A ↔ HasSmallVertexCover B) |
| 168 | |
| 169 | /-- The problem VertexCover: does the structure satisfy `HasSmallVertexCover`? -/ |
| 170 | def VertexCover : DecisionProblem Lax799700.CliqueFamily.markedGraph := |
| 171 | DecisionProblem.ofPred HasSmallVertexCover |
| 172 | |
| 173 | /-- The yes-instances of VertexCover are exactly the structures satisfying |
| 174 | `HasSmallVertexCover`. -/ |
| 175 | axiom vertexCover_iff : ∀ (A : Type) [Lax799700.CliqueFamily.markedGraph.Structure A], VertexCover A ↔ HasSmallVertexCover A |
| 176 | |
| 177 | /-- VertexCover is NP-complete. -/ |
| 178 | axiom vertexCover_NP_complete : NP.Complete VertexCover |
| 179 | |
| 180 | end Lax799700.CliqueFamily |
| 181 |
Builds on
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments