[Rule] MinimumFeedbackVertexSet to ILP

[fliingelephant]

Source: MinimumFeedbackVertexSet (#140)
Target: ILP
Motivation: Enables exact solving of directed FVS via ILP solvers. The topological-ordering formulation is compact (2n variables, m constraints).
Reference:

• Topological ordering constraints adapted from Miller, Tucker & Zemlin (1960), "Integer Programming Formulation of Traveling Salesman Problems" — same technique (ordering variables to eliminate directed cycles)
• Even, Naor & Schieber (1998), "Approximating Minimum Feedback Sets and Multicuts in Directed Graphs"

Reduction Algorithm

Notation:

• Source: MinimumFeedbackVertexSet instance with directed graph G = (V, A), n = |V|, m = |A|, weights w_i
• Target: ILP instance with 2n variables and m constraints

Key idea: A directed graph is a DAG if and only if it admits a topological ordering. Encode this with integer ordering variables and linear constraints.

Variable mapping:

Variable	Count	Domain	Meaning
$x_i$	n	{0, 1}	vertex i is removed
$o_i$	n	{0, ..., n−1}	topological order of vertex i

Constraint transformation:

For each arc $(u \to v) \in A$: if both endpoints are kept, the ordering must be consistent:

$$o_v - o_u \geq 1 - n \cdot (x_u + x_v)$$

• When $x_u = x_v = 0$ (both kept): $o_v \geq o_u + 1$ (enforces strict topological order)
• When either is removed: $o_v - o_u \geq 1 - n$ (always satisfied since $0 \leq o_i \leq n-1$)

Objective: minimize $\sum_i w_i \cdot x_i$

Correctness:

• ($\Rightarrow$) If G[V\S] is a DAG, it has a topological ordering. Set $o_i$ to the topological position. All arc constraints satisfied.
• ($\Leftarrow$) If the ILP is feasible with all arcs between kept vertices satisfying $o_v > o_u$, no directed cycle can exist (a cycle $v_1 \to v_2 \to \cdots \to v_k \to v_1$ would require $o_{v_1} < o_{v_2} < \cdots < o_{v_k} < o_{v_1}$, a contradiction).

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_vars	$2n$
num_constraints	$m$

Validation Method

• Cross-check with brute-force solver on small instances (n ≤ 10)
• Verify on known special cases: directed cycle $C_n$ has FVS = 1, complete directed graph (both arcs per pair) has FVS = n − 1
• Compare against example instance: FVS = 3

Example

Source: Cycle of triangles (n = 9, m = 15) from #140

Vertices: {0, 1, 2, 3, 4, 5, 6, 7, 8}
Arcs: {0→1, 1→2, 2→0, 3→4, 4→5, 5→3, 6→7, 7→8, 8→6,
       1→3, 4→6, 7→0, 2→5, 5→8, 8→2}
Unit weights: w_i = 1 for all i

Target ILP:

Variables: 9 binary x_i, 9 integer o_i ∈ {0,...,8}  (18 total)
Constraints: 15 (one per arc)
Objective: minimize Σ x_i

Solution: x = (1, 0, 0, 1, 0, 0, 0, 0, 1) → S = {0, 3, 8}, objective = 3.

Topological ordering of remaining DAG on {1, 2, 4, 5, 6, 7}:

o_1 = 0, o_4 = 1, o_2 = 2, o_6 = 3, o_5 = 4, o_7 = 5

Verification of arc constraints (remaining arcs only):

1→2: o_2 − o_1 = 2 ≥ 1  ✓
4→5: o_5 − o_4 = 3 ≥ 1  ✓
6→7: o_7 − o_6 = 2 ≥ 1  ✓
4→6: o_6 − o_4 = 2 ≥ 1  ✓
2→5: o_5 − o_2 = 2 ≥ 1  ✓

All 10 removed-endpoint arc constraints: relaxed to $o_v − o_u \geq 1 − 9$ (trivially satisfied) ✓

Overhead: n = 9, m = 15 → num_vars = 18, num_constraints = 15.

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Source problem not yet in codebase; novel reduction
Non-trivial	✅ Pass	Constructs ordering variables and Big-M linear constraints
Correctness	✅ Pass	Both references verified; ILP formulation and example are correct
Well-written	✅ Pass	All sections complete, symbols consistent, example fully worked

Overall: 4 passed, 0 failed, 0 warnings

---

Usefulness

MinimumFeedbackVertexSet is not yet implemented (proposed in #140), so no reduction path to ILP exists. This is a novel reduction that would enable exact FVS solving via ILP solvers. The compact formulation (2n variables, m constraints) is a practical advantage.

Non-trivial

The reduction involves genuine structural transformation: it introduces n integer ordering variables (o_i) alongside n binary selection variables (x_i), and constructs Big-M linear constraints that enforce topological ordering on the subgraph induced by kept vertices. This is a non-trivial adaptation of the Miller-Tucker-Zemlin (MTZ) technique from TSP to the feedback vertex set setting.

Correctness

Reference 1 — Miller, Tucker & Zemlin (1960): Verified. "Integer Programming Formulation of Traveling Salesman Problems," Journal of the ACM, Vol. 7(4), pp. 326-329. DOI 10.1145/321043.321046. The MTZ formulation uses ordering variables to eliminate subtours; the issue correctly adapts this technique to eliminate directed cycles for FVS.

Reference 2 — Even, Naor & Schieber (1998): Verified. "Approximating Minimum Feedback Sets and Multicuts in Directed Graphs," Algorithmica, Vol. 20, pp. 151-174. Note: this paper addresses approximation algorithms for FVS, not ILP formulations specifically. It serves as a valid general FVS reference but does not contain the proposed ILP formulation.

Formulation correctness: The constraint o_v - o_u >= 1 - n(x_u + x_v) correctly enforces:

• When both endpoints are kept (x_u = x_v = 0): strict topological order o_v > o_u
• When either is removed: constraint is trivially satisfied (RHS <= 1 - n)

This makes directed cycles among kept vertices infeasible (a cycle would require o_v1 < o_v2 < ... < o_vk < o_v1, contradiction).

Example verified: Removing S = {0, 3, 8} from the 9-vertex "cycle of triangles" graph leaves a DAG on {1, 2, 4, 5, 6, 7} with valid topological ordering o_1=0, o_4=1, o_2=2, o_6=3, o_5=4, o_7=5. Objective = 3 is optimal since the three disjoint directed triangles each require at least one vertex removed.

Well-written

All template sections are present and substantive:

• Source/Target: Clearly identified with cross-reference to [Model] MinimumFeedbackVertexSet #140
• Motivation: Concrete ("enables exact solving via ILP solvers") with size characterization
• References: Two relevant citations with links
• Reduction Algorithm: Complete step-by-step with variable table, constraint derivation, and correctness argument
• Size Overhead: Uses correct ILP getter names (num_vars, num_constraints) matching pred show ILP
• Validation Method: Brute-force cross-check and known special cases
• Example: Non-trivial (9 vertices, 15 arcs), fully worked with step-by-step verification of all arc constraints

Recommendations

• For additional rigor, consider citing Baharev et al. (2022), "Reduction Rules and ILP Are All You Need: Minimal Directed Feedback Vertex Set" which discusses practical ILP solving of directed FVS (though they use a cycle-based formulation with lazy constraint generation rather than the compact MTZ-style formulation proposed here).

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Source problem (MinimumFeedbackVertexSet) not yet in codebase; novel reduction
Non-trivial	✅ Pass	MTZ-style topological ordering gadget with big-M relaxation
Correctness	✅ Pass	Both references verified; formulation is mathematically sound
Well-written	✅ Pass	Complete, detailed, and implementable

Overall: 4 passed, 0 failed, 0 warnings

---

Usefulness

MinimumFeedbackVertexSet is not yet implemented (planned in #140), so no existing path to ILP exists. This reduction enables exact solving of directed FVS instances via ILP solvers, which is a natural and valuable connection. The compact formulation (2n variables, m constraints) is efficient — no exponential blowup in cycle enumeration. Pass.

Non-trivial

The reduction uses an MTZ-style topological ordering construction adapted from the Traveling Salesman Problem. It introduces n integer ordering variables o_i with big-M constraints that enforce strict topological order among kept vertices while relaxing constraints for removed vertices. This is a genuine structural transformation involving auxiliary integer variables and non-trivial constraint design — not a variable substitution or subtype coercion. Pass.

Correctness

Reference 1: Miller, Tucker & Zemlin (1960) — "Integer Programming Formulation of Traveling Salesman Problems," JACM 7(4):326–329. DOI: 10.1145/321043.321046. Verified. The paper introduces the MTZ subtour elimination constraints using ordering variables, which is exactly the technique adapted here for cycle elimination in FVS. The adaptation is valid: a directed graph with no cycles is a DAG, which admits a topological ordering — the same structural property that MTZ constraints enforce.

Reference 2: Even, Naor & Schieber (1998) — "Approximating Minimum Feedback Sets and Multicuts in Directed Graphs," Algorithmica 20:151–174. Springer link. Verified. The paper studies approximation algorithms for weighted FVS/FES in directed graphs, confirming the problem definition and its significance.

Formulation correctness:

• When both endpoints kept (x_u = x_v = 0): constraint becomes o_v - o_u >= 1, enforcing strict topological order. ✓
• When either removed (x_u + x_v >= 1): constraint relaxes to o_v - o_u >= 1 - n, which is trivially satisfied since 0 <= o_i <= n-1. ✓
• A cycle among kept vertices would require o_{v1} < o_{v2} < ... < o_{vk} < o_{v1}, a contradiction. ✓

Pass.

Well-written

Information completeness: All required sections present and substantive — Source, Target, Motivation, References, Reduction Algorithm, Size Overhead, Validation Method, and Example. ✓

Algorithm completeness: The reduction algorithm provides a complete, step-by-step procedure with clearly defined notation (n, m, G, V, A, w_i), variable mapping table, constraint transformation formula, objective, and both directions of the correctness proof. Fully implementable. ✓

Symbol consistency: All symbols defined before use. The notation section defines n = |V|, m = |A|. The overhead table uses the same symbols and maps to correct ILP getter names (num_vars, num_constraints), which match the ILP schema's size_fields. ✓

Example quality: The example uses 9 vertices and 15 arcs (non-trivial "cycle of triangles" graph from #140). It shows the full construction (18 variables, 15 constraints), provides a concrete optimal solution S = {0, 3, 8} with objective 3, gives explicit topological ordering of the remaining DAG, and verifies all 15 arc constraints individually. Brute-force verifiable. ✓

Pass.