Paper

Max Independent Set Remains NP-hard when Excluding a Planar Induced Minor

8 pages · 15 marked passages · pdflatex · download PDF · lax-762056

1	import Lax762056.Grid
2	import Lax762056.GraphProblems
3
	… module docstring, 9 lines
13
14	namespace Lax762056.IndependentSetHardness
15
16	open GraphProblems Grid
17
18	axiom independentSet_inducedGrid_hardness :
19	NPHardOn IndependentSet (ExcludesInducedGrid 5)
20
21	end Lax762056.IndependentSetHardness
22

1	import Lax762056.GraphEncoding
2
	… module docstring, 11 lines
14
15	namespace Lax762056.MaxCut
16
17	open Finset
18
19	noncomputable def edges {n : ℕ} (F : SimpleGraph (Fin n)) :
20	Finset (Fin n × Fin n) := by
21	classical
22	exact univ.filter fun e => e.1 < e.2 ∧ F.Adj e.1 e.2
23
24	noncomputable def cutSize {n : ℕ} (F : SimpleGraph (Fin n))
25	(S : Finset (Fin n)) : ℕ := by
26	classical
27	exact ((edges F).filter fun e =>
28	(e.1 ∈ S ∧ e.2 ∉ S) ∨ (e.1 ∉ S ∧ e.2 ∈ S)).card
29
30	noncomputable def maxCut {n : ℕ} (F : SimpleGraph (Fin n)) : ℕ :=
31	(univ : Finset (Fin n)).powerset.sup (cutSize F)
32
33	end Lax762056.MaxCut
34

1	import Lax762056.Grid
2	import Lax762056.GraphProblems
3
	… module docstring, 9 lines
13
14	namespace Lax762056.IndependentSetHardness
15
16	open GraphProblems Grid
17
18	axiom independentSet_inducedGrid_hardness :
19	NPHardOn IndependentSet (ExcludesInducedGrid 5)
20
21	end Lax762056.IndependentSetHardness
22

1	import Mathlib.Combinatorics.SimpleGraph.Basic
2
	… module docstring, 11 lines
14
15	namespace Lax762056.ColumnGraph
16
17	open SimpleGraph
18
19	abbrev Vertex (R : Type*) (c : ℕ) := R × Fin c × Bool
20
21	def columnGraph (R : Type*) (c : ℕ) : SimpleGraph (Vertex R c) :=
22	fromRel fun (row, column, side) (row', column', side') =>
23	(column = column' ∧ side ≠ side') ∨
24	(row = row' ∧ (column.val + 1 = column'.val ∨ column'.val + 1 = column.val))
25
26	end Lax762056.ColumnGraph
27

1	import Lax762056.ColumnGraph
2	import Lax762056.MaxCut
3
	… module docstring, 13 lines
17
18	namespace Lax762056.Reduction
19
20	open ColumnGraph MaxCut
21
22	abbrev Edge {n : ℕ} (F : SimpleGraph (Fin n)) :=
23	{e : Fin n × Fin n // e.1 < e.2 ∧ F.Adj e.1 e.2}
24
25	abbrev Row {n : ℕ} (F : SimpleGraph (Fin n)) := Edge F × Bool
26
27	abbrev Vertex {n : ℕ} (F : SimpleGraph (Fin n)) :=
28	ColumnGraph.Vertex (Row F) (2 * n - 1)
29
30	def retainedVertices {n : ℕ} (F : SimpleGraph (Fin n)) : Set (Vertex F) :=
31	fun ((edge, tag), column, side) =>
32	let u := edge.val.1.val
33	let v := edge.val.2.val
34	let j := column.val
35	(j = 2 * u ∧ side = tag) ∨
36	(2 * u < j ∧ j < 2 * v) ∨
37	(j = 2 * v ∧ side = !tag)
38
39	def reductionGraph {n : ℕ} (F : SimpleGraph (Fin n)) :
40	SimpleGraph (retainedVertices F) :=
41	(columnGraph (Row F) (2 * n - 1)).induce (retainedVertices F)
42
43	noncomputable def offset {n : ℕ} (F : SimpleGraph (Fin n)) : ℕ :=
44	2 * ∑ e ∈ edges F, (e.2.val - e.1.val)
45
46	end Lax762056.Reduction
47

Lax Lean Archive

1	import Mathlib.Combinatorics.SimpleGraph.Paths
2
	… module docstring, 9 lines
12
13	namespace Lax762056.AsteroidalCycles
14
15	open SimpleGraph
16
17	def AvoidsClosedNeighborhood {V : Type*} (G : SimpleGraph V)
18	(S T : Set V) : Prop :=
19	∀ x ∈ S, ∀ y ∈ T, x ≠ y ∧ ¬ G.Adj x y
20
21	def HasAsteroidalCycleTriple {V : Type*} (G : SimpleGraph V) : Prop :=
22	∃ (base : Fin 3 → V) (cycle : ∀ i, Walk G (base i) (base i)),
23	(∀ i, (cycle i).IsCycle) ∧
24	(Pairwise fun i j => AvoidsClosedNeighborhood G
25	{v \| v ∈ (cycle i).support} {v \| v ∈ (cycle j).support}) ∧
26	(∀ i j k, i ≠ j → i ≠ k → j ≠ k →
27	∃ u ∈ (cycle i).support, ∃ v ∈ (cycle j).support,
28	∃ p : Path G u v, AvoidsClosedNeighborhood G
29	{x \| x ∈ p.val.support} {x \| x ∈ (cycle k).support})
30
31	end Lax762056.AsteroidalCycles
32