Clique cover

CliqueCover is Karp's problem CLIQUE COVER [Kar72]: given a graph G and a number l, the declared vertices of G are the union of at most l cliques of the graph induced on them (Cslib.Complexity.Graph.CoveredByCliques). Instances (Cslib.Complexity.CliqueCoverInstance) are encoded by Cslib.Complexity.encCliqueCover, as for Cslib.Complexity.ChromaticNumber.

The cliques of a cover may be taken to be the color classes of a coloring of the complement (SimpleGraph.exists_cliqueCover_iff_colorable_compl), so complementing the graph on its declared vertices (Cslib.Complexity.Graph.compl) reduces CliqueCover and ChromaticNumber to each other. Karp's reduction from CHROMATIC NUMBER maps ⟨G, k⟩ to the complement of G with k cliques (Cslib.Complexity.Graph.compl_mem_CliqueCover_iff); the converse reduction gives NP membership.

Main definitions

• Cslib.Complexity.CliqueCoverInstance: instance (graph, cliques) of Clique Cover.
• Cslib.Complexity.encCliqueCover: polynomial-time encoding of CliqueCoverInstance.
• Cslib.Complexity.Graph.CoveredByCliques: covers of the declared vertices by cliques.
• Cslib.Complexity.CliqueCover: graphs with a number of cliques that suffices.

Main results

• Cslib.Complexity.Graph.mem_CliqueCover_iff_compl: a cover by l cliques is an l-coloring of the complement.
• Cslib.Complexity.Graph.compl_mem_CliqueCover_iff: correctness of Karp's reduction.
• Cslib.Complexity.polyTimeReducible_ChromaticNumber_CliqueCover, Cslib.Complexity.polyTimeReducible_CliqueCover_ChromaticNumber: the two reductions.
• Cslib.Complexity.CliqueCover.mem_NP, Cslib.Complexity.CliqueCover_npHard, Cslib.Complexity.CliqueCover_npComplete: CliqueCover is NP-complete.

References

• R. M. Karp, Reducibility among combinatorial problems

structure Cslib.Complexity.CliqueCoverInstance : Type

An instance (graph, cliques) of Clique Cover.

• graph : Graph

  The graph whose declared vertices are to be covered.

• cliques : ℕ

  The maximum number of cliques allowed in the cover.

theorem Cslib.Complexity.CliqueCoverInstance.ext {x y : CliqueCoverInstance} (graph : x.graph = y.graph) (cliques : x.cliques = y.cliques) : x = y

theorem Cslib.Complexity.CliqueCoverInstance.ext_iff {x y : CliqueCoverInstance} : x = y ↔ x.graph = y.graph ∧ x.cliques = y.cliques

def Cslib.Complexity.instDecidableEqCliqueCoverInstance.decEq (x✝ x✝¹ : CliqueCoverInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqCliqueCoverInstance : DecidableEq CliqueCoverInstance

@[instance_reducible]

instance Cslib.Complexity.instReprCliqueCoverInstance : Repr CliqueCoverInstance

def Cslib.Complexity.instReprCliqueCoverInstance.repr : CliqueCoverInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instInhabitedCliqueCoverInstance : Inhabited CliqueCoverInstance

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

theorem Cslib.Complexity.encCliqueCover_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, cliques := x1 x }) encIn encCliqueCover

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

theorem Cslib.Complexity.encCliqueCover_cliques_inO : Turing.MultiTapeTM.ComputableInO CliqueCoverInstance.cliques encCliqueCover Turing.MultiTapeTM.encNat (fun (a : CliqueCoverInstance) => (encCliqueCover a).length) fun (a : CliqueCoverInstance) => (encCliqueCover a).length

@[simp]

theorem Cslib.Complexity.encCliqueCover_apply (a : CliqueCoverInstance) : encCliqueCover a = encCliqueCoverFields (a.graph, a.cliques)

theorem Cslib.Complexity.encCliqueCover_graph_deg : Turing.MultiTapeTM.ComputableInDegree CliqueCoverInstance.graph encCliqueCover encGraph 1 1

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

@[reducible, inline]

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

The tuple of the fields of encCliqueCover.

theorem Cslib.Complexity.encCliqueCover_graph_inO : Turing.MultiTapeTM.ComputableInO CliqueCoverInstance.graph encCliqueCover encGraph (fun (a : CliqueCoverInstance) => (encCliqueCover a).length) fun (a : CliqueCoverInstance) => (encCliqueCover a).length

theorem Cslib.Complexity.encCliqueCover_cliques_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → CliqueCoverInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encCliqueCover S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).cliques) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.encCliqueCover_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : CliqueCoverInstance) => (a.graph, a.cliques)) encCliqueCover encCliqueCoverFields 1 1

theorem Cslib.Complexity.encCliqueCover_cliques_deg : Turing.MultiTapeTM.ComputableInDegree CliqueCoverInstance.cliques encCliqueCover Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encCliqueCover_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Graph × ℕ) => { graph := p.1, cliques := p.2 }) encCliqueCoverFields encCliqueCover 1 1

def Cslib.Complexity.encCliqueCover : CliqueCoverInstance ↪ List Bool

Encoding of CliqueCoverInstance as a pair (graph, cliques).

theorem Cslib.Complexity.encCliqueCover_cliques_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → CliqueCoverInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encCliqueCover → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).cliques) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encCliqueCover_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, cliques := x1 x }) encIn encCliqueCover budget

def Cslib.Complexity.Graph.CoveredByCliques (G : Graph) (l : ℕ) : Prop

The declared vertices of G are the union of at most l cliques of the graph induced on them.

def Cslib.Complexity.CliqueCover : Set CliqueCoverInstance

Clique cover [Kar72]: the graphs whose declared vertices are the union of at most the given number of cliques.

@[simp]

theorem Cslib.Complexity.mem_CliqueCover_iff {G : Graph} {l : ℕ} : { graph := G, cliques := l } ∈ CliqueCover ↔ G.CoveredByCliques l

Membership in CliqueCover unfolds to Graph.CoveredByCliques.

theorem Cslib.Complexity.Graph.mem_CliqueCover_iff_compl {G : Graph} {l : ℕ} : { graph := G, cliques := l } ∈ CliqueCover ↔ { graph := G.compl, colors := l } ∈ ChromaticNumber

A graph has a cover by l cliques exactly when its complement is l-colorable.

theorem Cslib.Complexity.Graph.compl_mem_CliqueCover_iff {G : Graph} {k : ℕ} : { graph := G.compl, cliques := k } ∈ CliqueCover ↔ { graph := G, colors := k } ∈ ChromaticNumber

Karp's reduction from ChromaticNumber. A graph is k-colorable exactly when its complement is covered by k cliques.

theorem Cslib.Complexity.polyTimeReducible_ChromaticNumber_CliqueCover : PolyTimeReducible encChromaticNumber encCliqueCover ChromaticNumber CliqueCover

ChromaticNumber reduces to CliqueCover in polynomial time by complementing the graph [Kar72].

theorem Cslib.Complexity.polyTimeReducible_CliqueCover_ChromaticNumber : PolyTimeReducible encCliqueCover encChromaticNumber CliqueCover ChromaticNumber

CliqueCover reduces to ChromaticNumber in polynomial time by complementing the graph.

theorem Cslib.Complexity.CliqueCover.mem_NP : CliqueCover ∈ NP encCliqueCover

CliqueCover belongs to NP.

theorem Cslib.Complexity.CliqueCover_npHard : NPHard encCliqueCover CliqueCover

CliqueCover is NP-hard.

theorem Cslib.Complexity.CliqueCover_npComplete : NPComplete encCliqueCover CliqueCover

Clique cover is NP-complete, with the number of cliques in binary [Kar72].