Independent Set Reduces to Multicoloured Clique

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

proven

Loading review…

Natural Language Statement

Theorem

Independent Set, parameterized by $k$ , fpt-reduces to Multicoloured Clique, parameterized by the number of colours [FHRV09, Lemma 1], [CFK+15, Theorem 13.7]. The reduction $reduce$ of $WH_F2_MccConstruction$ maps an instance with parameter $k$ to an instance with $k$ colours. It is computable in time $c\,(k+1)^2\,(|x|+1)$ on the words of instances and in polynomial time on all words, so it is also a polynomial-time many-one reduction.

Correctness. An independent set $\{v_0, \dots, v_{k-1}\}$ of $G$ gives the multicoloured clique $\{(c, v_c) : c < k\}$ : its vertices have distinct colours, copy distinct vertices, and copy non-adjacent ones. Conversely, a multicoloured clique $\{(c, v_c) : c < k\}$ yields $k$ distinct vertices $v_c$ , pairwise non-adjacent in $G$ .

Running time. The multicoloured graph has $kn$ vertices, and the program tests each of the $k^2 n^2$ ordered pairs; the word of the instance has at least $n^2$ entries.

The statements are:

statement	content
$construct_correct$	correctness of the construction on graphs
$word_encodes$	the word of the construction encodes the multicoloured graph
$reduce_word$ , $reduce_off_domain$	$reduce$ on the words of instances and on other words
$reduce_maps_domain$ , $reduce_correct$	instances go to instances, yes to yes and no to no
$parameter_preserved$	the parameter is preserved, $k' = k$
$reduce_fptTime$	time $c\,(k+1)^2\,(\lvert x\rvert+1)$ on the word RAM
$independentSet_isFptReduction$ , $independentSet_fptReduces_mcc$	a strict fpt-reduction of $Lax888481$
$reduce_polyTime$ , $independentSet_polyReduces_mcc$	polynomial time on every word; a polynomial-time reduction
$independentSet_le_mcc$	an fpt-reduction in the sense of $WH_A2_FptReductions$

Concept map

19 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 13 statements. Each proof establishes one of them relative to its assumptions.

Lean source view on GitHub

1	import Lax496464.WH_F2_MccConstruction
2	import Lax496464.WH_A2_FptReductions
3	import Lax762056.GraphProblems
4	import Lax759944.RamPolytime
5	import Lax888481.PolynomialReduction
6
7	/-!
8	---
9	title: Independent Set Reduces to Multicoloured Clique
10	type: theorem
11	---
12	**Independent Set, parameterized by $k$ , fpt-reduces to Multicoloured Clique, parameterized by the
13	number of colours** [FHRV09, Lemma 1], [CFK+15, Theorem 13.7]. The reduction `reduce` of
14	`WH_F2_MccConstruction` maps an instance with parameter $k$ to an instance with $k$ colours. It is
15	computable in time $c\,(k+1)^2\,(\|x\|+1)$ on the words of instances and in polynomial time on all
16	words, so it is also a polynomial-time many-one reduction.
17
18	Correctness. An independent set $\{v_0, \dots, v_{k-1}\}$ of $G$ gives the multicoloured
19	clique $\{(c, v_c) : c < k\}$ : its vertices have distinct colours, copy distinct vertices, and copy
20	non-adjacent ones. Conversely, a multicoloured clique $\{(c, v_c) : c < k\}$ yields $k$ distinct
21	vertices $v_c$ , pairwise non-adjacent in $G$ .
22
23	Running time. The multicoloured graph has $kn$ vertices, and the program tests each of the
24	$k^2 n^2$ ordered pairs; the word of the instance has at least $n^2$ entries.
25
26	The statements are:
27
28	\| statement \| content \|
29	\|---\|---\|
30	\| `construct_correct` \| correctness of the construction on graphs \|
31	\| `word_encodes` \| the word of the construction encodes the multicoloured graph \|
32	\| `reduce_word`, `reduce_off_domain` \| `reduce` on the words of instances and on other words \|
33	\| `reduce_maps_domain`, `reduce_correct` \| instances go to instances, yes to yes and no to no \|
34	\| `parameter_preserved` \| the parameter is preserved, $k' = k$ \|
35	\| `reduce_fptTime` \| time $c\,(k+1)^2\,(\lvert x\rvert+1)$ on the word RAM \|
36	\| `independentSet_isFptReduction`, `independentSet_fptReduces_mcc` \| a strict fpt-reduction of `Lax888481` \|
37	\| `reduce_polyTime`, `independentSet_polyReduces_mcc` \| polynomial time on every word; a polynomial-time reduction \|
38	\| `independentSet_le_mcc` \| an fpt-reduction in the sense of `WH_A2_FptReductions` \|
39
40	# Formalization Notes
41
42	Independent Set is `WH_F1_IndependentSetMatrix.problem`, the archive's `Lax762056` Independent
43	Set on adjacency-matrix words; its threshold is a lower bound, and a set of at least $k$ independent
44	vertices contains one of exactly $k$ . For $k = 0$ both sides hold, the empty choice being a
45	multicoloured clique with no colours.
46
47	Words. `word_encodes` states that the word of the construction satisfies the compressed sparse
48	row format of `Lax888481.MulticolouredClique`, with strictly increasing adjacency lists and the
49	colours of the construction. The parameter of a Multicoloured Clique word is its last entry, which
50	is $k$ .
51
52	Two notions of fpt-reduction. `independentSet_isFptReduction` is the strict fpt-reduction of
53	`Lax888481.ParameterizedComplexity`, with time $c\,g(k)\,(\|x\|+1)$ for $g(k) = (k+1)^2$ and new
54	parameter at most $h(k) = k$ . `independentSet_le_mcc` is the fpt-reduction of `WH_A2_FptReductions`.
55
56	Polynomial time. `reduce_polyTime` is `Lax759944.RamPolytime.RamPolytime` on every word,
57	malformed words included; the program first checks in one pass that the word is the encoding of an
58	instance: a run of ones and a zero, a symmetric $0/1$ matrix with zero diagonal whose side is the
59	length of that run, and a run of ones and a zero.
60	-/
61
62	namespace Lax496464.WH_F4_IndependentSetToMcc
63
64	open Lax762056.GraphEncoding (Instance)
65
66	-- The construction
67
68	/-- Correctness of the construction. `G` has an independent set of size at least `k` if
69	and only if the multicoloured graph has a multicoloured clique. -/
70	axiom construct_correct (I : Instance) :
71	Lax762056.GraphProblems.IndependentSet I ↔
72	(WH_F2_MccConstruction.construct I).HasMulticolouredClique
73
74	/-- The word encodes the construction. -/
75	axiom word_encodes (I : Instance) :
76	Lax888481.MulticolouredClique.EncodesInstance (WH_F2_MccConstruction.word I)
77	(WH_F2_MccConstruction.construct I)
78
79	-- The reduction on words
80
81	section Words
82
83	open Lax496464.WH_F1_IndependentSetMatrix (problem)
84	open Lax496464.WH_F2_MccConstruction (reduce)
85
86	/-- On the word of an instance, `reduce` is the word of the construction. -/
87	axiom reduce_word (I : Instance) :
88	reduce (WH_F1_IndependentSetMatrix.word I) = WH_F2_MccConstruction.word I
89
90	/-- On a word that presents no instance, `reduce` is the empty word. -/
91	axiom reduce_off_domain (x : List ℕ) (hx : x ∉ problem.Domain) : reduce x = []
92
93	/-- Instances go to instances. -/
94	axiom reduce_maps_domain :
95	∀ x ∈ problem.Domain, reduce x ∈ Lax888481.MulticolouredClique.problem.Domain
96
97	/-- The answer is preserved. -/
98	axiom reduce_correct :
99	∀ x ∈ problem.Domain, (problem.Yes x ↔ Lax888481.MulticolouredClique.problem.Yes (reduce x))
100
101	/-- The parameter is preserved: `k' = k`. -/
102	axiom parameter_preserved :
103	∀ x ∈ problem.Domain,
104	Lax888481.MulticolouredClique.problem.param (reduce x) = problem.param x
105
106	end Words
107
108	-- Running time and the reductions
109
110	section Time
111
112	open Lax808846.Ram Lax808846.RamComputes Lax888481.ParameterizedComplexity
113	open Lax496464.WH_F1_IndependentSetMatrix (problem)
114	open Lax496464.WH_F2_MccConstruction (reduce)
115
116	/-- Running time in the parameter `k`. At every word length, on every word of an instance whose
117	image fits, one program computes `reduce` within `c * (k + 1) ^ 2 * (\|x\| + 1)` instructions. -/
118	axiom reduce_fptTime :
119	∃ (prog : Program) (c : ℕ), ∀ w : ℕ,
120	ComputesInTime w prog
121	{x \| x ∈ problem.Domain ∧ Fits c w x ∧ Fits c w (reduce x)}
122	reduce (fun x => c * (problem.param x + 1) ^ 2 * (x.length + 1))
123
124	/-- The strict fpt-reduction, with `g k = (k + 1) ^ 2` and `h k = k`. -/
125	axiom independentSet_isFptReduction :
126	∃ (prog : Lax808846.Ram.Program) (c : ℕ),
127	Lax888481.ParameterizedComplexity.IsFptReduction problem
128	Lax888481.MulticolouredClique.problem reduce prog c (fun k => (k + 1) ^ 2) (fun k => k)
129
130	/-- Independent Set strictly fpt-reduces to Multicoloured Clique. -/
131	axiom independentSet_fptReduces_mcc :
132	Lax888481.ParameterizedComplexity.FptReduces problem Lax888481.MulticolouredClique.problem
133
134	/-- Polynomial running time, on every word. -/
135	axiom reduce_polyTime : Lax759944.RamPolytime.RamPolytime reduce
136
137	/-- Independent Set reduces to Multicoloured Clique in polynomial time. -/
138	axiom independentSet_polyReduces_mcc :
139	Lax888481.PolynomialReduction.PolyReduces {x \| problem.Yes x}
140	{x \| Lax888481.MulticolouredClique.problem.Yes x}
141
142	end Time
143
144	-- The fpt-reduction of the library
145
146	section Library
147
148	open Lax496464.WH_A2_FptReductions
149
150	/-- `p-Independent-Set ≤fpt Multicoloured Clique`, on adjacency-matrix words. -/
151	axiom independentSet_le_mcc :
152	WH_F1_IndependentSetMatrix.problem ≤ᶠᵖᵗ Lax888481.MulticolouredClique.problem
153
154	end Library
155
156	end Lax496464.WH_F4_IndependentSetToMcc
157

Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof

Formalization Notes

Independent Set is $WH_F1_IndependentSetMatrix.problem$ , the archive's $Lax762056$ Independent Set on adjacency-matrix words; its threshold is a lower bound, and a set of at least $k$ independent vertices contains one of exactly $k$ . For $k = 0$ both sides hold, the empty choice being a multicoloured clique with no colours.

Words. $word_encodes$ states that the word of the construction satisfies the compressed sparse row format of $Lax888481.MulticolouredClique$ , with strictly increasing adjacency lists and the colours of the construction. The parameter of a Multicoloured Clique word is its last entry, which is $k$ .

Two notions of fpt-reduction. $independentSet_isFptReduction$ is the strict fpt-reduction of $Lax888481.ParameterizedComplexity$ , with time $c\,g(k)\,(|x|+1)$ for $g(k) = (k+1)^2$ and new parameter at most $h(k) = k$ . $independentSet_le_mcc$ is the fpt-reduction of $WH_A2_FptReductions$ .

Polynomial time. $reduce_polyTime$ is $Lax759944.RamPolytime.RamPolytime$ on every word, malformed words included; the program first checks in one pass that the word is the encoding of an instance: a run of ones and a zero, a symmetric $0/1$ matrix with zero diagonal whose side is the length of that run, and a run of ones and a zero.

Builds on

Used by

Lax496464.WH_F5_MccNPHard

From Mathlib

none

Discussion

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

Loading discussion…

Lax Lean Archive

Independent Set Reduces to Multicoloured Clique

Flags

Flag this concept

Natural Language Statement

Theorem

1 `construct_correct` proven

2 `independentSet_fptReduces_mcc` proven

3 `independentSet_isFptReduction` proven

4 `independentSet_le_mcc` proven

5 `independentSet_polyReduces_mcc` proven

6 `parameter_preserved` proven

7 `reduce_correct` proven

8 `reduce_fptTime` proven

9 `reduce_maps_domain` proven

10 `reduce_off_domain` proven

11 `reduce_polyTime` proven

12 `reduce_word` proven

13 `word_encodes` proven

Lean source view on GitHub

Discussion

Settings