Paper
Max Independent Set Remains NP-hard when Excluding a Planar Induced Minor
8 pages · 15 marked passages · pdflatex · download PDF · lax-762056
-
Independent Set without a 5×5 induced grid minor
Deciding whether a graph has an independent set of size at least is NP-hard even when the graph excludes the grid as an induced minor. Consequently, Maximum Independent Set is NP-hard on this class.
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 -
Maximum cuts
For a graph on an ordered vertex set, each edge is represented once, by its endpoints . A cut is specified by a subset of vertices; its size is the number of edges with exactly one endpoint in . is the largest such size, with value zero for an edgeless graph.
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 -
Independent Set without a 5×5 induced grid minor
Deciding whether a graph has an independent set of size at least is NP-hard even when the graph excludes the grid as an induced minor. Consequently, Maximum Independent Set is NP-hard on this class.
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 -
Compose the reduction from Max Cut with the graph construction. Exclusion of the induced grid minor gives the target class. The independence-number identity gives equivalence after shifting the threshold.
-
Row and column graphs
For a row set and columns, the graph has vertices . Each column induces a complete bipartite graph between its two sides. Within a row, every vertex is adjacent to both vertices in each consecutive column. There are no other edges.
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 -
The Bonnet–Chang reduction
Order the vertices of as . For every edge with , reserve rows and in an intermediate graph with columns. Keep only columns from through . In row keep only side at column and side at column ; keep both sides at every intervening column. The resulting induced subgraph is .
The additive offset is .
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 -
Induced grid exclusion in row and column graphs
Every row and column graph excludes the grid as an induced minor.
1 import Lax762056.ColumnGraph 2 import Lax762056.Grid 3 … module docstring, 7 lines 11 12 namespace Lax762056.ColumnGridExclusion 13 14 open ColumnGraph Grid 15 16 axiom columnGraph_excludes_inducedGrid (R : Type*) (c : ℕ) : 17 ExcludesInducedGrid 5 (columnGraph R c) 18 19 end Lax762056.ColumnGridExclusion 20 -
Apply the general obstruction to the explicit triple of cycles in the grid.
-
Asteroidal triples of cycles
An asteroidal triple of cycles consists of three vertex-disjoint, pairwise nonadjacent cycles such that every pair is joined by a path avoiding the closed neighborhood of the third.
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 -
Asteroidal cycle triples obstruct induced minors
No graph containing an asteroidal triple of cycles is an induced minor of a row and column graph. The grid contains such a triple.
1 import Lax762056.AsteroidalCycles 2 import Lax762056.ColumnGraph 3 import Lax762056.Grid 4 … module docstring, 8 lines 13 14 namespace Lax762056.CycleObstruction 15 16 open AsteroidalCycles ColumnGraph Grid InducedMinors 17 18 axiom asteroidalCycles_obstruction (R W : Type*) (c : ℕ) (H : SimpleGraph W) 19 (hH : HasAsteroidalCycleTriple H) : 20 ¬ IsInducedMinor H (columnGraph R c) 21 22 axiom grid_five_has_asteroidalCycles : HasAsteroidalCycleTriple (squareGrid 5) 23 24 end Lax762056.CycleObstruction 25 -
Asteroidal cycle triples obstruct induced minors
No graph containing an asteroidal triple of cycles is an induced minor of a row and column graph. The grid contains such a triple.
1 import Lax762056.AsteroidalCycles 2 import Lax762056.ColumnGraph 3 import Lax762056.Grid 4 … module docstring, 8 lines 13 14 namespace Lax762056.CycleObstruction 15 16 open AsteroidalCycles ColumnGraph Grid InducedMinors 17 18 axiom asteroidalCycles_obstruction (R W : Type*) (c : ℕ) (H : SimpleGraph W) 19 (hH : HasAsteroidalCycleTriple H) : 20 ¬ IsInducedMinor H (columnGraph R c) 21 22 axiom grid_five_has_asteroidalCycles : HasAsteroidalCycleTriple (squareGrid 5) 23 24 end Lax762056.CycleObstruction 25 -
no assumptions
Each cycle's branch sets contain opposite sides of a column. The three columns are distinct. The middle column is contained in the middle cycle's closed neighborhood and separates the other two cycles, contradicting their avoiding path.
-
Induced grid exclusion in the reduction
For every finite simple graph , the reduction graph excludes the grid as an induced minor.
1 import Lax762056.Reduction 2 import Lax762056.Grid 3 … module docstring, 8 lines 12 13 namespace Lax762056.GridExclusion 14 15 open Grid Reduction 16 17 axiom reduction_excludes_inducedGrid {n : ℕ} (F : SimpleGraph (Fin n)) : 18 ExcludesInducedGrid 5 (reductionGraph F) 19 20 end Lax762056.GridExclusion 21 -
The independence number records the maximum cut
For every finite simple graph , . An independent set chooses at most one side in each column and so determines a cut of (empty columns may be assigned either side). The two rows for an edge contribute at most vertices, and at most when its endpoints lie on the same side. Conversely, every cut realizes the sum of these bounds.
1 import Lax762056.Reduction 2 … module docstring, 13 lines 16 17 namespace Lax762056.IndependenceIdentity 18 19 open Reduction MaxCut 20 21 axiom independence_eq_maxCut_offset {n : ℕ} (F : SimpleGraph (Fin n)) : 22 (reductionGraph F).indepNum = maxCut F + offset F 23 24 end Lax762056.IndependenceIdentity 25 -
no assumptions
Every independent set induces a cut, with at most the stated number of vertices in each edge's two rows. Conversely, the explicit construction from a maximum cut realizes the bound, including the additional vertex for each crossing edge.
Loading the paper…