Relative strength of spanning tree formulations: $P_{sub} \subseteq P_{cut}$

Proved

LinearOptimization.integer_program_formulation_strength

by Shuze Chen · Aug 9, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convex-hullformulation-strengthinteger-programmingpolyhedraspanning-tree

(Theorem 10.1 — Bertsimas & Tsitsiklis, p. 467, Section 10.3.) Let $G = (\mathcal{N}, \mathcal{E})$ be an undirected graph with $|\mathcal{N}| = n$ . For $S \subseteq \mathcal{N}$ let $E(S) = \{\{i,j\} \in \mathcal{E} \mid i, j \in S\}$ and let $\delta(S) = \{\{i,j\} \in \mathcal{E} \mid i \in S,\ j \notin S\}$ .

Let $P_{sub}$ be the feasible set of the linear programming relaxation of the subtour elimination formulation of the minimum spanning tree problem ( $\sum_{e \in \mathcal{E}} x_e = n - 1$ ; $\sum_{e \in E(S)} x_e \le |S| - 1$ for all $S \subset \mathcal{N}$ , $S \ne \emptyset, \mathcal{N}$ ; $0 \le x_e \le 1$ ), and let $P_{cut}$ be the feasible set of the linear programming relaxation of the cutset formulation ( $\sum_{e \in \mathcal{E}} x_e = n - 1$ ; $\sum_{e \in \delta(S)} x_e \ge 1$ for all $S \subset \mathcal{N}$ , $S \ne \emptyset, \mathcal{N}$ ; $0 \le x_e \le 1$ ).

The following properties hold:

(a) We have $P_{sub} \subseteq P_{cut}$ , and there exist examples for which the inclusion is strict.
(b) The polyhedron $P_{cut}$ can have fractional extreme points.

Preamble

import Mathlib.Analysis.Convex.Extreme
import Definitions.Def_Polyhedron
import Definitions.Def_LinearOptimization_MstRelaxations


open Matrix

/-- **Bertsimas & Tsitsiklis, Theorem 10.1 (p. 467).** Formulation strength for the minimum
spanning tree problem: (a) `P_sub ⊆ P_cut` for every finite undirected
graph, and the inclusion can be strict; (b) `P_cut` can have fractional
extreme points. -/

Formal statement

theorem LinearOptimization.integer_program_formulation_strength :
    (∀ (n k : ℕ) (ends : Fin k → Fin n × Fin n),
      mstSubtourRelaxation ends ⊆ mstCutsetRelaxation ends) ∧
    (∃ (n k : ℕ) (ends : Fin k → Fin n × Fin n),
      ¬mstCutsetRelaxation ends ⊆ mstSubtourRelaxation ends) ∧
    (∃ (n k : ℕ) (ends : Fin k → Fin n × Fin n) (x : Fin k → ℝ),
      x ∈ Set.extremePoints ℝ (mstCutsetRelaxation ends) ∧
      ∃ e, ¬∃ z : ℤ, x e = (z : ℝ)) := by
  sorry

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 10.1, p. 467

Read-back

What the Lean code literally says, in plain math · claude-fable-5

A closed statement (no free parameters) with three conjuncts, about the two MST relaxations parameterized by $n$ vertices and $k$ edges with endpoint map $\mathrm{ends}$ . Writing SUB for the subtour relaxation ( $\sum_e x_e=n-1$ ; for every nonempty proper vertex set $S$ , $\sum_{e:\ \text{both endpoints in }S}x_e\le|S|-1$ ; $0\le x_e\le1$ ) and CUT for the cutset relaxation ( $\sum_e x_e=n-1$ ; for every nonempty proper $S$ , $\sum_{e:\ \text{exactly one endpoint in }S}x_e\ge1$ ; $0\le x_e\le1$ ): (i) for every $n$ , $k$ , and $\mathrm{ends}$ , $\mathrm{SUB}\subseteq\mathrm{CUT}$ ; (ii) there exist $n$ , $k$ , $\mathrm{ends}$ with $\mathrm{CUT}\not\subseteq\mathrm{SUB}$ (the reverse inclusion fails for some instance); (iii) there exist $n$ , $k$ , $\mathrm{ends}$ and a point $x$ that is an extreme point of CUT (in the Mathlib sense: $x\in\mathrm{CUT}$ , and whenever $x$ lies in the open segment between two points of CUT both endpoints equal $x$ ) having some coordinate $x_e$ that is not equal to any integer. The instances in (ii) and (iii) are existentially quantified and need not coincide.

Human review

Endorsed by Community (Bot) · Aug 9, 2026
Endorsed by Shuze Chen · Aug 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Relative strength of spanning tree formulations: Psub⊆PcutP_{sub} \subseteq P_{cut}Psub​⊆Pcut​

Relative strength of spanning tree formulations: $P_{sub} \subseteq P_{cut}$