[Rule] MaximumLeafSpanningTree to ILP

[isPANN]

Motivation

Direct ILP formulation for MaximumLeafSpanningTree. Companion issue for #897. Enables ILP-based solving.

Source

MaximumLeafSpanningTree

Target

ILP (Integer Linear Programming)

Reference

Standard spanning tree ILP with leaf-count objective.

Reduction Algorithm

Input: Graph G = (V, E) with n = |V|, m = |E|.

1. Create binary variables y_e ∈ {0, 1} for each edge e ∈ E (y_e = 1 means edge e is in the tree).
2. Create binary variables z_v ∈ {0, 1} for each vertex v (z_v = 1 means v is a leaf).
3. Tree cardinality: Σ_e y_e = n - 1.
4. Subtour elimination: for each non-empty proper subset S ⊂ V, Σ_{e ∈ E(S)} y_e ≤ |S| - 1 (or use flow-based formulation).
5. Degree-leaf linking: for each vertex v, let d_v = Σ_{e incident to v} y_e. Then z_v ≤ 1 means v can be a leaf only if d_v = 1. Use: d_v ≥ 1 (spanning), z_v ≥ 1 - (d_v - 1) (if degree 1 then leaf), z_v ≤ 1, d_v - 1 ≤ (n-1)(1 - z_v).
6. Objective: maximize Σ_v z_v.

Solution extraction: Read y_e = 1 to identify the spanning tree.

Size Overhead

Code metric	Formula
num_variables	m + n
num_constraints	2^n + 3*n + 1

Validation Method

Closed-loop test.

Example

Source: P4: v0—v1—v2—v3. Only spanning tree is the path itself → 2 leaves. Max(2).

[isPANN]

Please kindly check the following items (PR #976):

• Paper (PDF): check definition, proof sketch, example figure, and reproducible pred commands
• Implementation (Optional): spot-check the source files changed in this PR for correctness

💬 Join the discussion on Zulip — feel free to ask questions or leave feedback there.