Steiner Tree

Lax799700.Steiner · concepts/Lax799700/Steiner.lean · lax-799700

proven

Loading review…

Natural Language Statement

Theorem

STEINER TREE: given a graph, a set of terminals and a threshold $k$ , is there a connected set of vertices containing every terminal and using at most $k$ non-terminals (SteinerTree, the node-weighted form with unit weights), or a set of at most $k$ arcs of the graph connecting a set of vertices that contains every terminal (EdgeSteinerTree, the edge-weighted form, arcs counted as ordered pairs)? The vocabulary is that of graphs with two unary marks, the terminals and the marked set carrying $k$ in unary representation. Connectivity (ConnectedOn) is not first-order; the membership proofs certify it by a root of the chosen set and a strict partial order in which every other chosen vertex has a chosen neighbor strictly below it. Both forms are NP-hard by ordered first-order reductions from Vertex Cover.

Concept map

7 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

Lean source view on GitHub

Show types on hover

1	import Mathlib.Data.Fintype.EquivFin
2	import Mathlib.Data.Set.Card
3	import Mathlib.SetTheory.Cardinal.Finite
4	import Mathlib.Logic.Equiv.Prod
5	import Mathlib.ModelTheory.Semantics
6	import Mathlib.ModelTheory.Complexity
7	import Mathlib.Tactic.FinCases
8	import Mathlib.ModelTheory.Syntax
9	import Lax904597.Classes
10	import Lax799700.Problems
11
12	/-!
13	---
14	title: Steiner Tree
15	type: theorem
16	---
17	STEINER TREE: given a graph, a set of terminals and a threshold $k$ , is
18	there a connected set of vertices containing every terminal and using at
19	most $k$ non-terminals (SteinerTree, the node-weighted form with unit
20	weights), or a set of at most $k$ arcs of the graph connecting a set of
21	vertices that contains every terminal (EdgeSteinerTree, the edge-weighted
22	form, arcs counted as ordered pairs)? The vocabulary is that of graphs
23	with two unary marks, the terminals and the marked set carrying $k$ in
24	unary representation. Connectivity (ConnectedOn) is not first-order; the
25	membership proofs certify it by a root of the chosen set and a strict
26	partial order in which every other chosen vertex has a chosen neighbor
27	strictly below it. Both forms are NP-hard by ordered first-order
28	reductions from Vertex Cover.
29
30	-/
31
32	namespace Lax799700.Steiner
33
34	open FirstOrder
35
36	open FirstOrder.Language
37
38	/-- The relation symbols of the language. -/
39	inductive steinerGraphRel : ℕ → Type where
40	/-- `adj a b`: there is an edge between `a` and `b`. -/
41	\| adj : steinerGraphRel 2
42	/-- `terminal a`: the vertex `a` must be spanned. -/
43	\| terminal : steinerGraphRel 1
44	/-- `marked a`: the vertex `a` belongs to the marked set carrying the
45	threshold. -/
46	\| marked : steinerGraphRel 1
47	deriving DecidableEq
48
49	/-- The relational language of graphs with terminals: adjacency, a set of
50	terminals to be spanned, and a marked set whose cardinality is the budget of
51	non-terminals. -/
52	def steinerGraph : FirstOrder.Language :=
53	⟨fun _ => Empty, steinerGraphRel⟩
54
55	instance instIsRelationalSteinerGraph : FirstOrder.Language.IsRelational steinerGraph := fun _ =>
56	(inferInstance : IsEmpty Empty)
57
58	/-- `adj a b`: there is an edge between `a` and `b`. -/
59	abbrev stAdj : steinerGraph.Relations 2 :=
60	.adj
61
62	/-- `terminal a`: the vertex `a` must be spanned. -/
63	abbrev stTerminal : steinerGraph.Relations 1 :=
64	.terminal
65
66	/-- `marked a`: the vertex `a` belongs to the marked set carrying the
67	threshold. -/
68	abbrev stMarked : steinerGraph.Relations 1 :=
69	.marked
70
71	open FirstOrder
72
73	open Language Structure
74
75	section Connectivity
76
77	variable {A : Type}
78
79	/-- The edges available inside a chosen set: adjacency in either direction,
80	restricted to the set. -/
81	def Link (Adjp : A → A → Prop) (S : A → Prop) (a b : A) : Prop :=
82	S a ∧ S b ∧ (Adjp a b ∨ Adjp b a)
83
84	/-- A set of vertices is connected if any two of its members are joined by a
85	path inside it. -/
86	def ConnectedOn (Adjp : A → A → Prop) (S : A → Prop) : Prop :=
87	∀ x y, S x → S y → Relation.ReflTransGen (Link Adjp S) x y
88
89	end Connectivity
90
91	section Generic
92
93	variable {A : Type}
94
95	/-- Some connected set contains every terminal and uses at most as many
96	non-terminals as the number encoded by the marked set. -/
97	def SteinerOn (Adjp : A → A → Prop) (Term Kp : A → Prop) : Prop :=
98	∃ S : A → Prop, (∀ x, Term x → S x) ∧ ConnectedOn Adjp S ∧
99	{x \| S x ∧ ¬Term x}.ncard ≤ {x \| Kp x}.ncard
100
101	variable {B : Type}
102
103	/-- Some set of edges of the graph, connecting a set that contains every
104	terminal, is at most as large as the number encoded by the marked set: the
105	edge-weighted Steiner tree with unit weights, Karp's original reading.
106
107	The chosen edges are given as a set of ordered pairs, one per edge, and
108	connectivity reads them symmetrically
109	(`DescriptiveComplexity.ConnectedOn`); a witness listing both orientations of an edge
110	merely pays for it twice, so the yes-instances are unaffected. The threshold
111	compares a count of pairs with a count of elements, which is meaningful
112	because a threshold is just a number – and necessary here, since an edge set
113	can be quadratically larger than the universe. -/
114	def SteinerEdgeOn (Adjp : A → A → Prop) (Term Kp : A → Prop) : Prop :=
115	∃ T : A → A → Prop, ∃ S : A → Prop,
116	(∀ a b, T a b → Adjp a b) ∧ (∀ x, Term x → S x) ∧ ConnectedOn T S ∧
117	{p : A × A \| T p.1 p.2}.ncard ≤ {x \| Kp x}.ncard
118
119	end Generic
120
121	section Problem
122
123	section Shorthands
124
125	variable {A : Type} [steinerGraph.Structure A]
126
127	/-- `adj a b`: there is an edge between `a` and `b`. -/
128	def STAdj {A : Type} [steinerGraph.Structure A] (a0 : A) (a1 : A) : Prop :=
129	FirstOrder.Language.Structure.RelMap stAdj ![a0, a1]
130
131	/-- `terminal a`: the vertex `a` must be spanned. -/
132	def STTerminal {A : Type} [steinerGraph.Structure A] (a0 : A) : Prop :=
133	FirstOrder.Language.Structure.RelMap stTerminal ![a0]
134
135	/-- `marked a`: the vertex `a` belongs to the marked set carrying the
136	threshold. -/
137	def STMarked {A : Type} [steinerGraph.Structure A] (a0 : A) : Prop :=
138	FirstOrder.Language.Structure.RelMap stMarked ![a0]
139
140	end Shorthands
141
142	variable (A : Type) [steinerGraph.Structure A]
143
144	/-- A graph with terminals admits a connected set spanning the terminals and
145	using at most as many non-terminals as its marked set has elements.
146	(Finiteness of the universe is part of the property: cardinality thresholds
147	are only meaningful on finite structures.) -/
148	def HasSmallSteinerTree : Prop :=
149	Finite A ∧ SteinerOn (STAdj (A := A)) STTerminal STMarked
150
151	end Problem
152
153	/-- A graph with terminals admits a set of edges connecting its terminals, of
154	size at most the number encoded by the marked set. -/
155	def HasSmallEdgeSteinerTree (A : Type) [steinerGraph.Structure A] : Prop :=
156	Finite A ∧ SteinerEdgeOn (STAdj (A := A)) STTerminal STMarked
157
158	open Lax904597.Problems Lax904597.Classes Lax799700.Problems
159
160	/-- The property `HasSmallEdgeSteinerTree` is isomorphism-invariant. -/
161	axiom hasSmallEdgeSteinerTree_iso : ∀ {A B : Type} [Lax799700.Steiner.steinerGraph.Structure A] [Lax799700.Steiner.steinerGraph.Structure B],
162	(A ≃[Lax799700.Steiner.steinerGraph] B) → (HasSmallEdgeSteinerTree A ↔ HasSmallEdgeSteinerTree B)
163
164	/-- The problem EdgeSteinerTree: does the structure satisfy `HasSmallEdgeSteinerTree`? -/
165	def EdgeSteinerTree : DecisionProblem Lax799700.Steiner.steinerGraph :=
166	DecisionProblem.ofPred HasSmallEdgeSteinerTree
167
168	/-- The yes-instances of EdgeSteinerTree are exactly the structures satisfying
169	`HasSmallEdgeSteinerTree`. -/
170	axiom edgeSteinerTree_iff : ∀ (A : Type) [Lax799700.Steiner.steinerGraph.Structure A], EdgeSteinerTree A ↔ HasSmallEdgeSteinerTree A
171
172	/-- EdgeSteinerTree is NP-complete. -/
173	axiom edgeSteinerTree_NP_complete : NP.Complete EdgeSteinerTree
174
175	/-- The property `HasSmallSteinerTree` is isomorphism-invariant. -/
176	axiom hasSmallSteinerTree_iso : ∀ {A B : Type} [Lax799700.Steiner.steinerGraph.Structure A] [Lax799700.Steiner.steinerGraph.Structure B],
177	(A ≃[Lax799700.Steiner.steinerGraph] B) → (HasSmallSteinerTree A ↔ HasSmallSteinerTree B)
178
179	/-- The problem SteinerTree: does the structure satisfy `HasSmallSteinerTree`? -/
180	def SteinerTree : DecisionProblem Lax799700.Steiner.steinerGraph :=
181	DecisionProblem.ofPred HasSmallSteinerTree
182
183	/-- The yes-instances of SteinerTree are exactly the structures satisfying
184	`HasSmallSteinerTree`. -/
185	axiom steinerTree_iff : ∀ (A : Type) [Lax799700.Steiner.steinerGraph.Structure A], SteinerTree A ↔ HasSmallSteinerTree A
186
187	/-- SteinerTree is NP-complete. -/
188	axiom steinerTree_NP_complete : NP.Complete SteinerTree
189
190	end Lax799700.Steiner
191

Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof

Builds on

Used by

none

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

Steiner Tree

Flags

Flag this concept

Natural Language Statement

Theorem

1 `edgeSteinerTree_iff` proven

2 `edgeSteinerTree_NP_complete` proven

3 `hasSmallEdgeSteinerTree_iso` proven

4 `hasSmallSteinerTree_iso` proven

5 `steinerTree_iff` proven

6 `steinerTree_NP_complete` proven

Lean source view on GitHub

Discussion

Settings