Clique, Independent Set and Dominating Set

Lax496464.WH_C1_GraphProblems · concepts/Lax496464/WH_C1_GraphProblems.lean · lax-496464

definition

Loading review…

Natural Language Statement

Definition

Three graph problems parameterized by the solution size [FG06, Section 1.2].

$p$ -Clique. Instance: a graph $G$ and $k \in \mathbb N$ . Parameter: $k$ . Question: does $G$ have a clique of $k$ vertices?

$p$ -Independent-Set. The same with $k$ pairwise non-adjacent vertices.

$p$ -Dominating-Set. The same with $k$ vertices such that every vertex is one of them or adjacent to one of them.

Concept map

6 concepts; 8 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Lax888481.ParameterizedComplexity
2	import Lax271696.VertexCover
3	import Mathlib.Combinatorics.SimpleGraph.Clique
4
5	/-!
6	---
7	title: Clique, Independent Set and Dominating Set
8	type: definition
9	---
10	Three graph problems parameterized by the solution size [FG06, Section 1.2].
11
12	$p$ -Clique. Instance: a graph $G$ and $k \in \mathbb N$ . Parameter: $k$ . Question: does
13	$G$ have a clique of $k$ vertices?
14
15	$p$ -Independent-Set. The same with $k$ pairwise non-adjacent vertices.
16
17	$p$ -Dominating-Set. The same with $k$ vertices such that every vertex is one of them or adjacent
18	to one of them.
19
20	# Formalization Notes
21
22	The three problems share the archive's format for a graph with a parameter
23	(`Lax271696.VertexCover.EncodesParamInstance`): the compressed sparse row encoding of the graph
24	followed by $k$ . The parameter is the last entry. Solution sizes are exact; for cliques and
25	independent sets this is equivalent to "at least $k$ ", and for dominating sets to "at most $k$ "
26	whenever $k$ does not exceed the number of vertices.
27
28	Multicoloured Clique is the archive's `Lax888481.MulticolouredClique.problem`, on the same graph
29	encoding followed by the colours (`WH_D12_MulticolouredClique`).
30	-/
31
32	namespace Lax496464.WH_C1_GraphProblems
33
34	open Lax271696.VertexCover
35	open Lax888481.ParameterizedComplexity (Problem)
36
37	/-- The words that present a graph with a parameter. -/
38	def GraphInstances : Set (List ℕ) := {x \| ∃ n G k, EncodesParamInstance x n G k}
39
40	/-- `p-Clique`. -/
41	def Clique : Problem where
42	Domain := GraphInstances
43	Yes x := ∃ n G k, EncodesParamInstance x n G k ∧ ∃ s : Finset (Fin n), G.IsNClique k s
44	param x := x.getLast?.getD 0
45
46	/-- `p-Independent-Set`. -/
47	def IndependentSet : Problem where
48	Domain := GraphInstances
49	Yes x := ∃ n G k, EncodesParamInstance x n G k ∧ ∃ s : Finset (Fin n), Gᶜ.IsNClique k s
50	param x := x.getLast?.getD 0
51
52	/-- `p-Dominating-Set`. -/
53	def DominatingSet : Problem where
54	Domain := GraphInstances
55	Yes x := ∃ n G k, EncodesParamInstance x n G k ∧
56	∃ s : Finset (Fin n), s.card = k ∧ ∀ v, v ∈ s ∨ ∃ u ∈ s, G.Adj u v
57	param x := x.getLast?.getD 0
58
59	end Lax496464.WH_C1_GraphProblems
60

Formalization Notes

The three problems share the archive's format for a graph with a parameter ( $Lax271696.VertexCover.EncodesParamInstance$ ): the compressed sparse row encoding of the graph followed by $k$ . The parameter is the last entry. Solution sizes are exact; for cliques and independent sets this is equivalent to "at least $k$ ", and for dominating sets to "at most $k$ " whenever $k$ does not exceed the number of vertices.

Multicoloured Clique is the archive's $Lax888481.MulticolouredClique.problem$ , on the same graph encoding followed by the colours ( $WH_D12_MulticolouredClique$ ).

Builds on

Used by

From Mathlib

Mathlib.Combinatorics.SimpleGraph.Clique

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Clique, Independent Set and Dominating Set

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments