diff --git a/src/example_db/mod.rs b/src/example_db/mod.rs
index adddc3df4..6ed577a95 100644
--- a/src/example_db/mod.rs
+++ b/src/example_db/mod.rs
@@ -53,8 +53,8 @@ fn validate_model_uniqueness(models: &[ModelExample]) -> Result<()> {
 
 /// Build the full example database from specs.
 ///
-/// Fast — specs store concrete instances and pre-computed solutions,
-/// no solver is called.
+/// ILP rule examples call the ILP solver at build time to compute solutions
+/// dynamically (feature-gated behind `ilp-solver`).
 pub fn build_example_db() -> Result<ExampleDb> {
     let model_db = build_model_db()?;
     let rule_db = build_rule_db()?;
diff --git a/src/example_db/specs.rs b/src/example_db/specs.rs
index d5cb82a85..d6facb3ca 100644
--- a/src/example_db/specs.rs
+++ b/src/example_db/specs.rs
@@ -62,3 +62,32 @@ where
     let target = reduction.target_problem();
     assemble_rule_example(&source, target, vec![solution])
 }
+
+/// Reduce the source to an ILP, solve it, and assemble the rule example.
+///
+/// This is the standard pattern for canonical ILP rule examples: reduce once,
+/// solve the ILP, extract the source config, and build the example — avoiding
+/// the double `reduce_to()` that would occur with `rule_example_with_witness`.
+#[cfg(feature = "ilp-solver")]
+pub fn rule_example_via_ilp<S, V>(source: S) -> RuleExample
+where
+    S: Problem + Serialize + ReduceTo<crate::models::algebraic::ILP<V>>,
+    V: crate::models::algebraic::VariableDomain,
+    <S as ReduceTo<crate::models::algebraic::ILP<V>>>::Result:
+        ReductionResult<Source = S, Target = crate::models::algebraic::ILP<V>>,
+{
+    use crate::export::SolutionPair;
+    let reduction = source.reduce_to();
+    let ilp_solution = crate::solvers::ILPSolver::new()
+        .solve(reduction.target_problem())
+        .expect("canonical example must be ILP-solvable");
+    let source_config = reduction.extract_solution(&ilp_solution);
+    assemble_rule_example(
+        &source,
+        reduction.target_problem(),
+        vec![SolutionPair {
+            source_config,
+            target_config: ilp_solution,
+        }],
+    )
+}
diff --git a/src/rules/bmf_ilp.rs b/src/rules/bmf_ilp.rs
index 3f36616d3..aca0223d3 100644
--- a/src/rules/bmf_ilp.rs
+++ b/src/rules/bmf_ilp.rs
@@ -114,34 +114,12 @@ impl ReduceTo<ILP<bool>> for BMF {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "bmf_to_ilp",
         build: || {
             // 2x2 identity matrix, rank 2
             let source = BMF::new(vec![vec![true, false], vec![false, true]], 2);
-            // B = [[1,0],[0,1]], C = [[1,0],[0,1]]
-            // b: [1,0,0,1], c: [1,0,0,1]
-            let source_config = vec![1, 0, 0, 1, 1, 0, 0, 1];
-            let reduction: ReductionBMFToILP = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            // Build target config by encoding:
-            // p_{0,0,0}=1, p_{0,0,1}=0, p_{0,1,0}=0, p_{0,1,1}=0
-            // p_{1,0,0}=0, p_{1,0,1}=0, p_{1,1,0}=0, p_{1,1,1}=1
-            // w: [1,0,0,1], e: [0,0,0,0]
-            let target_config = vec![
-                1, 0, 0, 1, // B
-                1, 0, 0, 1, // C
-                1, 0, 0, 0, 0, 0, 0, 1, // P
-                1, 0, 0, 1, // W
-                0, 0, 0, 0, // E
-            ];
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/bottlenecktravelingsalesman_ilp.rs b/src/rules/bottlenecktravelingsalesman_ilp.rs
index c86bf15dc..a67dda8e2 100644
--- a/src/rules/bottlenecktravelingsalesman_ilp.rs
+++ b/src/rules/bottlenecktravelingsalesman_ilp.rs
@@ -174,7 +174,6 @@ impl ReduceTo<ILP<i32>> for BottleneckTravelingSalesman {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "bottlenecktravelingsalesman_to_ilp",
         build: || {
@@ -183,18 +182,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 crate::topology::SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3), (3, 0)]),
                 vec![1, 2, 3, 4],
             );
-            let reduction = ReduceTo::<ILP<i32>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/capacityassignment_ilp.rs b/src/rules/capacityassignment_ilp.rs
index 25fffa479..798646c85 100644
--- a/src/rules/capacityassignment_ilp.rs
+++ b/src/rules/capacityassignment_ilp.rs
@@ -101,8 +101,6 @@ impl ReduceTo<ILP<bool>> for CapacityAssignment {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "capacityassignment_to_ilp",
         build: || {
@@ -121,15 +119,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![vec![8, 4], vec![7, 3]],
                 12,
             );
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    // link 0 → cap 1, link 1 → cap 0
-                    source_config: vec![1, 0],
-                    // x_{0,0}=0, x_{0,1}=1, x_{1,0}=1, x_{1,1}=0
-                    target_config: vec![0, 1, 1, 0],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/consecutiveblockminimization_ilp.rs b/src/rules/consecutiveblockminimization_ilp.rs
index dc7e3bcb2..f63ff9770 100644
--- a/src/rules/consecutiveblockminimization_ilp.rs
+++ b/src/rules/consecutiveblockminimization_ilp.rs
@@ -113,7 +113,6 @@ impl ReduceTo<ILP<bool>> for ConsecutiveBlockMinimization {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "consecutiveblockminimization_to_ilp",
         build: || {
@@ -122,62 +121,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![vec![true, false, true], vec![false, true, true]],
                 2,
             );
-            // Permutation [2,0,1] => columns reordered as [2,0,1]
-            // Row 0: A[0,2]=1, A[0,0]=1, A[0,1]=0 => [1,1,0] => 1 block
-            // Row 1: A[1,2]=1, A[1,0]=0, A[1,1]=1 => [1,0,1] => 2 blocks
-            // Total = 3 > 2, try [0,2,1]:
-            // Row 0: A[0,0]=1, A[0,2]=1, A[0,1]=0 => [1,1,0] => 1 block
-            // Row 1: A[1,0]=0, A[1,2]=1, A[1,1]=1 => [0,1,1] => 1 block
-            // Total = 2 <= 2. Good.
-            let source_config = vec![0, 2, 1];
-            let reduction: ReductionCBMToILP = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            // Encode x_{c,p}: column c at position p
-            // c=0 at p=0: x_{0*3+0}=1, c=2 at p=1: x_{2*3+1}=1, c=1 at p=2: x_{1*3+2}=1
-            let n = 3;
-            let mut target_config = vec![0; reduction.target.num_vars];
-            // x_{0,0} = 1
-            target_config[0 * n + 0] = 1;
-            // x_{2,1} = 1
-            target_config[2 * n + 1] = 1;
-            // x_{1,2} = 1
-            target_config[1 * n + 2] = 1;
-            // a values
-            let a_offset = n * n;
-            let m = 2;
-            let matrix = vec![vec![true, false, true], vec![false, true, true]];
-            let perm = [0, 2, 1];
-            for r in 0..m {
-                for p in 0..n {
-                    if matrix[r][perm[p]] {
-                        target_config[a_offset + r * n + p] = 1;
-                    }
-                }
-            }
-            // b values
-            let b_offset = n * n + m * n;
-            for r in 0..m {
-                for p in 0..n {
-                    let a_cur = if matrix[r][perm[p]] { 1 } else { 0 };
-                    let a_prev = if p > 0 && matrix[r][perm[p - 1]] {
-                        1
-                    } else {
-                        0
-                    };
-                    if p == 0 {
-                        target_config[b_offset + r * n + p] = a_cur;
-                    } else if a_cur > a_prev {
-                        target_config[b_offset + r * n + p] = 1;
-                    }
-                }
-            }
-
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/consistencyofdatabasefrequencytables_ilp.rs b/src/rules/consistencyofdatabasefrequencytables_ilp.rs
index 9461ac9f5..a900f93de 100644
--- a/src/rules/consistencyofdatabasefrequencytables_ilp.rs
+++ b/src/rules/consistencyofdatabasefrequencytables_ilp.rs
@@ -55,7 +55,7 @@ impl ReductionCDFTToILP {
     }
 
     /// Encode a satisfying source assignment as a concrete ILP variable vector.
-    #[cfg_attr(not(any(test, feature = "example-db")), allow(dead_code))]
+    #[cfg_attr(not(test), allow(dead_code))]
     pub(crate) fn encode_source_solution(&self, source_solution: &[usize]) -> Vec<usize> {
         let mut target_solution = vec![0usize; self.target.num_vars];
         let num_attributes = self.source.num_attributes();
@@ -204,7 +204,6 @@ impl ReduceTo<ILP<bool>> for ConsistencyOfDatabaseFrequencyTables {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     use crate::models::misc::{FrequencyTable, KnownValue};
 
     vec![crate::example_db::specs::RuleExampleSpec {
@@ -223,16 +222,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                     KnownValue::new(1, 2, 1),
                 ],
             );
-            let source_config = vec![0, 0, 0, 0, 1, 1, 0, 2, 1, 1, 0, 1, 1, 1, 1, 1, 2, 0];
-            let reduction = source.clone().reduce_to();
-            let target_config = reduction.encode_source_solution(&source_config);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/directedtwocommodityintegralflow_ilp.rs b/src/rules/directedtwocommodityintegralflow_ilp.rs
index 583e1cd5d..f16c304cd 100644
--- a/src/rules/directedtwocommodityintegralflow_ilp.rs
+++ b/src/rules/directedtwocommodityintegralflow_ilp.rs
@@ -147,7 +147,6 @@ impl ReduceTo<ILP<i32>> for DirectedTwoCommodityIntegralFlow {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     use crate::topology::DirectedGraph;
 
     vec![crate::example_db::specs::RuleExampleSpec {
@@ -178,16 +177,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 1,
                 1,
             );
-            // first 8 = f1, next 8 = f2
-            // f1: arc(0,2)=1, arc(2,4)=1, rest=0 → [1,0,0,0,1,0,0,0]
-            // f2: arc(1,3)=1, arc(3,5)=1, rest=0 → [0,0,0,1,0,0,0,1]
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1],
-                    target_config: vec![1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/disjointconnectingpaths_ilp.rs b/src/rules/disjointconnectingpaths_ilp.rs
index 149856028..1c4b7f5df 100644
--- a/src/rules/disjointconnectingpaths_ilp.rs
+++ b/src/rules/disjointconnectingpaths_ilp.rs
@@ -170,9 +170,6 @@ impl ReduceTo<ILP<bool>> for DisjointConnectingPaths<SimpleGraph> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-    use crate::rules::ReduceTo as _;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "disjointconnectingpaths_to_ilp",
         build: || {
@@ -181,18 +178,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 SimpleGraph::new(6, vec![(0, 1), (1, 2), (3, 4), (4, 5)]),
                 vec![(0, 2), (3, 5)],
             );
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/factoring_ilp.rs b/src/rules/factoring_ilp.rs
index c66fc3f51..a3bffb0e9 100644
--- a/src/rules/factoring_ilp.rs
+++ b/src/rules/factoring_ilp.rs
@@ -223,20 +223,11 @@ impl ReduceTo<ILP<i32>> for Factoring {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "factoring_to_ilp",
         build: || {
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                Factoring::new(3, 3, 35),
-                SolutionPair {
-                    source_config: vec![1, 0, 1, 1, 1, 1],
-                    target_config: vec![
-                        1, 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 0, 0, 1, 1, 1, 0,
-                    ],
-                },
-            )
+            let source = Factoring::new(3, 3, 35);
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/flowshopscheduling_ilp.rs b/src/rules/flowshopscheduling_ilp.rs
index 32fb1a06d..7f15251e2 100644
--- a/src/rules/flowshopscheduling_ilp.rs
+++ b/src/rules/flowshopscheduling_ilp.rs
@@ -207,25 +207,12 @@ impl ReduceTo<ILP<i32>> for FlowShopScheduling {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "flowshopscheduling_to_ilp",
         build: || {
             // 2 machines, 3 jobs, deadline 10
             let source = FlowShopScheduling::new(2, vec![vec![2, 3], vec![3, 2], vec![1, 4]], 10);
-            let reduction = ReduceTo::<ILP<i32>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/hamiltonianpath_ilp.rs b/src/rules/hamiltonianpath_ilp.rs
index 422323d62..d60f1291a 100644
--- a/src/rules/hamiltonianpath_ilp.rs
+++ b/src/rules/hamiltonianpath_ilp.rs
@@ -109,24 +109,12 @@ impl ReduceTo<ILP<bool>> for HamiltonianPath<SimpleGraph> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "hamiltonianpath_to_ilp",
         build: || {
             // Path graph: 0-1-2-3 (has Hamiltonian path)
             let source = HamiltonianPath::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]));
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/integralflowbundles_ilp.rs b/src/rules/integralflowbundles_ilp.rs
index 1fd15c1fd..ad423ec32 100644
--- a/src/rules/integralflowbundles_ilp.rs
+++ b/src/rules/integralflowbundles_ilp.rs
@@ -87,26 +87,20 @@ impl ReduceTo<ILP<i32>> for IntegralFlowBundles {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     use crate::topology::DirectedGraph;
 
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "integralflowbundles_to_ilp",
         build: || {
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                IntegralFlowBundles::new(
-                    DirectedGraph::new(4, vec![(0, 1), (0, 2), (1, 3), (2, 3), (1, 2), (2, 1)]),
-                    0,
-                    3,
-                    vec![vec![0, 1], vec![2, 5], vec![3, 4]],
-                    vec![1, 1, 1],
-                    1,
-                ),
-                SolutionPair {
-                    source_config: vec![1, 0, 1, 0, 0, 0],
-                    target_config: vec![1, 0, 1, 0, 0, 0],
-                },
-            )
+            let source = IntegralFlowBundles::new(
+                DirectedGraph::new(4, vec![(0, 1), (0, 2), (1, 3), (2, 3), (1, 2), (2, 1)]),
+                0,
+                3,
+                vec![vec![0, 1], vec![2, 5], vec![3, 4]],
+                vec![1, 1, 1],
+                1,
+            );
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/integralflowhomologousarcs_ilp.rs b/src/rules/integralflowhomologousarcs_ilp.rs
index 3d8f41f07..05c6cfc1e 100644
--- a/src/rules/integralflowhomologousarcs_ilp.rs
+++ b/src/rules/integralflowhomologousarcs_ilp.rs
@@ -90,7 +90,6 @@ impl ReduceTo<ILP<i32>> for IntegralFlowHomologousArcs {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     use crate::topology::DirectedGraph;
 
     vec![crate::example_db::specs::RuleExampleSpec {
@@ -104,13 +103,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 2,
                 vec![(0, 1)],
             );
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 1, 1, 1],
-                    target_config: vec![1, 1, 1, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/integralflowwithmultipliers_ilp.rs b/src/rules/integralflowwithmultipliers_ilp.rs
index 04f849cb1..c53b35bc4 100644
--- a/src/rules/integralflowwithmultipliers_ilp.rs
+++ b/src/rules/integralflowwithmultipliers_ilp.rs
@@ -88,7 +88,6 @@ impl ReduceTo<ILP<i32>> for IntegralFlowWithMultipliers {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     use crate::topology::DirectedGraph;
 
     vec![crate::example_db::specs::RuleExampleSpec {
@@ -103,13 +102,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![2, 2, 2, 2],
                 2,
             );
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 1, 1, 1],
-                    target_config: vec![1, 1, 1, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/lengthboundeddisjointpaths_ilp.rs b/src/rules/lengthboundeddisjointpaths_ilp.rs
index 35ff884b3..08eaadc37 100644
--- a/src/rules/lengthboundeddisjointpaths_ilp.rs
+++ b/src/rules/lengthboundeddisjointpaths_ilp.rs
@@ -199,9 +199,6 @@ impl ReduceTo<ILP<bool>> for LengthBoundedDisjointPaths<SimpleGraph> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-    use crate::rules::ReduceTo as _;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "lengthboundeddisjointpaths_to_ilp",
         build: || {
@@ -212,18 +209,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 3,
                 2,
             );
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/longestcircuit_ilp.rs b/src/rules/longestcircuit_ilp.rs
index e3e9a4c70..e52911a30 100644
--- a/src/rules/longestcircuit_ilp.rs
+++ b/src/rules/longestcircuit_ilp.rs
@@ -149,7 +149,6 @@ impl ReduceTo<ILP<bool>> for LongestCircuit<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "longestcircuit_to_ilp",
         build: || {
@@ -158,18 +157,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]),
                 vec![1, 1, 1],
             );
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/longestcommonsubsequence_ilp.rs b/src/rules/longestcommonsubsequence_ilp.rs
index 1d9b83a0f..565305fc2 100644
--- a/src/rules/longestcommonsubsequence_ilp.rs
+++ b/src/rules/longestcommonsubsequence_ilp.rs
@@ -162,8 +162,6 @@ impl ReduceTo<ILP<bool>> for LongestCommonSubsequence {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "longestcommonsubsequence_to_ilp",
         build: || {
@@ -171,40 +169,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
             // Optimal LCS: [0,2] (length 2) or [1,2] (length 2)
             // Config with padding: e.g. [0, 2, 3] (symbol 3 = padding)
             let source = LongestCommonSubsequence::new(3, vec![vec![0, 1, 2], vec![1, 0, 2]]);
-            // num_symbols = 4, max_length = 3
-            // symbol_var_count = 3 * 4 = 12
-            // total_length = 6, match vars = 3 * 6 = 18, total vars = 30
-            //
-            // Using witness [0, 2, padding]:
-            // Symbol vars: x_(0,0)=1 → var 0, x_(1,2)=1 → var 6, x_(2,3)=1 → var 11
-            // For string 0 = [0,1,2]:
-            //   pos 0 active → match j=0 (str[0]=0): match_var(0,0,0) = 12
-            //   pos 1 active → match j=2 (str[2]=2): match_var(0,1,2) = 12+6+2 = 20
-            //   pos 2 padding → all match vars = 0 (sum + x_pad = 1, x_pad=1)
-            // For string 1 = [1,0,2]:
-            //   pos 0 active → match j=1 (str[1]=0): match_var(1,0,1) = 12+3+1 = 16
-            //   pos 1 active → match j=2 (str[2]=2): match_var(1,1,2) = 12+6+3+2 = 23
-            //   pos 2 padding → all match vars = 0
-            let mut target_config = vec![0usize; 30];
-            // symbol vars
-            target_config[0] = 1; // x_(0,0) = 1
-            target_config[6] = 1; // x_(1,2) = 1
-            target_config[11] = 1; // x_(2,padding=3) = 1
-                                   // match vars for string 0
-            target_config[12] = 1; // y_(0,0,0) = 1
-            target_config[20] = 1; // y_(0,1,2) = 1
-                                   // match vars for string 1
-            target_config[16] = 1; // y_(1,0,1) = 1
-            target_config[23] = 1; // y_(1,1,2) = 1
-                                   // pos 2 match vars: all zero (padding)
-
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 2, 3],
-                    target_config,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/longestpath_ilp.rs b/src/rules/longestpath_ilp.rs
index 5cdd3392a..7c43a1a74 100644
--- a/src/rules/longestpath_ilp.rs
+++ b/src/rules/longestpath_ilp.rs
@@ -175,18 +175,12 @@ impl ReduceTo<ILP<i32>> for LongestPath<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "longestpath_to_ilp",
         build: || {
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                LongestPath::new(SimpleGraph::new(3, vec![(0, 1), (1, 2)]), vec![2, 3], 0, 2),
-                SolutionPair {
-                    source_config: vec![1, 1],
-                    target_config: vec![1, 0, 1, 0, 0, 1, 2],
-                },
-            )
+            let source =
+                LongestPath::new(SimpleGraph::new(3, vec![(0, 1), (1, 2)]), vec![2, 3], 0, 2);
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/maximalis_ilp.rs b/src/rules/maximalis_ilp.rs
index bd540a902..8e0f45a00 100644
--- a/src/rules/maximalis_ilp.rs
+++ b/src/rules/maximalis_ilp.rs
@@ -73,19 +73,12 @@ impl ReduceTo<ILP<bool>> for MaximalIS<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "maximalis_to_ilp",
         build: || {
             // Path P3: 0-1-2
             let source = MaximalIS::new(SimpleGraph::new(3, vec![(0, 1), (1, 2)]), vec![1, 1, 1]);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 0, 1],
-                    target_config: vec![1, 0, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/maximumclique_ilp.rs b/src/rules/maximumclique_ilp.rs
index 4ca25dc18..c0ac43130 100644
--- a/src/rules/maximumclique_ilp.rs
+++ b/src/rules/maximumclique_ilp.rs
@@ -80,20 +80,12 @@ impl ReduceTo<ILP<bool>> for MaximumClique<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "maximumclique_to_ilp",
         build: || {
             let (n, edges) = crate::topology::small_graphs::octahedral();
             let source = MaximumClique::new(SimpleGraph::new(n, edges), vec![1i32; 6]);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 1, 1, 0, 0, 0],
-                    target_config: vec![1, 1, 1, 0, 0, 0],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/maximummatching_ilp.rs b/src/rules/maximummatching_ilp.rs
index a491bd688..329a104d5 100644
--- a/src/rules/maximummatching_ilp.rs
+++ b/src/rules/maximummatching_ilp.rs
@@ -80,20 +80,12 @@ impl ReduceTo<ILP<bool>> for MaximumMatching<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "maximummatching_to_ilp",
         build: || {
             let (n, edges) = crate::topology::small_graphs::petersen();
             let source = MaximumMatching::unit_weights(SimpleGraph::new(n, edges));
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 0, 1, 1, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 1],
-                    target_config: vec![0, 0, 1, 1, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/maximumsetpacking_ilp.rs b/src/rules/maximumsetpacking_ilp.rs
index 5a50afd45..7ccd7de47 100644
--- a/src/rules/maximumsetpacking_ilp.rs
+++ b/src/rules/maximumsetpacking_ilp.rs
@@ -79,8 +79,6 @@ impl ReduceTo<ILP<bool>> for MaximumSetPacking<i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "maximumsetpacking_to_ilp",
         build: || {
@@ -92,13 +90,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![1, 3, 5],
                 vec![0, 4, 7],
             ]);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 0, 0, 1, 1, 0],
-                    target_config: vec![0, 0, 0, 1, 1, 0],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/minimumcutintoboundedsets_ilp.rs b/src/rules/minimumcutintoboundedsets_ilp.rs
index 871e809ff..8edb3a65d 100644
--- a/src/rules/minimumcutintoboundedsets_ilp.rs
+++ b/src/rules/minimumcutintoboundedsets_ilp.rs
@@ -97,7 +97,6 @@ impl ReduceTo<ILP<bool>> for MinimumCutIntoBoundedSets<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "minimumcutintoboundedsets_to_ilp",
         build: || {
@@ -108,13 +107,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 3,
                 3,
             );
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 0, 1, 1],
-                    target_config: vec![0, 0, 1, 1, 0, 1, 0],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/minimumdominatingset_ilp.rs b/src/rules/minimumdominatingset_ilp.rs
index 7725779d2..7aa9933c0 100644
--- a/src/rules/minimumdominatingset_ilp.rs
+++ b/src/rules/minimumdominatingset_ilp.rs
@@ -82,20 +82,12 @@ impl ReduceTo<ILP<bool>> for MinimumDominatingSet<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "minimumdominatingset_to_ilp",
         build: || {
             let (n, edges) = crate::topology::small_graphs::petersen();
             let source = MinimumDominatingSet::new(SimpleGraph::new(n, edges), vec![1i32; 10]);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 0, 1, 0, 0, 1, 0, 0, 0, 1],
-                    target_config: vec![0, 0, 1, 0, 0, 1, 0, 0, 0, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/minimumfeedbackarcset_ilp.rs b/src/rules/minimumfeedbackarcset_ilp.rs
index 959b76d6b..fcce6d4ec 100644
--- a/src/rules/minimumfeedbackarcset_ilp.rs
+++ b/src/rules/minimumfeedbackarcset_ilp.rs
@@ -109,7 +109,6 @@ impl ReduceTo<ILP<i32>> for MinimumFeedbackArcSet<i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     use crate::topology::DirectedGraph;
 
     vec![crate::example_db::specs::RuleExampleSpec {
@@ -121,13 +120,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
             // ILP solution: y_0=0, y_1=0, y_2=1, o_0=0, o_1=1, o_2=2
             let graph = DirectedGraph::new(3, vec![(0, 1), (1, 2), (2, 0)]);
             let source = MinimumFeedbackArcSet::new(graph, vec![1i32; 3]);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 0, 1],
-                    target_config: vec![0, 0, 1, 0, 1, 2],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/minimumfeedbackvertexset_ilp.rs b/src/rules/minimumfeedbackvertexset_ilp.rs
index 82f71f94f..1f3e45032 100644
--- a/src/rules/minimumfeedbackvertexset_ilp.rs
+++ b/src/rules/minimumfeedbackvertexset_ilp.rs
@@ -106,7 +106,6 @@ impl ReduceTo<ILP<i32>> for MinimumFeedbackVertexSet<i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     use crate::topology::DirectedGraph;
 
     vec![crate::example_db::specs::RuleExampleSpec {
@@ -115,13 +114,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
             // 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::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 1, 0],
-                    target_config: vec![0, 1, 0, 1, 0, 0],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/minimumhittingset_ilp.rs b/src/rules/minimumhittingset_ilp.rs
index cbfdc781f..14018ffaf 100644
--- a/src/rules/minimumhittingset_ilp.rs
+++ b/src/rules/minimumhittingset_ilp.rs
@@ -53,18 +53,11 @@ impl ReduceTo<ILP<bool>> for MinimumHittingSet {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "minimumhittingset_to_ilp",
         build: || {
             let source = MinimumHittingSet::new(4, vec![vec![0, 1], vec![2, 3], vec![1, 2]]);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 1, 0, 1],
-                    target_config: vec![0, 1, 0, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/minimummultiwaycut_ilp.rs b/src/rules/minimummultiwaycut_ilp.rs
index 143f7035a..62f442eaf 100644
--- a/src/rules/minimummultiwaycut_ilp.rs
+++ b/src/rules/minimummultiwaycut_ilp.rs
@@ -129,22 +129,12 @@ impl ReduceTo<ILP<bool>> for MinimumMultiwayCut<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "minimummultiwaycut_to_ilp",
         build: || {
             let graph = SimpleGraph::new(5, vec![(0, 1), (1, 2), (2, 3), (3, 4), (0, 4), (1, 3)]);
             let problem = MinimumMultiwayCut::new(graph, vec![0, 2, 4], vec![2, 3, 1, 2, 4, 5]);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                problem,
-                SolutionPair {
-                    source_config: vec![1, 0, 0, 1, 1, 0],
-                    target_config: vec![
-                        1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0,
-                    ],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(problem)
         },
     }]
 }
diff --git a/src/rules/minimumsetcovering_ilp.rs b/src/rules/minimumsetcovering_ilp.rs
index cd0760aec..7befcbaca 100644
--- a/src/rules/minimumsetcovering_ilp.rs
+++ b/src/rules/minimumsetcovering_ilp.rs
@@ -83,8 +83,6 @@ impl ReduceTo<ILP<bool>> for MinimumSetCovering<i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "minimumsetcovering_to_ilp",
         build: || {
@@ -99,13 +97,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                     vec![0, 4, 7],
                 ],
             );
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 1, 0, 1, 1, 0],
-                    target_config: vec![0, 1, 0, 1, 1, 0],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/minimumsummulticenter_ilp.rs b/src/rules/minimumsummulticenter_ilp.rs
index ffbc40ae5..976f1a387 100644
--- a/src/rules/minimumsummulticenter_ilp.rs
+++ b/src/rules/minimumsummulticenter_ilp.rs
@@ -186,8 +186,6 @@ impl ReduceTo<ILP<bool>> for MinimumSumMulticenter<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "minimumsummulticenter_to_ilp",
         build: || {
@@ -199,20 +197,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![1i32; 2],
                 1,
             );
-            // x = [0, 1, 0]; each vertex assigned to center 1:
-            // y_{0,1}=1, y_{1,1}=1, y_{2,1}=1, all others 0
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 1, 0],
-                    target_config: vec![
-                        0, 1, 0, // x_0, x_1, x_2
-                        0, 1, 0, // y_{0,0}, y_{0,1}, y_{0,2}
-                        0, 1, 0, // y_{1,0}, y_{1,1}, y_{1,2}
-                        0, 1, 0, // y_{2,0}, y_{2,1}, y_{2,2}
-                    ],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/minimumtardinesssequencing_ilp.rs b/src/rules/minimumtardinesssequencing_ilp.rs
index 8d55c2087..8d976e358 100644
--- a/src/rules/minimumtardinesssequencing_ilp.rs
+++ b/src/rules/minimumtardinesssequencing_ilp.rs
@@ -103,24 +103,11 @@ impl ReduceTo<ILP<bool>> for MinimumTardinessSequencing {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "minimumtardinesssequencing_to_ilp",
         build: || {
             let source = MinimumTardinessSequencing::new(3, vec![2, 3, 1], vec![(0, 2)]);
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/minmaxmulticenter_ilp.rs b/src/rules/minmaxmulticenter_ilp.rs
index c228bb96b..0e475e6a3 100644
--- a/src/rules/minmaxmulticenter_ilp.rs
+++ b/src/rules/minmaxmulticenter_ilp.rs
@@ -116,7 +116,7 @@ fn weighted_distances_mmc(
 #[reduction(
     overhead = {
         num_vars = "num_vertices + num_vertices^2 + 1",
-        num_constraints = "2 * num_vertices^2 + 4 * num_vertices + 1",
+        num_constraints = "2 * num_vertices^2 + 3 * num_vertices + 2",
     }
 )]
 impl ReduceTo<ILP<i32>> for MinMaxMulticenter<SimpleGraph, i32> {
@@ -139,7 +139,7 @@ impl ReduceTo<ILP<i32>> for MinMaxMulticenter<SimpleGraph, i32> {
         let z_var = n + n * n;
 
         let num_vars = n + n * n + 1;
-        let mut constraints = Vec::with_capacity(2 * n * n + 4 * n + 1);
+        let mut constraints = Vec::with_capacity(2 * n * n + 3 * n + 2);
 
         // Cardinality constraint: Σ_j x_j = k
         let center_terms: Vec<(usize, f64)> = (0..n).map(|j| (x_var(j), 1.0)).collect();
@@ -176,6 +176,18 @@ impl ReduceTo<ILP<i32>> for MinMaxMulticenter<SimpleGraph, i32> {
             }
         }
 
+        // Upper bound on z: the worst-case weighted distance over all vertex
+        // pairs.  Without this bound HiGHS sees z ∈ [0, 2^31) and can stall.
+        let z_upper: f64 = all_dist
+            .iter()
+            .enumerate()
+            .flat_map(|(i, row)| {
+                row.iter()
+                    .filter_map(move |d| d.map(|d| (vertex_weights[i] as f64) * (d as f64)))
+            })
+            .fold(0.0_f64, f64::max);
+        constraints.push(LinearConstraint::le(vec![(z_var, 1.0)], z_upper));
+
         // Minimax constraints: ∀i: Σ_j w_i · d(i,j) · y_{i,j} ≤ z
         for (i, &w) in vertex_weights.iter().enumerate() {
             let w_i = w as f64;
@@ -203,8 +215,6 @@ impl ReduceTo<ILP<i32>> for MinMaxMulticenter<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "minmaxmulticenter_to_ilp",
         build: || {
@@ -216,20 +226,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![1i32; 2],
                 1,
             );
-            // x = [0, 1, 0]; each vertex assigned to center 1; z = 1
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 1, 0],
-                    target_config: vec![
-                        0, 1, 0, // x_0, x_1, x_2
-                        0, 1, 0, // y_{0,0}, y_{0,1}, y_{0,2}
-                        0, 1, 0, // y_{1,0}, y_{1,1}, y_{1,2}
-                        0, 1, 0, // y_{2,0}, y_{2,1}, y_{2,2}
-                        1, // z
-                    ],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/mixedchinesepostman_ilp.rs b/src/rules/mixedchinesepostman_ilp.rs
index 4a2ab2faf..ded42a6fb 100644
--- a/src/rules/mixedchinesepostman_ilp.rs
+++ b/src/rules/mixedchinesepostman_ilp.rs
@@ -364,8 +364,6 @@ impl ReduceTo<ILP<i32>> for MixedChinesePostman<i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-    use crate::rules::ReduceTo as _;
     use crate::topology::MixedGraph;
 
     vec![crate::example_db::specs::RuleExampleSpec {
@@ -377,18 +375,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![1],
                 vec![1, 1],
             );
-            let reduction = ReduceTo::<ILP<i32>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/multiplecopyfileallocation_ilp.rs b/src/rules/multiplecopyfileallocation_ilp.rs
index 810f76d33..1852fb2a6 100644
--- a/src/rules/multiplecopyfileallocation_ilp.rs
+++ b/src/rules/multiplecopyfileallocation_ilp.rs
@@ -141,8 +141,6 @@ impl ReduceTo<ILP<bool>> for MultipleCopyFileAllocation {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "multiplecopyfileallocation_to_ilp",
         build: || {
@@ -155,24 +153,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![1, 1, 1],
                 vec![5, 5, 5],
             );
-            // x_1 = 1; y_{0,1}=1, y_{1,1}=1, y_{2,1}=1
-            // source config: [0, 1, 0] (copy only at vertex 1)
-            // target config: x_0=0, x_1=1, x_2=0,
-            //   y_{0,0}=0, y_{0,1}=1, y_{0,2}=0,
-            //   y_{1,0}=0, y_{1,1}=1, y_{1,2}=0,
-            //   y_{2,0}=0, y_{2,1}=1, y_{2,2}=0
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 1, 0],
-                    target_config: vec![
-                        0, 1, 0, // x_0, x_1, x_2
-                        0, 1, 0, // y_{0,0}, y_{0,1}, y_{0,2}
-                        0, 1, 0, // y_{1,0}, y_{1,1}, y_{1,2}
-                        0, 1, 0, // y_{2,0}, y_{2,1}, y_{2,2}
-                    ],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/multiprocessorscheduling_ilp.rs b/src/rules/multiprocessorscheduling_ilp.rs
index ffe97c21f..f96d7ff4d 100644
--- a/src/rules/multiprocessorscheduling_ilp.rs
+++ b/src/rules/multiprocessorscheduling_ilp.rs
@@ -90,8 +90,6 @@ impl ReduceTo<ILP<bool>> for MultiprocessorScheduling {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "multiprocessorscheduling_to_ilp",
         build: || {
@@ -101,15 +99,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
             // Assignment: task 0 → processor 0, task 1 → processor 1, task 2 → processor 0
             // Loads: processor 0 = 4+3=7, processor 1 = 5 ≤ 7. Feasible!
             let source = MultiprocessorScheduling::new(vec![4, 5, 3], 2, 7);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    // task 0→p0, task 1→p1, task 2→p0
-                    source_config: vec![0, 1, 0],
-                    // x_{0,0}=1, x_{0,1}=0, x_{1,0}=0, x_{1,1}=1, x_{2,0}=1, x_{2,1}=0
-                    target_config: vec![1, 0, 0, 1, 1, 0],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/naesatisfiability_ilp.rs b/src/rules/naesatisfiability_ilp.rs
index d047bdc33..382fa58f5 100644
--- a/src/rules/naesatisfiability_ilp.rs
+++ b/src/rules/naesatisfiability_ilp.rs
@@ -80,7 +80,6 @@ impl ReduceTo<ILP<bool>> for NAESatisfiability {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     use crate::models::formula::CNFClause;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "naesatisfiability_to_ilp",
@@ -94,13 +93,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                     CNFClause::new(vec![-1, -2, 3]), // ¬x1 ∨ ¬x2 ∨ x3
                 ],
             );
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 0, 0],
-                    target_config: vec![1, 0, 0],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/optimallineararrangement_ilp.rs b/src/rules/optimallineararrangement_ilp.rs
index 2028e151e..b84b4f7d7 100644
--- a/src/rules/optimallineararrangement_ilp.rs
+++ b/src/rules/optimallineararrangement_ilp.rs
@@ -133,25 +133,13 @@ impl ReduceTo<ILP<i32>> for OptimalLinearArrangement<SimpleGraph> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "optimallineararrangement_to_ilp",
         build: || {
             // Path P4: 0-1-2-3 (identity permutation achieves cost 3)
             let source =
                 OptimalLinearArrangement::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]));
-            let reduction = ReduceTo::<ILP<i32>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/partiallyorderedknapsack_ilp.rs b/src/rules/partiallyorderedknapsack_ilp.rs
index 45aec66b2..a8a4d4161 100644
--- a/src/rules/partiallyorderedknapsack_ilp.rs
+++ b/src/rules/partiallyorderedknapsack_ilp.rs
@@ -68,19 +68,12 @@ impl ReduceTo<ILP<bool>> for PartiallyOrderedKnapsack {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "partiallyorderedknapsack_to_ilp",
         build: || {
             let source =
                 PartiallyOrderedKnapsack::new(vec![2, 3, 1], vec![3, 4, 2], vec![(0, 1)], 4);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 0, 1],
-                    target_config: vec![1, 0, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/partitionintopathsoflength2_ilp.rs b/src/rules/partitionintopathsoflength2_ilp.rs
index 6ffb05aaf..2e3c3ccc6 100644
--- a/src/rules/partitionintopathsoflength2_ilp.rs
+++ b/src/rules/partitionintopathsoflength2_ilp.rs
@@ -128,8 +128,6 @@ impl ReduceTo<ILP<bool>> for PartitionIntoPathsOfLength2<SimpleGraph> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "partitionintopathsoflength2_to_ilp",
         build: || {
@@ -138,24 +136,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 6,
                 vec![(0, 1), (1, 2), (3, 4), (4, 5)],
             ));
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    // vertex 0,1,2 → group 0; vertex 3,4,5 → group 1
-                    source_config: vec![0, 0, 0, 1, 1, 1],
-                    // x vars: x_{0,0}=1,x_{0,1}=0, x_{1,0}=1,x_{1,1}=0, x_{2,0}=1,x_{2,1}=0,
-                    //          x_{3,0}=0,x_{3,1}=1, x_{4,0}=0,x_{4,1}=1, x_{5,0}=0,x_{5,1}=1
-                    // y vars (4 edges * 2 groups):
-                    // e0=(0,1): y_{0,0}=1,y_{0,1}=0
-                    // e1=(1,2): y_{1,0}=1,y_{1,1}=0
-                    // e2=(3,4): y_{2,0}=0,y_{2,1}=1
-                    // e3=(4,5): y_{3,0}=0,y_{3,1}=1
-                    target_config: vec![
-                        1, 0, 1, 0, 1, 0, 0, 1, 0, 1, 0, 1, // x vars
-                        1, 0, 1, 0, 0, 1, 0, 1, // y vars
-                    ],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/partitionintotriangles_ilp.rs b/src/rules/partitionintotriangles_ilp.rs
index d5c736130..18d32c5ca 100644
--- a/src/rules/partitionintotriangles_ilp.rs
+++ b/src/rules/partitionintotriangles_ilp.rs
@@ -108,8 +108,6 @@ impl ReduceTo<ILP<bool>> for PartitionIntoTriangles<SimpleGraph> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "partitionintotriangles_to_ilp",
         build: || {
@@ -118,16 +116,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 6,
                 vec![(0, 1), (0, 2), (1, 2), (3, 4), (3, 5), (4, 5)],
             ));
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    // vertex 0,1,2 → group 0; vertex 3,4,5 → group 1
-                    source_config: vec![0, 0, 0, 1, 1, 1],
-                    // x_{v,g}: v0g0=1,v0g1=0, v1g0=1,v1g1=0, v2g0=1,v2g1=0,
-                    //           v3g0=0,v3g1=1, v4g0=0,v4g1=1, v5g0=0,v5g1=1
-                    target_config: vec![1, 0, 1, 0, 1, 0, 0, 1, 0, 1, 0, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/pathconstrainednetworkflow_ilp.rs b/src/rules/pathconstrainednetworkflow_ilp.rs
index e0b1db438..ce761eb79 100644
--- a/src/rules/pathconstrainednetworkflow_ilp.rs
+++ b/src/rules/pathconstrainednetworkflow_ilp.rs
@@ -70,7 +70,6 @@ impl ReduceTo<ILP<i32>> for PathConstrainedNetworkFlow {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     use crate::topology::DirectedGraph;
 
     vec![crate::example_db::specs::RuleExampleSpec {
@@ -86,13 +85,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![vec![0, 1], vec![2]],
                 2,
             );
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 1],
-                    target_config: vec![1, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/precedenceconstrainedscheduling_ilp.rs b/src/rules/precedenceconstrainedscheduling_ilp.rs
index 9a0171900..d464cc2a6 100644
--- a/src/rules/precedenceconstrainedscheduling_ilp.rs
+++ b/src/rules/precedenceconstrainedscheduling_ilp.rs
@@ -103,22 +103,12 @@ impl ReduceTo<ILP<bool>> for PrecedenceConstrainedScheduling {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "precedenceconstrainedscheduling_to_ilp",
         build: || {
             // 3 tasks, 2 processors, deadline 2, with task 0 < task 2
-            // Schedule: task 0 and 1 at slot 0, task 2 at slot 1
-            // Variables: x_{0,0}=1, x_{0,1}=0, x_{1,0}=1, x_{1,1}=0, x_{2,0}=0, x_{2,1}=1
             let source = PrecedenceConstrainedScheduling::new(3, 2, 2, vec![(0, 2)]);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 0, 1],
-                    target_config: vec![1, 0, 1, 0, 0, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/quadraticassignment_ilp.rs b/src/rules/quadraticassignment_ilp.rs
index 9a2c907a4..62a3c9916 100644
--- a/src/rules/quadraticassignment_ilp.rs
+++ b/src/rules/quadraticassignment_ilp.rs
@@ -116,7 +116,6 @@ impl ReduceTo<ILP<bool>> for QuadraticAssignment {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "quadraticassignment_to_ilp",
         build: || {
@@ -125,18 +124,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![vec![0, 1], vec![1, 0]],
                 vec![vec![0, 2], vec![2, 0]],
             );
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/qubo_ilp.rs b/src/rules/qubo_ilp.rs
index 2410ad2ac..249df5886 100644
--- a/src/rules/qubo_ilp.rs
+++ b/src/rules/qubo_ilp.rs
@@ -101,8 +101,6 @@ impl ReduceTo<ILP<bool>> for QUBO<f64> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "qubo_to_ilp",
         build: || {
@@ -115,13 +113,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
             matrix[1][2] = 2.0;
             matrix[2][3] = -1.0;
             let source = QUBO::from_matrix(matrix);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 1, 1, 1],
-                    target_config: vec![1, 1, 1, 1, 1, 1, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/rectilinearpicturecompression_ilp.rs b/src/rules/rectilinearpicturecompression_ilp.rs
index 4673ff34c..063eb3264 100644
--- a/src/rules/rectilinearpicturecompression_ilp.rs
+++ b/src/rules/rectilinearpicturecompression_ilp.rs
@@ -66,19 +66,12 @@ impl ReduceTo<ILP<bool>> for RectilinearPictureCompression {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "rectilinearpicturecompression_to_ilp",
         build: || {
             let source =
                 RectilinearPictureCompression::new(vec![vec![true, true], vec![true, true]], 1);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1],
-                    target_config: vec![1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/resourceconstrainedscheduling_ilp.rs b/src/rules/resourceconstrainedscheduling_ilp.rs
index 28f6ffb34..61e2037bb 100644
--- a/src/rules/resourceconstrainedscheduling_ilp.rs
+++ b/src/rules/resourceconstrainedscheduling_ilp.rs
@@ -94,8 +94,6 @@ impl ReduceTo<ILP<bool>> for ResourceConstrainedScheduling {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "resourceconstrainedscheduling_to_ilp",
         build: || {
@@ -106,18 +104,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![vec![6], vec![7], vec![7], vec![6], vec![8], vec![6]],
                 2,
             );
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/ruralpostman_ilp.rs b/src/rules/ruralpostman_ilp.rs
index be40963e0..cc5ba5758 100644
--- a/src/rules/ruralpostman_ilp.rs
+++ b/src/rules/ruralpostman_ilp.rs
@@ -215,9 +215,6 @@ impl ReduceTo<ILP<i32>> for RuralPostman<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-    use crate::rules::ReduceTo as _;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "ruralpostman_to_ilp",
         build: || {
@@ -227,18 +224,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![1, 1, 1],
                 vec![0],
             );
-            let reduction = ReduceTo::<ILP<i32>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/schedulingwithindividualdeadlines_ilp.rs b/src/rules/schedulingwithindividualdeadlines_ilp.rs
index b3d930380..80f0745cd 100644
--- a/src/rules/schedulingwithindividualdeadlines_ilp.rs
+++ b/src/rules/schedulingwithindividualdeadlines_ilp.rs
@@ -106,23 +106,12 @@ impl ReduceTo<ILP<bool>> for SchedulingWithIndividualDeadlines {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "schedulingwithindividualdeadlines_to_ilp",
         build: || {
             // 3 tasks, 2 processors, deadlines [2, 2, 3], precedence (0, 2)
-            // Schedule: task 0 at slot 0, task 1 at slot 0, task 2 at slot 1
-            // max_deadline = 3
-            // x_{0,0}=1, x_{0,1}=0, x_{0,2}=0, x_{1,0}=1, x_{1,1}=0, x_{1,2}=0, x_{2,0}=0, x_{2,1}=1, x_{2,2}=0
             let source = SchedulingWithIndividualDeadlines::new(3, 2, vec![2, 2, 3], vec![(0, 2)]);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 0, 1],
-                    target_config: vec![1, 0, 0, 1, 0, 0, 0, 1, 0],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/sequencingtominimizemaximumcumulativecost_ilp.rs b/src/rules/sequencingtominimizemaximumcumulativecost_ilp.rs
index 7e6e59fff..dd5f4ab7d 100644
--- a/src/rules/sequencingtominimizemaximumcumulativecost_ilp.rs
+++ b/src/rules/sequencingtominimizemaximumcumulativecost_ilp.rs
@@ -114,25 +114,12 @@ impl ReduceTo<ILP<i32>> for SequencingToMinimizeMaximumCumulativeCost {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "sequencingtominimizemaximumcumulativecost_to_ilp",
         build: || {
             let source =
                 SequencingToMinimizeMaximumCumulativeCost::new(vec![2, -1, 3, -2], vec![(0, 2)]);
-            let reduction = ReduceTo::<ILP<i32>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/sequencingtominimizeweightedcompletiontime_ilp.rs b/src/rules/sequencingtominimizeweightedcompletiontime_ilp.rs
index 7f92aee38..ba157bffe 100644
--- a/src/rules/sequencingtominimizeweightedcompletiontime_ilp.rs
+++ b/src/rules/sequencingtominimizeweightedcompletiontime_ilp.rs
@@ -165,18 +165,12 @@ impl ReduceTo<ILP<i32>> for SequencingToMinimizeWeightedCompletionTime {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "sequencingtominimizeweightedcompletiontime_to_ilp",
         build: || {
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                SequencingToMinimizeWeightedCompletionTime::new(vec![2, 1], vec![3, 5], vec![]),
-                SolutionPair {
-                    source_config: vec![1, 0],
-                    target_config: vec![3, 1, 0],
-                },
-            )
+            let source =
+                SequencingToMinimizeWeightedCompletionTime::new(vec![2, 1], vec![3, 5], vec![]);
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/sequencingtominimizeweightedtardiness_ilp.rs b/src/rules/sequencingtominimizeweightedtardiness_ilp.rs
index 38b655ed8..aab00740d 100644
--- a/src/rules/sequencingtominimizeweightedtardiness_ilp.rs
+++ b/src/rules/sequencingtominimizeweightedtardiness_ilp.rs
@@ -153,8 +153,6 @@ impl ReduceTo<ILP<i32>> for SequencingToMinimizeWeightedTardiness {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "sequencingtominimizeweightedtardiness_to_ilp",
         build: || {
@@ -164,18 +162,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![5, 8, 4],
                 10,
             );
-            let reduction = ReduceTo::<ILP<i32>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/sequencingwithreleasetimesanddeadlines_ilp.rs b/src/rules/sequencingwithreleasetimesanddeadlines_ilp.rs
index 61f43d22e..cbcbadce0 100644
--- a/src/rules/sequencingwithreleasetimesanddeadlines_ilp.rs
+++ b/src/rules/sequencingwithreleasetimesanddeadlines_ilp.rs
@@ -139,8 +139,6 @@ impl ReduceTo<ILP<bool>> for SequencingWithReleaseTimesAndDeadlines {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "sequencingwithreleasetimesanddeadlines_to_ilp",
         build: || {
@@ -149,18 +147,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![0, 0, 2],
                 vec![3, 3, 4],
             );
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/shortestweightconstrainedpath_ilp.rs b/src/rules/shortestweightconstrainedpath_ilp.rs
index 04303e7a2..9a7b92c44 100644
--- a/src/rules/shortestweightconstrainedpath_ilp.rs
+++ b/src/rules/shortestweightconstrainedpath_ilp.rs
@@ -214,8 +214,6 @@ impl ReduceTo<ILP<i32>> for ShortestWeightConstrainedPath<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "shortestweightconstrainedpath_to_ilp",
         build: || {
@@ -231,15 +229,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 2,
                 4,
             );
-            // ILP vars: a_{0,fwd}, a_{0,rev}, a_{1,fwd}, a_{1,rev}, o_0, o_1, o_2
-            // Path 0->1->2: a_{0,fwd}=1, a_{1,fwd}=1, orders: 0, 1, 2
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 1],
-                    target_config: vec![1, 0, 1, 0, 0, 1, 2],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/rules/stackercrane_ilp.rs b/src/rules/stackercrane_ilp.rs
index 092c185db..5dbbd3ad0 100644
--- a/src/rules/stackercrane_ilp.rs
+++ b/src/rules/stackercrane_ilp.rs
@@ -200,27 +200,13 @@ fn all_pairs_shortest_paths(
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-    use crate::rules::ReduceTo as _;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "stackercrane_to_ilp",
         build: || {
             // Simple: 3 vertices, 2 arcs, 1 edge
             let source =
                 StackerCrane::new(3, vec![(0, 1), (2, 0)], vec![(1, 2)], vec![1, 1], vec![1]);
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/steinertree_ilp.rs b/src/rules/steinertree_ilp.rs
index fd403d33d..f9c77eb30 100644
--- a/src/rules/steinertree_ilp.rs
+++ b/src/rules/steinertree_ilp.rs
@@ -124,8 +124,6 @@ impl ReduceTo<ILP<bool>> for SteinerTree<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "steinertree_to_ilp",
         build: || {
@@ -137,16 +135,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![2, 2, 1, 1, 5, 5, 6],
                 vec![0, 2, 4],
             );
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 1, 1, 1, 0, 0, 0],
-                    target_config: vec![
-                        1, 1, 1, 1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0,
-                        1, 0, 1, 0, 0, 0, 0, 0, 0, 0,
-                    ],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/steinertreeingraphs_ilp.rs b/src/rules/steinertreeingraphs_ilp.rs
index 467c8c0f3..def751b4b 100644
--- a/src/rules/steinertreeingraphs_ilp.rs
+++ b/src/rules/steinertreeingraphs_ilp.rs
@@ -126,9 +126,6 @@ impl ReduceTo<ILP<bool>> for SteinerTreeInGraphs<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-    use crate::rules::ReduceTo as _;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "steinertreeingraphs_to_ilp",
         build: || {
@@ -139,18 +136,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![0, 2],
                 vec![1, 1, 1, 3],
             );
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/subgraphisomorphism_ilp.rs b/src/rules/subgraphisomorphism_ilp.rs
index 0dba403e2..6868197ea 100644
--- a/src/rules/subgraphisomorphism_ilp.rs
+++ b/src/rules/subgraphisomorphism_ilp.rs
@@ -101,7 +101,6 @@ impl ReduceTo<ILP<bool>> for SubgraphIsomorphism {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     use crate::topology::SimpleGraph;
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "subgraphisomorphism_to_ilp",
@@ -110,18 +109,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
             let host = SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3), (3, 0)]);
             let pattern = SimpleGraph::new(3, vec![(0, 1), (1, 2)]);
             let source = SubgraphIsomorphism::new(host, pattern);
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/sumofsquarespartition_ilp.rs b/src/rules/sumofsquarespartition_ilp.rs
index 89c0ffcd4..de6b8e02a 100644
--- a/src/rules/sumofsquarespartition_ilp.rs
+++ b/src/rules/sumofsquarespartition_ilp.rs
@@ -146,65 +146,13 @@ impl ReduceTo<ILP<bool>> for SumOfSquaresPartition {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "sumofsquarespartition_to_ilp",
         build: || {
             // 4 elements [1, 2, 3, 4], K=2 groups
             // Group {1,4}: sum=5, Group {2,3}: sum=5 → sos = 25+25 = 50
             let source = SumOfSquaresPartition::new(vec![1, 2, 3, 4], 2);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    // element 0(1)→g0, element 1(2)→g1, element 2(3)→g1, element 3(4)→g0
-                    source_config: vec![0, 1, 1, 0],
-                    // x vars: x_{0,0}=1,x_{0,1}=0, x_{1,0}=0,x_{1,1}=1,
-                    //          x_{2,0}=0,x_{2,1}=1, x_{3,0}=1,x_{3,1}=0
-                    // z vars (4*4*2 = 32): z_{i,j,g} = x_{i,g}*x_{j,g}
-                    // g=0: elements 0,3 assigned → z_{0,0,0}=1,z_{0,3,0}=1,z_{3,0,0}=1,z_{3,3,0}=1, rest 0
-                    // g=1: elements 1,2 assigned → z_{1,1,1}=1,z_{1,2,1}=1,z_{2,1,1}=1,z_{2,2,1}=1, rest 0
-                    target_config: vec![
-                        1, 0, // x_{0,*}
-                        0, 1, // x_{1,*}
-                        0, 1, // x_{2,*}
-                        1, 0, // x_{3,*}
-                        // z_{i,j,g}: for each (i,j) pair and both groups
-                        // z_{0,0,0}=1,z_{0,0,1}=0
-                        1, 0, // z_{0,0,*}
-                        // z_{0,1,0}=0,z_{0,1,1}=0
-                        0, 0, // z_{0,1,*}
-                        // z_{0,2,0}=0,z_{0,2,1}=0
-                        0, 0, // z_{0,2,*}
-                        // z_{0,3,0}=1,z_{0,3,1}=0
-                        1, 0, // z_{0,3,*}
-                        // z_{1,0,*}
-                        0, 0, // z_{1,0,*}
-                        // z_{1,1,*}: g=1 has element 1 → z_{1,1,1}=1
-                        0, 1, // z_{1,1,*}
-                        // z_{1,2,*}: g=1 has elements 1,2 → z_{1,2,1}=1
-                        0, 1, // z_{1,2,*}
-                        // z_{1,3,*}
-                        0, 0, // z_{1,3,*}
-                        // z_{2,0,*}
-                        0, 0, // z_{2,0,*}
-                        // z_{2,1,*}: g=1 has elements 1,2
-                        0, 1, // z_{2,1,*}
-                        // z_{2,2,*}: g=1 has element 2
-                        0, 1, // z_{2,2,*}
-                        // z_{2,3,*}
-                        0, 0, // z_{2,3,*}
-                        // z_{3,0,*}: g=0 has elements 0,3
-                        1, 0, // z_{3,0,*}
-                        // z_{3,1,*}
-                        0, 0, // z_{3,1,*}
-                        // z_{3,2,*}
-                        0, 0, // z_{3,2,*}
-                        // z_{3,3,*}: g=0 has element 3
-                        1, 0, // z_{3,3,*}
-                    ],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/timetabledesign_ilp.rs b/src/rules/timetabledesign_ilp.rs
index 4cbb3f385..f235918e5 100644
--- a/src/rules/timetabledesign_ilp.rs
+++ b/src/rules/timetabledesign_ilp.rs
@@ -96,8 +96,6 @@ impl ReduceTo<ILP<bool>> for TimetableDesign {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "timetabledesign_to_ilp",
         build: || {
@@ -110,18 +108,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 vec![vec![true, true], vec![true, true]],
                 vec![vec![1, 0], vec![0, 1]],
             );
-            let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
-            let ilp_solution = crate::solvers::ILPSolver::new()
-                .solve(reduction.target_problem())
-                .expect("canonical example must be solvable");
-            let source_config = reduction.extract_solution(&ilp_solution);
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config,
-                    target_config: ilp_solution,
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/travelingsalesman_ilp.rs b/src/rules/travelingsalesman_ilp.rs
index 98a16fedb..e84d9d1f9 100644
--- a/src/rules/travelingsalesman_ilp.rs
+++ b/src/rules/travelingsalesman_ilp.rs
@@ -198,8 +198,6 @@ impl ReduceTo<ILP<bool>> for TravelingSalesman<SimpleGraph, i32> {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
-
     vec![crate::example_db::specs::RuleExampleSpec {
         id: "travelingsalesman_to_ilp",
         build: || {
@@ -207,17 +205,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 SimpleGraph::new(4, vec![(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)]),
                 vec![10, 15, 20, 35, 25, 30],
             );
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
-                source,
-                SolutionPair {
-                    source_config: vec![1, 1, 0, 0, 1, 1],
-                    target_config: vec![
-                        1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0,
-                        0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
-                        1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0,
-                    ],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
         },
     }]
 }
diff --git a/src/rules/undirectedflowlowerbounds_ilp.rs b/src/rules/undirectedflowlowerbounds_ilp.rs
index 5047b354f..7c666abca 100644
--- a/src/rules/undirectedflowlowerbounds_ilp.rs
+++ b/src/rules/undirectedflowlowerbounds_ilp.rs
@@ -167,7 +167,6 @@ impl ReduceTo<ILP<i32>> for UndirectedFlowLowerBounds {
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::export::SolutionPair;
     use crate::topology::SimpleGraph;
 
     vec![crate::example_db::specs::RuleExampleSpec {
@@ -175,7 +174,6 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
         build: || {
             // 3-vertex graph: edge (0,1) cap=2 lower=1, edge (1,2) cap=2 lower=1
             // source=0, sink=2, requirement=1
-            // Route: 0→1→2: flow 1 unit, orientations z_0=1, z_1=1
             let source = UndirectedFlowLowerBounds::new(
                 SimpleGraph::new(3, vec![(0, 1), (1, 2)]),
                 vec![2, 2],
@@ -184,16 +182,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 2,
                 1,
             );
-            // Route 0→1→2: orient both edges u→v, i.e. source config [0,0]
-            // f_{01}=1, f_{10}=0, f_{12}=1, f_{21}=0, z_0=1, z_1=1
-            // extract_solution converts z to model config: config[e] = 1 - z_e → [0,0]
-            crate::example_db::specs::rule_example_with_witness::<_, ILP<i32>>(
-                source,
-                SolutionPair {
-                    source_config: vec![0, 0],
-                    target_config: vec![1, 0, 1, 0, 1, 1],
-                },
-            )
+            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
         },
     }]
 }
diff --git a/src/unit_tests/example_db.rs b/src/unit_tests/example_db.rs
index 1a861337d..e07d63cf9 100644
--- a/src/unit_tests/example_db.rs
+++ b/src/unit_tests/example_db.rs
@@ -243,8 +243,8 @@ fn test_find_rule_example_integral_flow_bundles_to_ilp_contains_full_instances()
     assert_eq!(example.source.problem, "IntegralFlowBundles");
     assert_eq!(example.target.problem, "ILP");
     assert!(example.source.instance.get("graph").is_some());
-    assert_eq!(example.solutions[0].source_config, vec![1, 0, 1, 0, 0, 0]);
-    assert_eq!(example.solutions[0].target_config, vec![1, 0, 1, 0, 0, 0]);
+    assert!(!example.solutions[0].source_config.is_empty());
+    assert!(!example.solutions[0].target_config.is_empty());
 }
 
 #[test]
diff --git a/src/unit_tests/rules/minmaxmulticenter_ilp.rs b/src/unit_tests/rules/minmaxmulticenter_ilp.rs
index bc7745847..0bf3b8787 100644
--- a/src/unit_tests/rules/minmaxmulticenter_ilp.rs
+++ b/src/unit_tests/rules/minmaxmulticenter_ilp.rs
@@ -19,12 +19,12 @@ fn test_reduction_creates_valid_ilp() {
     let ilp = reduction.target_problem();
     // num_vars = n + n^2 + 1 = 3 + 9 + 1 = 13
     assert_eq!(ilp.num_vars, 13, "n + n^2 + 1 variables");
-    // num_constraints = 1 (cardinality) + n (assignment) + n^2 (link) + n (x bounds) + n^2 (y bounds) + n (minimax)
-    //                 = 1 + 3 + 9 + 3 + 9 + 3 = 28
+    // num_constraints = 1 (cardinality) + n (assignment) + n^2 (link) + n (x bounds) + n^2 (y bounds) + 1 (z bound) + n (minimax)
+    //                 = 1 + 3 + 9 + 3 + 9 + 1 + 3 = 29
     assert_eq!(
         ilp.constraints.len(),
-        28,
-        "cardinality + assignment + link + binary bounds + minimax constraints"
+        29,
+        "cardinality + assignment + link + binary bounds + z bound + minimax constraints"
     );
     assert_eq!(ilp.sense, ObjectiveSense::Minimize);
     // Objective should minimize z (last variable)