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

Proved

LinearOptimization.integer_program_formulation_strength

by Shuze Chen · Aug 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

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

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}$