Vertex Cover reduces to Steiner Tree

The classical reduction, read in the tagged framework (DescriptiveComplexity.steinerInterp, tag Fin 3, dimension 2): a marked graph becomes the bipartite incidence structure of its edges, plus a root joined to every vertex.

• tag 0 on the diagonal carries the vertices of the input;
• tag 1 on adjacent off-diagonal pairs carries the edges, which are the terminals;
• tag 2 on the diagonal of the minimum carries the root, also a terminal;
• everything else is junk: isolated, non-terminal, unmarked, and therefore never in a chosen set.

A connected set containing all terminals must join every edge-terminal to the root, and an edge's only neighbours are its two endpoints, so the vertices it uses form a vertex cover; conversely a vertex cover joins every edge to the root through one of its endpoints. Since vertices are the only non-terminals, the budget counts exactly the cover, and the marked diagonal transports the threshold unchanged.

The root is a single fresh element, so – as for the fresh variable of DescriptiveComplexity.Problems.NaeSat – this is an ordered reduction: an interpretation adds elements only by tags, and a tag contributes a whole copy of the universe, so the root has to be picked out inside its copy as the minimum (DescriptiveComplexity.minF).

@[reducible, inline]

abbrev DescriptiveComplexity.sAdjSym : (FirstOrder.Language.markedGraph.sum FirstOrder.Language.order).Relations 2

The adjacency symbol over the ordered expansion of marked graphs.

Equations

• DescriptiveComplexity.sAdjSym = Sum.inl FirstOrder.Language.mgAdj

@[reducible, inline]

abbrev DescriptiveComplexity.sMarkedSym : (FirstOrder.Language.markedGraph.sum FirstOrder.Language.order).Relations 1

The mark symbol over the ordered expansion of marked graphs.

Equations

• DescriptiveComplexity.sMarkedSym = Sum.inl FirstOrder.Language.mgMarked

inductive DescriptiveComplexity.SteinerTag : Type

The three sorts of point of the interpreted structure. Tags built from constructors, rather than Fin 3, so that the tag match inside the defining formulas reduces definitionally in the characterization proofs.

• vertex : SteinerTag

  A vertex of the input graph, carried by the diagonal.

• edge : SteinerTag

  An edge of the input graph, carried by an adjacent off-diagonal pair.

• root : SteinerTag

  The root, carried by the diagonal of the minimum.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSteinerTag : DecidableEq SteinerTag

Equations

• DescriptiveComplexity.instDecidableEqSteinerTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.instFintypeSteinerTag : Fintype SteinerTag

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DescriptiveComplexity.instInhabitedSteinerTag : Inhabited SteinerTag

Equations

• DescriptiveComplexity.instInhabitedSteinerTag = { default := DescriptiveComplexity.SteinerTag.vertex }

noncomputable def DescriptiveComplexity.steinerInterp : FOInterpretation (FirstOrder.Language.markedGraph.sum FirstOrder.Language.order) FirstOrder.Language.steinerGraph SteinerTag 2

The interpretation of Vertex Cover into Steiner Tree.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.vPt {A : Type} (v : A) : steinerInterp.Map A

The point carrying the vertex v.

Equations

• DescriptiveComplexity.vPt v = (DescriptiveComplexity.SteinerTag.vertex, ![v, v])

def DescriptiveComplexity.ePt {A : Type} (u v : A) : steinerInterp.Map A

The point carrying the (oriented) edge (u, v).

Equations

• DescriptiveComplexity.ePt u v = (DescriptiveComplexity.SteinerTag.edge, ![u, v])

def DescriptiveComplexity.rPt {A : Type} (m : A) : steinerInterp.Map A

The point carrying the root, at the minimum m.

Equations

• DescriptiveComplexity.rPt m = (DescriptiveComplexity.SteinerTag.root, ![m, m])

theorem DescriptiveComplexity.vPt_injective {A : Type} : Function.Injective vPt

Shapes

The three master characterizations, from which the point-level lemmas above and the case analyses of the correctness proof follow.

theorem DescriptiveComplexity.steiner_adj_iff {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (t t' : SteinerTag) (w w' : Fin 2 → A) : STAdj (t, w) (t', w') ↔ t = SteinerTag.vertex ∧ t' = SteinerTag.edge ∧ w 0 = w 1 ∧ (MGAdj (w' 0) (w' 1) ∧ w' 0 ≠ w' 1) ∧ (w 0 = w' 0 ∨ w 0 = w' 1) ∨ t = SteinerTag.root ∧ t' = SteinerTag.vertex ∧ w 0 = w 1 ∧ (∀ (a : A), w 0 ≤ a) ∧ w' 0 = w' 1

theorem DescriptiveComplexity.steiner_terminal_iff {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (t : SteinerTag) (w : Fin 2 → A) : STTerminal (t, w) ↔ t = SteinerTag.edge ∧ MGAdj (w 0) (w 1) ∧ w 0 ≠ w 1 ∨ t = SteinerTag.root ∧ w 0 = w 1 ∧ ∀ (a : A), w 0 ≤ a

theorem DescriptiveComplexity.steiner_marked_iff {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (t : SteinerTag) (w : Fin 2 → A) : STMarked (t, w) ↔ t = SteinerTag.vertex ∧ w 0 = w 1 ∧ MGMarked (w 0)

@[simp]

theorem DescriptiveComplexity.steiner_adj_ve {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (v u w : A) : STAdj (vPt v) (ePt u w) ↔ (MGAdj u w ∧ u ≠ w) ∧ (v = u ∨ v = w)

@[simp]

theorem DescriptiveComplexity.steiner_adj_rv {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (m v : A) : STAdj (rPt m) (vPt v) ↔ ∀ (a : A), m ≤ a

@[simp]

theorem DescriptiveComplexity.steiner_terminal_e {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (u v : A) : STTerminal (ePt u v) ↔ MGAdj u v ∧ u ≠ v

@[simp]

theorem DescriptiveComplexity.steiner_terminal_r {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (m : A) : STTerminal (rPt m) ↔ ∀ (a : A), m ≤ a

@[simp]

theorem DescriptiveComplexity.steiner_terminal_v {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (v : A) : ¬STTerminal (vPt v)

@[simp]

theorem DescriptiveComplexity.steiner_marked_v {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (v : A) : STMarked (vPt v) ↔ MGMarked v

theorem DescriptiveComplexity.steiner_marked_shape {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {p : steinerInterp.Map A} (h : STMarked p) : ∃ (v : A), p = vPt v

A marked point of the interpreted structure is a vertex point.

theorem DescriptiveComplexity.steiner_terminal_shape {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {p : steinerInterp.Map A} (h : STTerminal p) : (∃ (u : A) (v : A), p = ePt u v ∧ MGAdj u v ∧ u ≠ v) ∨ ∃ (r : A), p = rPt r ∧ ∀ (a : A), r ≤ a

A terminal of the interpreted structure is an edge point or the root.

theorem DescriptiveComplexity.steiner_link_ePt {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {S : steinerInterp.Map A → Prop} {u v : A} {q : steinerInterp.Map A} (h : Link STAdj S (ePt u v) q) : (q = vPt u ∨ q = vPt v) ∧ S q

The neighbours of an edge point are the points of its two endpoints.

Counting on the vertex points

theorem DescriptiveComplexity.ncard_vPt_eq {A : Type} (P : A → Prop) (Q : steinerInterp.Map A → Prop) (hshape : ∀ (p : steinerInterp.Map A), Q p → ∃ (v : A), p = vPt v) (hP : ∀ (v : A), Q (vPt v) ↔ P v) : {p : steinerInterp.Map A | Q p}.ncard = {v : A | P v}.ncard

A predicate holding only of vertex points encodes the same number as its restriction to the vertices.

Correctness

theorem DescriptiveComplexity.hasSmallVertexCover_iff_steiner_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : HasSmallVertexCover A ↔ HasSmallSteinerTree (steinerInterp.Map A)

Correctness of the interpretation: a graph has a vertex cover at most as large as its marked set iff the associated incidence structure has a Steiner tree of the same budget.

noncomputable def DescriptiveComplexity.vertexCover_ordered_fo_reduction_steinerTree : OrderedFOReduction VertexCover SteinerTree

Vertex Cover ordered-FO-reduces to Steiner Tree: the edges become the terminals, the vertices the available Steiner points, and the minimum of a spare copy the root joining them all.

Equations

• One or more equations did not get rendered due to their size.

The edge-weighted variant

The same construction, with one clause changed: the marked set must now count k plus one unit per edge point, since a Steiner tree of the incidence structure spends one edge joining each edge point to an endpoint before it can spend anything on the cover. Marking the edge points themselves is exactly that budget, and it needs no arithmetic in the formulas.

noncomputable def DescriptiveComplexity.steinerEdgeInterp : FOInterpretation (FirstOrder.Language.markedGraph.sum FirstOrder.Language.order) FirstOrder.Language.steinerGraph SteinerTag 2

The interpretation of Vertex Cover into the edge-weighted Steiner Tree: as DescriptiveComplexity.steinerInterp, but the marked set also contains every edge point.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.veePt {A : Type} (v : A) : steinerEdgeInterp.Map A

The vertex point of the edge-weighted interpretation.

Equations

• DescriptiveComplexity.veePt v = (DescriptiveComplexity.SteinerTag.vertex, ![v, v])

def DescriptiveComplexity.eeePt {A : Type} (u v : A) : steinerEdgeInterp.Map A

The edge point of the edge-weighted interpretation.

Equations

• DescriptiveComplexity.eeePt u v = (DescriptiveComplexity.SteinerTag.edge, ![u, v])

def DescriptiveComplexity.reePt {A : Type} (m : A) : steinerEdgeInterp.Map A

The root point of the edge-weighted interpretation.

Equations

• DescriptiveComplexity.reePt m = (DescriptiveComplexity.SteinerTag.root, ![m, m])

theorem DescriptiveComplexity.veePt_injective {A : Type} : Function.Injective veePt

theorem DescriptiveComplexity.steinerE_adj_iff {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (t t' : SteinerTag) (w w' : Fin 2 → A) : STAdj (t, w) (t', w') ↔ t = SteinerTag.vertex ∧ t' = SteinerTag.edge ∧ w 0 = w 1 ∧ (MGAdj (w' 0) (w' 1) ∧ w' 0 ≠ w' 1) ∧ (w 0 = w' 0 ∨ w 0 = w' 1) ∨ t = SteinerTag.root ∧ t' = SteinerTag.vertex ∧ w 0 = w 1 ∧ (∀ (a : A), w 0 ≤ a) ∧ w' 0 = w' 1

theorem DescriptiveComplexity.steinerE_terminal_iff {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (t : SteinerTag) (w : Fin 2 → A) : STTerminal (t, w) ↔ t = SteinerTag.edge ∧ MGAdj (w 0) (w 1) ∧ w 0 ≠ w 1 ∨ t = SteinerTag.root ∧ w 0 = w 1 ∧ ∀ (a : A), w 0 ≤ a

theorem DescriptiveComplexity.steinerE_marked_iff {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (t : SteinerTag) (w : Fin 2 → A) : STMarked (t, w) ↔ t = SteinerTag.vertex ∧ w 0 = w 1 ∧ MGMarked (w 0) ∨ t = SteinerTag.edge ∧ MGAdj (w 0) (w 1) ∧ w 0 ≠ w 1

@[simp]

theorem DescriptiveComplexity.steinerE_adj_ve {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (v u w : A) : STAdj (veePt v) (eeePt u w) ↔ (MGAdj u w ∧ u ≠ w) ∧ (v = u ∨ v = w)

@[simp]

theorem DescriptiveComplexity.steinerE_adj_rv {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (m v : A) : STAdj (reePt m) (veePt v) ↔ ∀ (a : A), m ≤ a

@[simp]

theorem DescriptiveComplexity.steinerE_terminal_e {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (u v : A) : STTerminal (eeePt u v) ↔ MGAdj u v ∧ u ≠ v

@[simp]

theorem DescriptiveComplexity.steinerE_terminal_r {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (m : A) : STTerminal (reePt m) ↔ ∀ (a : A), m ≤ a

@[simp]

theorem DescriptiveComplexity.steinerE_terminal_v {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (v : A) : ¬STTerminal (veePt v)

@[simp]

theorem DescriptiveComplexity.steinerE_marked_v {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (v : A) : STMarked (veePt v) ↔ MGMarked v

@[simp]

theorem DescriptiveComplexity.steinerE_marked_e {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (u v : A) : STMarked (eeePt u v) ↔ MGAdj u v ∧ u ≠ v

theorem DescriptiveComplexity.steinerE_link_ePt {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {S : steinerEdgeInterp.Map A → Prop} {u v : A} {q : steinerEdgeInterp.Map A} (h : Link STAdj S (eeePt u v) q) : (q = veePt u ∨ q = veePt v) ∧ S q

The neighbours of an edge point are the points of its two endpoints.

Correctness of the edge-weighted reduction

def DescriptiveComplexity.EdgePtSet (A : Type) [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] : Set (steinerEdgeInterp.Map A)

The edge points of the interpreted structure: what the marked set pays for before any cover.

Equations

• DescriptiveComplexity.EdgePtSet A = {p : DescriptiveComplexity.steinerEdgeInterp.Map A | ∃ (u : A) (v : A), (DescriptiveComplexity.MGAdj u v ∧ u ≠ v) ∧ p = DescriptiveComplexity.eeePt u v}

theorem DescriptiveComplexity.steinerE_terminal_shape {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {p : steinerEdgeInterp.Map A} (h : STTerminal p) : p ∈ EdgePtSet A ∨ ∃ (r : A), p = reePt r ∧ ∀ (a : A), r ≤ a

theorem DescriptiveComplexity.steinerE_marked_shape {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {p : steinerEdgeInterp.Map A} (h : STMarked p) : (∃ (v : A), p = veePt v ∧ MGMarked v) ∨ p ∈ EdgePtSet A

theorem DescriptiveComplexity.ncard_marked_edge {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Finite A] : {p : steinerEdgeInterp.Map A | STMarked p}.ncard = {v : A | MGMarked v}.ncard + (EdgePtSet A).ncard

The marked set of the interpreted structure is one unit per edge point, plus the marked vertices.

theorem DescriptiveComplexity.hasSmallVertexCover_iff_edgeSteiner_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : HasSmallVertexCover A ↔ HasSmallEdgeSteinerTree (steinerEdgeInterp.Map A)

Correctness of the edge-weighted interpretation: a graph has a vertex cover at most as large as its marked set iff the associated incidence structure has an edge-weighted Steiner tree within the enlarged budget.

noncomputable def DescriptiveComplexity.vertexCover_ordered_fo_reduction_edgeSteinerTree : OrderedFOReduction VertexCover EdgeSteinerTree

Vertex Cover ordered-FO-reduces to the edge-weighted Steiner Tree: Karp's original reading of the problem, with the budget enlarged by one unit per edge point – the price of attaching each terminal to the tree.

Equations

• One or more equations did not get rendered due to their size.