Vertex covers

VertexCover is the set of graphs, given by a list of vertices and a list of edges, together with a number k, such that k of the declared vertices meet every edge between declared vertices [Kar72]. Graphs are read on their declared vertices through Cslib.Complexity.Graph.induced, and covers through SimpleGraph.IsVertexCover. Edges with an undeclared endpoint and self-loops are therefore ignored, and repeated vertex entries count once.

The cover has exactly k distinct vertices, matching IndependentSet. Since a set of declared vertices containing a cover is a cover, this agrees with the textbook formulation "a cover of at most k vertices" for every k up to the number n of distinct declared vertices, and VertexCover rejects every k > n (mem_VertexCover_iff_exists_card_le). In particular a graph without declared vertices belongs to VertexCover only with k = 0.

A set of declared vertices is a vertex cover exactly when the remaining declared vertices form an independent set (SimpleGraph.isIndepSet_compl_iff_isVertexCover), so IndependentSet.toVertexCover maps (G, m) to (G, n - m), where n is the number of distinct declared vertices; a target m > n is mapped to the unsatisfiable target n + 1 [Kar72].

The same problem as a class of finite structures, closed under isomorphism and without an encoding, with the target size given by a unary relation, is Cslib.Logic.FO.sizedGraph.VertexCover. There loops are ignored, edges need not be symmetric, and the reductions between independent set, clique and vertex cover are quantifier-free first-order interpretations.

Main definitions

• Cslib.Complexity.VertexCoverInstance, Cslib.Complexity.VertexCover.
• Cslib.Complexity.VertexCover.declaredEdges: the listed edges between declared vertices.
• Cslib.Complexity.VertexCover.isUncoveredEdge, Cslib.Complexity.VertexCover.uncoveredEdges, Cslib.Complexity.VertexCover.isCover, Cslib.Complexity.VertexCover.verifier.
• Cslib.Complexity.IndependentSet.toVertexCover.
• Cslib.Complexity.Graph.vertexCoverNum: the vertex cover number.

Main results

• Cslib.Complexity.mem_VertexCover_iff_exists_card_le: covers of exactly k vertices versus covers of at most k vertices.
• Cslib.Complexity.IndependentSet.toVertexCover_mem_iff: toVertexCover x ∈ VertexCover ↔ x ∈ IndependentSet.
• Cslib.Complexity.Graph.vertexCoverNum_eq_card_sub_indepNum: the vertex cover number is the number of distinct declared vertices minus the independence number.
• Cslib.Complexity.IndependentSet.computableInPolyTime_toVertexCover: the reduction is polynomial-time, with targets in binary.
• Cslib.Complexity.VertexCover.isCover_eq_true_iff, Cslib.Complexity.VertexCover.isVerifier, Cslib.Complexity.VertexCover.mem_NP: VertexCover ∈ NP encVertexCoverInstance.
• Cslib.Complexity.polyTimeReducible_IndependentSet_VertexCover, Cslib.Complexity.VertexCover_npHard, Cslib.Complexity.VertexCover_npComplete: VertexCover is NP-complete.

References

• M. R. Garey and D. S. Johnson, Computers and Intractability
• R. M. Karp, Reducibility among combinatorial problems
• M. Sipser, Introduction to the Theory of Computation

structure Cslib.Complexity.VertexCoverInstance : Type

An instance (graph, k) of Vertex Cover.

• graph : Graph

  The graph in which to find a vertex cover.

• k : ℕ

  The target number of declared vertices.

theorem Cslib.Complexity.VertexCoverInstance.ext {x y : VertexCoverInstance} (graph : x.graph = y.graph) (k : x.k = y.k) : x = y

theorem Cslib.Complexity.VertexCoverInstance.ext_iff {x y : VertexCoverInstance} : x = y ↔ x.graph = y.graph ∧ x.k = y.k

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqVertexCoverInstance : DecidableEq VertexCoverInstance

def Cslib.Complexity.instDecidableEqVertexCoverInstance.decEq (x✝ x✝¹ : VertexCoverInstance) : Decidable (x✝ = x✝¹)

def Cslib.Complexity.instReprVertexCoverInstance.repr : VertexCoverInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instReprVertexCoverInstance : Repr VertexCoverInstance

@[instance_reducible]

instance Cslib.Complexity.instInhabitedVertexCoverInstance : Inhabited VertexCoverInstance

def Cslib.Complexity.encVertexCoverInstance : VertexCoverInstance ↪ List Bool

Framed encGraph followed by binary target encNat, encoding VertexCoverInstance.

@[reducible, inline]

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

The tuple of the fields of encVertexCoverInstance.

theorem Cslib.Complexity.encVertexCoverInstance_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Graph × ℕ) => { graph := p.1, k := p.2 }) encVertexCoverInstanceFields encVertexCoverInstance 1 1

theorem Cslib.Complexity.encVertexCoverInstance_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : VertexCoverInstance) => (a.graph, a.k)) encVertexCoverInstance encVertexCoverInstanceFields 1 1

theorem Cslib.Complexity.encVertexCoverInstance_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, k := x1 x }) encIn encVertexCoverInstance (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encVertexCoverInstance_k_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → VertexCoverInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encVertexCoverInstance → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).k) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encVertexCoverInstance_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, k := x1 x }) encIn encVertexCoverInstance budget

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

theorem Cslib.Complexity.encVertexCoverInstance_k_inO : Turing.MultiTapeTM.ComputableInO VertexCoverInstance.k encVertexCoverInstance Turing.MultiTapeTM.encNat (fun (a : VertexCoverInstance) => (encVertexCoverInstance a).length) fun (a : VertexCoverInstance) => (encVertexCoverInstance a).length

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

theorem Cslib.Complexity.encVertexCoverInstance_graph_deg : Turing.MultiTapeTM.ComputableInDegree VertexCoverInstance.graph encVertexCoverInstance encGraph 1 1

theorem Cslib.Complexity.encVertexCoverInstance_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, k := x1 x }) encIn encVertexCoverInstance

theorem Cslib.Complexity.encVertexCoverInstance_k_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → VertexCoverInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encVertexCoverInstance S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).k) encIn✝ Turing.MultiTapeTM.encNat S✝

@[simp]

theorem Cslib.Complexity.encVertexCoverInstance_apply (a : VertexCoverInstance) : encVertexCoverInstance a = encVertexCoverInstanceFields (a.graph, a.k)

theorem Cslib.Complexity.encVertexCoverInstance_k_deg : Turing.MultiTapeTM.ComputableInDegree VertexCoverInstance.k encVertexCoverInstance Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encVertexCoverInstance_graph_inO : Turing.MultiTapeTM.ComputableInO VertexCoverInstance.graph encVertexCoverInstance encGraph (fun (a : VertexCoverInstance) => (encVertexCoverInstance a).length) fun (a : VertexCoverInstance) => (encVertexCoverInstance a).length

def Cslib.Complexity.VertexCover : Set VertexCoverInstance

The graphs with a vertex cover of k of their vertices: k declared vertices meeting every edge between two declared vertices [Kar72].

theorem Cslib.Complexity.mem_VertexCover_iff {x : VertexCoverInstance} : x ∈ VertexCover ↔ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ x.graph.vertices) ∧ (∀ u ∈ x.graph.vertices, ∀ v ∈ x.graph.vertices, x.graph.toSimpleGraph.Adj u v → u ∈ S ∨ v ∈ S) ∧ S.card = x.k

Membership in VertexCover as a finite set of k declared vertices meeting every edge between declared vertices.

@[simp]

theorem Cslib.Complexity.mem_VertexCover_iff_mk {G : Graph} {k : ℕ} : { graph := G, k := k } ∈ VertexCover ↔ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ G.vertices) ∧ (∀ u ∈ G.vertices, ∀ v ∈ G.vertices, G.toSimpleGraph.Adj u v → u ∈ S ∨ v ∈ S) ∧ S.card = k

theorem Cslib.Complexity.mem_VertexCover_iff_exists_card_le {x : VertexCoverInstance} : x ∈ VertexCover ↔ x.k ≤ x.graph.vertices.toFinset.card ∧ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ x.graph.vertices) ∧ (∀ u ∈ x.graph.vertices, ∀ v ∈ x.graph.vertices, x.graph.toSimpleGraph.Adj u v → u ∈ S ∨ v ∈ S) ∧ S.card ≤ x.k

VertexCover through covers of at most k vertices: x ∈ VertexCover exactly when x.k is at most the number of distinct declared vertices and some cover has at most x.k vertices.

theorem Cslib.Complexity.mem_VertexCover_iff_exists_card_le_mk {G : Graph} {k : ℕ} : { graph := G, k := k } ∈ VertexCover ↔ k ≤ G.vertices.toFinset.card ∧ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ G.vertices) ∧ (∀ u ∈ G.vertices, ∀ v ∈ G.vertices, G.toSimpleGraph.Adj u v → u ∈ S ∨ v ∈ S) ∧ S.card ≤ k

Reduction from independent sets

def Cslib.Complexity.IndependentSet.toVertexCover (x : IndependentSetInstance) : VertexCoverInstance

The reduction from IndependentSet to VertexCover: keep the graph and replace the target m by n - m, where n is the number of distinct declared vertices, or by n + 1 when m > n.

theorem Cslib.Complexity.IndependentSet.toVertexCover_mem_iff (x : IndependentSetInstance) : toVertexCover x ∈ VertexCover ↔ x ∈ IndependentSet

Independent sets are complements of vertex covers.

theorem Cslib.Complexity.IndependentSet.computableInPolyTime_toVertexCover : Turing.MultiTapeTM.ComputableInPolyTime toVertexCover encIndependentSetInstance encVertexCoverInstance

The reduction toVertexCover is polynomial-time: the vertex count is computed in unary, and the binary target is compared with it by saturating decoding.

def Cslib.Complexity.VertexCover.isDeclaredEdge (G : Graph) (e : ℕ × ℕ) : Bool

Whether both endpoints of e are declared vertices of G.

def Cslib.Complexity.VertexCover.declaredEdges (G : Graph) : List (ℕ × ℕ)

The listed edges of G between declared vertices.

theorem Cslib.Complexity.VertexCover.mem_declaredEdges {G : Graph} {e : ℕ × ℕ} : e ∈ declaredEdges G ↔ e ∈ G.edges ∧ e.1 ∈ G.vertices ∧ e.2 ∈ G.vertices

An edge is declared when it is listed and both endpoints are declared vertices.

theorem Cslib.Complexity.VertexCover.computableInPolyTime_declaredEdges : Turing.MultiTapeTM.ComputableInPolyTime declaredEdges encGraph (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))

Listing the edges between declared vertices is polynomial-time.

def Cslib.Complexity.VertexCover.isUncoveredEdge (G : Graph) (C : List ℕ) (e : ℕ × ℕ) : Bool

Whether the edge e joins two distinct declared vertices of G and neither endpoint is in C.

def Cslib.Complexity.VertexCover.uncoveredEdges (G : Graph) (C : List ℕ) : List (ℕ × ℕ)

The edges of G between distinct declared vertices with neither endpoint in C.

def Cslib.Complexity.VertexCover.isCover (G : Graph) (C : List ℕ) : Bool

Whether C covers every edge of G between declared vertices.

theorem Cslib.Complexity.VertexCover.isUncoveredEdge_eq_true_iff {G : Graph} {C : List ℕ} {e : ℕ × ℕ} : isUncoveredEdge G C e = true ↔ e.1 ∈ G.vertices ∧ e.2 ∈ G.vertices ∧ e.1 ≠ e.2 ∧ e.1 ∉ C ∧ e.2 ∉ C

theorem Cslib.Complexity.VertexCover.mem_uncoveredEdges_iff {G : Graph} {C : List ℕ} {e : ℕ × ℕ} : e ∈ uncoveredEdges G C ↔ e ∈ G.edges ∧ e.1 ∈ G.vertices ∧ e.2 ∈ G.vertices ∧ e.1 ≠ e.2 ∧ e.1 ∉ C ∧ e.2 ∉ C

theorem Cslib.Complexity.VertexCover.isCover_eq_true_iff {G : Graph} {C : List ℕ} : isCover G C = true ↔ ∀ u ∈ G.vertices, ∀ v ∈ G.vertices, G.toSimpleGraph.Adj u v → u ∈ C ∨ v ∈ C

isCover G C holds exactly when every edge between declared vertices of G has an endpoint in C.

theorem Cslib.Complexity.VertexCover.computableInPolyTime_uncoveredEdges : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × List ℕ) => uncoveredEdges p.1 p.2) (Turing.MultiTapeTM.encPair encGraph (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))

Listing the uncovered edges is polynomial-time.

theorem Cslib.Complexity.VertexCover.computableInPolyTime_isCover : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Graph × List ℕ) => isCover p.1 p.2) (Turing.MultiTapeTM.encPair encGraph (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encBool

Testing whether C is a cover of G is polynomial-time.

def Cslib.Complexity.VertexCover.verifier : VertexCoverInstance × List Bool → Bool

The verifier for VertexCover, a subset verifier (Cslib.Complexity.subsetVerifier): select distinct declared vertices by the certificate mask, check that their count equals k, and check that every edge between declared vertices has a selected endpoint (isCover).

theorem Cslib.Complexity.VertexCover.isVerifier : IsVerifier encVertexCoverInstance Polynomial.X verifier VertexCover

VertexCover.verifier verifies VertexCover with certificates as long as the encoded instance.

theorem Cslib.Complexity.VertexCover.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encVertexCoverInstance Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The VertexCover verifier is polynomial-time.

theorem Cslib.Complexity.VertexCover.mem_NP : VertexCover ∈ NP encVertexCoverInstance

VertexCover belongs to NP.

theorem Cslib.Complexity.polyTimeReducible_IndependentSet_VertexCover : PolyTimeReducible encIndependentSetInstance encVertexCoverInstance IndependentSet VertexCover

IndependentSet reduces to VertexCover in polynomial time via IndependentSet.toVertexCover.

theorem Cslib.Complexity.VertexCover_npHard : NPHard encVertexCoverInstance VertexCover

VertexCover is NP-hard.

theorem Cslib.Complexity.VertexCover_npComplete : NPComplete encVertexCoverInstance VertexCover

VertexCover is NP-complete [Kar72].

The vertex cover number

noncomputable def Cslib.Complexity.Graph.vertexCoverNum (G : Graph) : ℕ

The vertex cover number of a graph: the least number of declared vertices meeting every edge between declared vertices.

theorem Cslib.Complexity.Graph.vertexCoverNum_mem_VertexCover (G : Graph) : { graph := G, k := G.vertexCoverNum } ∈ VertexCover

The vertex cover number is the size of a vertex cover.

theorem Cslib.Complexity.Graph.vertexCoverNum_le_of_mem_VertexCover {G : Graph} {k : ℕ} (h : { graph := G, k := k } ∈ VertexCover) : G.vertexCoverNum ≤ k

Every vertex cover has at least G.vertexCoverNum vertices.

theorem Cslib.Complexity.Graph.vertexCoverNum_eq_card_sub_indepNum (G : Graph) : G.vertexCoverNum = G.vertices.toFinset.card - G.indepNum

A vertex cover is the complement of an independent set: the vertex cover number is the number of distinct declared vertices minus the independence number.