Fix #141: Add MinimumFeedbackVertexSet to ILP reduction (#624)

* Add plan for #141: MinimumFeedbackVertexSet to ILP reduction

* Implement #141: MinimumFeedbackVertexSet to ILP reduction

Add MTZ-style topological ordering reduction from MinimumFeedbackVertexSet
to ILP<i32>. Uses 2n variables (n binary + n integer ordering) and m + 2n
constraints. Includes unit tests, example program, and paper documentation.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

* chore: remove plan file after implementation

* chore: fix formatting after merge

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

* fix: migrate MFVS example to example-db pattern, add canonical specs

Remove old-style example binary and add canonical_rule_example_specs()
to the MFVS-to-ILP rule, matching the current project convention.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

* fix: support ILP<i32> in CLI solve_ilp dispatch

The solve_ilp function only downcasted to ILP<bool>, causing
`pred solve` to fail for problems that reduce to ILP<i32> (e.g.,
MinimumFeedbackVertexSet). Now tries both ILP<bool> and ILP<i32>.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

* Regenerate fixtures and fix formatting after merge with main

- examples.json now includes MFVS-to-ILP canonical example
- create.rs: remove extra blank line (rustfmt)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: GiggleLiu <cacate0129@gmail.com>

Author: 3 people

docs/paper/reductions.typ

@@ -3286,6 +3286,22 @@ The following reductions to Integer Linear Programming are straightforward formu
   _Solution extraction._ $D = {v : x_v = 1}$.
 ]
 
+#reduction-rule("MinimumFeedbackVertexSet", "ILP")[
+  A directed graph is a DAG iff it admits a topological ordering. MTZ-style ordering variables enforce this: for each kept vertex, an integer position variable must increase strictly along every arc. Removed vertices relax the ordering constraints via big-$M$ terms.
+][
+  _Construction._ Given directed graph $G = (V, A)$ with $n = |V|$, $m = |A|$, and weights $w_v$:
+
+  _Variables:_ Binary $x_v in {0, 1}$ for each $v in V$: $x_v = 1$ iff $v$ is removed. Integer $o_v in {0, dots, n-1}$ for each $v in V$: topological order position. Total: $2n$ variables.
+
+  _Constraints:_ (1) For each arc $(u -> v) in A$: $o_v - o_u >= 1 - n(x_u + x_v)$. When both endpoints are kept ($x_u = x_v = 0$), this forces $o_v > o_u$ (strict topological order). When either is removed, the constraint relaxes to $o_v - o_u >= 1 - n$ (trivially satisfied). (2) Binary bounds: $x_v <= 1$. (3) Order bounds: $o_v <= n - 1$. Total: $m + 2n$ constraints.
+
+  _Objective:_ Minimize $sum_v w_v x_v$.
+
+  _Correctness._ ($arrow.r.double$) If $S$ is a feedback vertex set, then $G[V backslash S]$ is a DAG with a topological ordering. Set $x_v = 1$ for $v in S$, $o_v$ to the topological position for kept vertices, and $o_v = 0$ for removed vertices. All constraints are satisfied. ($arrow.l.double$) If the ILP is feasible with all arc constraints satisfied, no directed cycle can exist among kept vertices: a cycle $v_1 -> dots -> v_k -> v_1$ would require $o_(v_1) < o_(v_2) < dots < o_(v_k) < o_(v_1)$, a contradiction.
+
+  _Solution extraction._ $S = {v : x_v = 1}$.
+]
+
 #reduction-rule("MaximumClique", "ILP")[
   A clique requires every pair of selected vertices to be adjacent; equivalently, no two selected vertices may share a _non_-edge. This is the independent set formulation on the complement graph $overline(G)$.
 ][

problemreductions-cli/src/commands/create.rs

@@ -1721,7 +1721,6 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> {
     emit_problem_output(&output, out)
 }
 
-
 /// Reject non-unit weights when the resolved variant uses `weight=One`.
 fn reject_nonunit_weights_for_one_variant(
     canonical: &str,

problemreductions-cli/src/dispatch.rs

@@ -165,17 +165,27 @@ pub struct SolveResult {
     pub evaluation: String,
 }
 
-/// Solve an ILP problem directly. The input must be an `ILP` instance.
+/// Solve an ILP problem directly. The input must be an `ILP<bool>` or `ILP<i32>` instance.
 fn solve_ilp(any: &dyn Any) -> Result<SolveResult> {
-    let problem = any
-        .downcast_ref::<ILP>()
-        .ok_or_else(|| anyhow::anyhow!("Internal error: expected ILP problem instance"))?;
-    let solver = ILPSolver::new();
-    let config = solver
-        .solve(problem)
-        .ok_or_else(|| anyhow::anyhow!("ILP solver found no feasible solution"))?;
-    let evaluation = format!("{:?}", problem.evaluate(&config));
-    Ok(SolveResult { config, evaluation })
+    if let Some(problem) = any.downcast_ref::<ILP<bool>>() {
+        let solver = ILPSolver::new();
+        let config = solver
+            .solve(problem)
+            .ok_or_else(|| anyhow::anyhow!("ILP solver found no feasible solution"))?;
+        let evaluation = format!("{:?}", problem.evaluate(&config));
+        return Ok(SolveResult { config, evaluation });
+    }
+    if let Some(problem) = any.downcast_ref::<ILP<i32>>() {
+        let solver = ILPSolver::new();
+        let config = solver
+            .solve(problem)
+            .ok_or_else(|| anyhow::anyhow!("ILP solver found no feasible solution"))?;
+        let evaluation = format!("{:?}", problem.evaluate(&config));
+        return Ok(SolveResult { config, evaluation });
+    }
+    Err(anyhow::anyhow!(
+        "Internal error: expected ILP<bool> or ILP<i32> problem instance"
+    ))
 }
 
 #[cfg(test)]

src/example_db/fixtures/examples.json

@@ -0,0 +1,123 @@
+//! Reduction from MinimumFeedbackVertexSet to ILP (Integer Linear Programming).
+//!
+//! Uses MTZ-style topological ordering constraints:
+//! - Variables: n binary x_i (vertex removal) + n integer o_i (topological order) = 2n total
+//! - Constraints: For each arc (u->v): o_v - o_u >= 1 - n*(x_u + x_v)
+//!   Plus binary bounds (x_i <= 1) and order bounds (o_i <= n-1)
+//! - Objective: Minimize the weighted sum of removed vertices
+
+use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
+use crate::models::graph::MinimumFeedbackVertexSet;
+use crate::reduction;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+
+/// Result of reducing MinimumFeedbackVertexSet to ILP.
+///
+/// The ILP uses integer variables (`ILP<i32>`) because it needs both
+/// binary selection variables (x_i) and integer ordering variables (o_i).
+///
+/// Variable layout:
+/// - `x_i` at index `i` for `i in 0..n`: binary (0 or 1), vertex removal indicator
+/// - `o_i` at index `n + i` for `i in 0..n`: integer in {0, ..., n-1}, topological order
+#[derive(Debug, Clone)]
+pub struct ReductionMFVSToILP {
+    target: ILP<i32>,
+    /// Number of vertices in the source graph (needed for solution extraction).
+    num_vertices: usize,
+}
+
+impl ReductionResult for ReductionMFVSToILP {
+    type Source = MinimumFeedbackVertexSet<i32>;
+    type Target = ILP<i32>;
+
+    fn target_problem(&self) -> &ILP<i32> {
+        &self.target
+    }
+
+    /// Extract solution from ILP back to MinimumFeedbackVertexSet.
+    ///
+    /// The first n variables of the ILP solution are the binary x_i values,
+    /// which directly correspond to the FVS configuration (1 = removed).
+    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
+        target_solution[..self.num_vertices].to_vec()
+    }
+}
+
+#[reduction(
+    overhead = {
+        num_vars = "2 * num_vertices",
+        num_constraints = "num_arcs + 2 * num_vertices",
+    }
+)]
+impl ReduceTo<ILP<i32>> for MinimumFeedbackVertexSet<i32> {
+    type Result = ReductionMFVSToILP;
+
+    fn reduce_to(&self) -> Self::Result {
+        let n = self.graph().num_vertices();
+        let arcs = self.graph().arcs();
+        let num_vars = 2 * n;
+
+        // Variable indices:
+        // x_i = i         (binary: vertex i removed?)
+        // o_i = n + i     (integer: topological order of vertex i)
+
+        let mut constraints = Vec::new();
+
+        // Binary bounds: x_i <= 1 for i in 0..n
+        for i in 0..n {
+            constraints.push(LinearConstraint::le(vec![(i, 1.0)], 1.0));
+        }
+
+        // Order bounds: o_i <= n - 1 for i in 0..n
+        for i in 0..n {
+            constraints.push(LinearConstraint::le(vec![(n + i, 1.0)], (n - 1) as f64));
+        }
+
+        // Arc constraints: for each arc (u -> v):
+        //   o_v - o_u >= 1 - n * (x_u + x_v)
+        // Rearranged: o_v - o_u + n*x_u + n*x_v >= 1
+        let n_f64 = n as f64;
+        for &(u, v) in &arcs {
+            let terms = vec![
+                (n + v, 1.0),  // o_v
+                (n + u, -1.0), // -o_u
+                (u, n_f64),    // n * x_u
+                (v, n_f64),    // n * x_v
+            ];
+            constraints.push(LinearConstraint::ge(terms, 1.0));
+        }
+
+        // Objective: minimize sum w_i * x_i
+        let objective: Vec<(usize, f64)> = self
+            .weights()
+            .iter()
+            .enumerate()
+            .map(|(i, &w)| (i, w as f64))
+            .collect();
+
+        let target = ILP::new(num_vars, constraints, objective, ObjectiveSense::Minimize);
+
+        ReductionMFVSToILP {
+            target,
+            num_vertices: n,
+        }
+    }
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
+    use crate::topology::DirectedGraph;
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "minimumfeedbackvertexset_to_ilp",
+        build: || {
+            // Simple cycle: 0 -> 1 -> 2 -> 0 (FVS = 1 vertex)
+            let graph = DirectedGraph::new(3, vec![(0, 1), (1, 2), (2, 0)]);
+            let source = MinimumFeedbackVertexSet::new(graph, vec![1i32; 3]);
+            crate::example_db::specs::direct_ilp_example::<_, i32, _>(source, |_, _| true)
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/minimumfeedbackvertexset_ilp.rs"]
+mod tests;

src/rules/minimumfeedbackvertexset_ilp.rs

@@ -64,6 +64,8 @@ pub(crate) mod maximumsetpacking_ilp;
 #[cfg(feature = "ilp-solver")]
 pub(crate) mod minimumdominatingset_ilp;
 #[cfg(feature = "ilp-solver")]
+pub(crate) mod minimumfeedbackvertexset_ilp;
+#[cfg(feature = "ilp-solver")]
 pub(crate) mod minimumsetcovering_ilp;
 #[cfg(feature = "ilp-solver")]
 pub(crate) mod qubo_ilp;
@@ -112,6 +114,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
         specs.extend(maximummatching_ilp::canonical_rule_example_specs());
         specs.extend(maximumsetpacking_ilp::canonical_rule_example_specs());
         specs.extend(minimumdominatingset_ilp::canonical_rule_example_specs());
+        specs.extend(minimumfeedbackvertexset_ilp::canonical_rule_example_specs());
         specs.extend(minimumsetcovering_ilp::canonical_rule_example_specs());
         specs.extend(qubo_ilp::canonical_rule_example_specs());
         specs.extend(travelingsalesman_ilp::canonical_rule_example_specs());