Cliques

Clique is the set of graphs with a clique of a given number of their vertices Arora and Barak, Section 2.4. A set of vertices is independent in a graph exactly when it is a clique in the complement of the graph on its vertices (Graph.compl), so complementing the graph reduces IndependentSet to Clique [Kar72]. The verifier is Cslib.Complexity.Graph.verifySubset for adjacency, an instance of the subset-witness verifier Cslib.Complexity.subsetVerifier.

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.Clique. 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.CliqueInstance, Cslib.Complexity.Clique, Cslib.Complexity.Graph.compl.
• Cslib.Complexity.Graph.cliqueNum: the clique number (G.induced.cliqueNum).
• Cslib.Complexity.Clique.verifier.

Main results

• Cslib.Complexity.mem_Clique_iff: cliques as subsets of ℕ contained in the declared vertices.
• Cslib.Complexity.Graph.induced_compl, Cslib.Complexity.Graph.compl_mem_Clique_iff: G.compl.induced = G.inducedᶜ and (G.compl, m) ∈ Clique ↔ (G, m) ∈ IndependentSet.
• Cslib.Complexity.Graph.compl_mem_IndependentSet_iff: (G.compl, m) ∈ IndependentSet ↔ (G, m) ∈ Clique.
• Cslib.Complexity.Graph.le_cliqueNum_iff, Cslib.Complexity.Graph.cliqueNum_compl: the clique number is the largest target of Clique, and that of the complement is the independence number.
• Cslib.Complexity.Graph.computableInPolyTime_compl: complementing a graph on its declared vertices is polynomial-time.
• Cslib.Complexity.Clique.mem_NP: Clique ∈ NP encCliqueInstance.
• Cslib.Complexity.polyTimeReducible_IndependentSet_Clique, Cslib.Complexity.polyTimeReducible_Clique_IndependentSet: IndependentSet and Clique reduce to each other in polynomial time.
• Cslib.Complexity.Clique_npHard: Clique is NP-hard.
• Cslib.Complexity.Clique_npComplete: Clique is NP-complete.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• R. M. Karp, Reducibility among combinatorial problems

structure Cslib.Complexity.CliqueInstance : Type

An instance (graph, m) of Clique.

• graph : Graph

  The graph in which to find a clique.

• m : ℕ

  The target number of declared vertices.

theorem Cslib.Complexity.CliqueInstance.ext_iff {x y : CliqueInstance} : x = y ↔ x.graph = y.graph ∧ x.m = y.m

theorem Cslib.Complexity.CliqueInstance.ext {x y : CliqueInstance} (graph : x.graph = y.graph) (m : x.m = y.m) : x = y

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqCliqueInstance : DecidableEq CliqueInstance

def Cslib.Complexity.instDecidableEqCliqueInstance.decEq (x✝ x✝¹ : CliqueInstance) : Decidable (x✝ = x✝¹)

def Cslib.Complexity.instReprCliqueInstance.repr : CliqueInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instReprCliqueInstance : Repr CliqueInstance

@[instance_reducible]

instance Cslib.Complexity.instInhabitedCliqueInstance : Inhabited CliqueInstance

theorem Cslib.Complexity.encCliqueInstance_m_deg : Turing.MultiTapeTM.ComputableInDegree CliqueInstance.m encCliqueInstance Turing.MultiTapeTM.encNat 1 1

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

theorem Cslib.Complexity.encCliqueInstance_m_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → CliqueInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encCliqueInstance → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).m) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encCliqueInstance_m_inO : Turing.MultiTapeTM.ComputableInO CliqueInstance.m encCliqueInstance Turing.MultiTapeTM.encNat (fun (a : CliqueInstance) => (encCliqueInstance a).length) fun (a : CliqueInstance) => (encCliqueInstance a).length

theorem Cslib.Complexity.encCliqueInstance_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Graph × ℕ) => { graph := p.1, m := p.2 }) encCliqueInstanceFields encCliqueInstance 1 1

@[reducible, inline]

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

The tuple of the fields of encCliqueInstance.

theorem Cslib.Complexity.encCliqueInstance_graph_inO : Turing.MultiTapeTM.ComputableInO CliqueInstance.graph encCliqueInstance encGraph (fun (a : CliqueInstance) => (encCliqueInstance a).length) fun (a : CliqueInstance) => (encCliqueInstance a).length

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

@[simp]

theorem Cslib.Complexity.encCliqueInstance_apply (a : CliqueInstance) : encCliqueInstance a = encCliqueInstanceFields (a.graph, a.m)

theorem Cslib.Complexity.encCliqueInstance_graph_deg : Turing.MultiTapeTM.ComputableInDegree CliqueInstance.graph encCliqueInstance encGraph 1 1

theorem Cslib.Complexity.encCliqueInstance_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, m := x1 x }) encIn encCliqueInstance budget

theorem Cslib.Complexity.encCliqueInstance_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : CliqueInstance) => (a.graph, a.m)) encCliqueInstance encCliqueInstanceFields 1 1

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

theorem Cslib.Complexity.encCliqueInstance_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, m := x1 x }) encIn encCliqueInstance

theorem Cslib.Complexity.encCliqueInstance_m_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → CliqueInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encCliqueInstance S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).m) encIn✝ Turing.MultiTapeTM.encNat S✝

def Cslib.Complexity.encCliqueInstance : CliqueInstance ↪ List Bool

Framed encGraph followed by binary target encNat, encoding CliqueInstance.

def Cslib.Complexity.Clique : Set CliqueInstance

The graphs with a clique of m of their vertices.

theorem Cslib.Complexity.mem_Clique_iff {x : CliqueInstance} : x ∈ Clique ↔ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ x.graph.vertices) ∧ x.graph.toSimpleGraph.IsNClique x.m S

Membership in Clique as a finite set of m declared vertices that is a clique in x.graph.toSimpleGraph.

@[simp]

theorem Cslib.Complexity.mem_Clique_iff_mk {G : Graph} {m : ℕ} : { graph := G, m := m } ∈ Clique ↔ ∃ (S : Finset ℕ), (∀ v ∈ S, v ∈ G.vertices) ∧ G.toSimpleGraph.IsNClique m S

def Cslib.Complexity.Graph.compl (G : Graph) : Graph

The complement of a graph on its vertices: an edge between any two distinct vertices that are not adjacent.

theorem Cslib.Complexity.Graph.compl_adj_iff {G : Graph} {u v : ℕ} (hu : u ∈ G.vertices) (hv : v ∈ G.vertices) : G.compl.toSimpleGraph.Adj u v ↔ u ≠ v ∧ ¬G.toSimpleGraph.Adj u v

On the vertices of a graph, adjacency in the complement is non-adjacency in the graph.

@[simp]

theorem Cslib.Complexity.Graph.induced_compl (G : Graph) : G.compl.induced = G.inducedᶜ

The induced graph of the complement is the complement of the induced graph.

theorem Cslib.Complexity.Graph.compl_mem_Clique_iff (G : Graph) (m : ℕ) : { graph := G.compl, m := m } ∈ Clique ↔ { graph := G, m := m } ∈ IndependentSet

Independent sets are cliques of the complement.

theorem Cslib.Complexity.Graph.compl_mem_IndependentSet_iff (G : Graph) (m : ℕ) : { graph := G.compl, m := m } ∈ IndependentSet ↔ { graph := G, m := m } ∈ Clique

Cliques are independent sets of the complement.

theorem Cslib.Complexity.Graph.computableInPolyTime_compl : Turing.MultiTapeTM.ComputableInPolyTime compl encGraph encGraph

Complementing a graph on its declared vertices is polynomial-time with the graph encoding.

def Cslib.Complexity.Clique.verifier : CliqueInstance × List Bool → Bool

The verifier for Clique: select distinct declared vertices from the certificate mask, check that their count equals m, and check that every two distinct selected vertices are adjacent.

theorem Cslib.Complexity.Clique.isVerifier : IsVerifier encCliqueInstance Polynomial.X verifier Clique

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

theorem Cslib.Complexity.Clique.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encCliqueInstance Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The Clique verifier is polynomial-time.

theorem Cslib.Complexity.Clique.mem_NP : Clique ∈ NP encCliqueInstance

Clique belongs to NP.

def Cslib.Complexity.independentSetToClique (x : IndependentSetInstance) : CliqueInstance

Complementing the graph reduces IndependentSet to Clique.

theorem Cslib.Complexity.computableInPolyTime_independentSetToClique : Turing.MultiTapeTM.ComputableInPolyTime independentSetToClique encIndependentSetInstance encCliqueInstance

theorem Cslib.Complexity.independentSetToClique_mem_iff (x : IndependentSetInstance) : independentSetToClique x ∈ Clique ↔ x ∈ IndependentSet

def Cslib.Complexity.cliqueToIndependentSet (x : CliqueInstance) : IndependentSetInstance

Complementing the graph reduces Clique to IndependentSet.

theorem Cslib.Complexity.computableInPolyTime_cliqueToIndependentSet : Turing.MultiTapeTM.ComputableInPolyTime cliqueToIndependentSet encCliqueInstance encIndependentSetInstance

theorem Cslib.Complexity.cliqueToIndependentSet_mem_iff (x : CliqueInstance) : cliqueToIndependentSet x ∈ IndependentSet ↔ x ∈ Clique

theorem Cslib.Complexity.polyTimeReducible_IndependentSet_Clique : PolyTimeReducible encIndependentSetInstance encCliqueInstance IndependentSet Clique

IndependentSet reduces to Clique in polynomial time by complementing the graph on its declared vertices.

theorem Cslib.Complexity.polyTimeReducible_Clique_IndependentSet : PolyTimeReducible encCliqueInstance encIndependentSetInstance Clique IndependentSet

Clique reduces to IndependentSet in polynomial time by complementing the graph on its declared vertices.

theorem Cslib.Complexity.Clique_npHard : NPHard encCliqueInstance Clique

Clique is NP-hard.

theorem Cslib.Complexity.Clique_npComplete : NPComplete encCliqueInstance Clique

Clique is NP-complete.

The clique number

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

The clique number of a graph: the largest number of declared vertices that are pairwise adjacent.

theorem Cslib.Complexity.Graph.mem_Clique_of_le {G : Graph} {k k' : ℕ} (h : { graph := G, m := k } ∈ Clique) (hk : k' ≤ k) : { graph := G, m := k' } ∈ Clique

Fewer vertices of a clique form a clique.

theorem Cslib.Complexity.Graph.le_cliqueNum_iff {G : Graph} {k : ℕ} : k ≤ G.cliqueNum ↔ { graph := G, m := k } ∈ Clique

The clique number is the largest target of Clique.

theorem Cslib.Complexity.Graph.le_card_of_mem_Clique {G : Graph} {k : ℕ} (h : { graph := G, m := k } ∈ Clique) : k ≤ G.vertices.toFinset.card

A clique has at most as many vertices as the distinct declared vertices.

theorem Cslib.Complexity.Graph.cliqueNum_compl (G : Graph) : G.compl.cliqueNum = G.indepNum

Cliques of the complement are independent sets: the clique number of the complement on the declared vertices is the independence number.