diff --git a/src/rules/test_helpers.rs b/src/rules/test_helpers.rs
index 6053ad18..9fb71e31 100644
--- a/src/rules/test_helpers.rs
+++ b/src/rules/test_helpers.rs
@@ -193,6 +193,23 @@ pub(crate) fn assert_satisfaction_round_trip_from_satisfaction_target<R>(
     );
 }
 
+#[cfg(feature = "ilp-solver")]
+pub(crate) fn assert_bf_vs_ilp<R>(source: &R::Source, reduction: &R)
+where
+    R: ReductionResult,
+    R::Source: Problem + 'static,
+    R::Target: 'static,
+    <R::Source as Problem>::Value: Aggregate + std::fmt::Debug + PartialEq,
+{
+    use crate::solvers::{ILPSolver, Solver};
+    let bf_value = BruteForce::new().solve(source);
+    let ilp_solution = ILPSolver::new()
+        .solve_dyn(reduction.target_problem())
+        .expect("ILP should be solvable");
+    let extracted = reduction.extract_solution(&ilp_solution);
+    assert_eq!(source.evaluate(&extracted), bf_value);
+}
+
 pub(crate) fn solve_optimization_problem<P>(problem: &P) -> Option<Vec<usize>>
 where
     P: Problem + 'static,
diff --git a/src/unit_tests/rules/acyclicpartition_ilp.rs b/src/unit_tests/rules/acyclicpartition_ilp.rs
index 3aa3c8cc..97efc979 100644
--- a/src/unit_tests/rules/acyclicpartition_ilp.rs
+++ b/src/unit_tests/rules/acyclicpartition_ilp.rs
@@ -78,3 +78,10 @@ fn test_infeasible_instance() {
     let solver = ILPSolver::new();
     assert!(solver.solve(ilp).is_none());
 }
+
+#[test]
+fn test_acyclicpartition_to_ilp_bf_vs_ilp() {
+    let source = small_instance();
+    let reduction: ReductionAcyclicPartitionToILP = ReduceTo::<ILP<i32>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/balancedcompletebipartitesubgraph_ilp.rs b/src/unit_tests/rules/balancedcompletebipartitesubgraph_ilp.rs
index 6ba457bd..9c4cc110 100644
--- a/src/unit_tests/rules/balancedcompletebipartitesubgraph_ilp.rs
+++ b/src/unit_tests/rules/balancedcompletebipartitesubgraph_ilp.rs
@@ -58,3 +58,10 @@ fn test_extract_solution_identity() {
     assert_eq!(extracted, vec![1, 1, 0, 1, 1, 0]);
     assert!(source.evaluate(&extracted).0);
 }
+
+#[test]
+fn test_balancedcompletebipartitesubgraph_to_ilp_bf_vs_ilp() {
+    let source = small_instance();
+    let reduction: ReductionBCBSToILP = ReduceTo::<ILP<bool>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/bicliquecover_ilp.rs b/src/unit_tests/rules/bicliquecover_ilp.rs
index e3617056..db542b59 100644
--- a/src/unit_tests/rules/bicliquecover_ilp.rs
+++ b/src/unit_tests/rules/bicliquecover_ilp.rs
@@ -61,3 +61,10 @@ fn test_single_edge() {
         "single edge biclique cover",
     );
 }
+
+#[test]
+fn test_bicliquecover_to_ilp_bf_vs_ilp() {
+    let source = small_instance();
+    let reduction: ReductionBicliqueCoverToILP = ReduceTo::<ILP<bool>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/biconnectivityaugmentation_ilp.rs b/src/unit_tests/rules/biconnectivityaugmentation_ilp.rs
index 6ae7488c..fa21abed 100644
--- a/src/unit_tests/rules/biconnectivityaugmentation_ilp.rs
+++ b/src/unit_tests/rules/biconnectivityaugmentation_ilp.rs
@@ -77,3 +77,10 @@ fn test_already_biconnected() {
     let extracted = reduction.extract_solution(&ilp_sol);
     assert!(source.evaluate(&extracted).0);
 }
+
+#[test]
+fn test_biconnectivityaugmentation_to_ilp_bf_vs_ilp() {
+    let source = small_instance();
+    let reduction: ReductionBiconnAugToILP = ReduceTo::<ILP<i32>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/binpacking_ilp.rs b/src/unit_tests/rules/binpacking_ilp.rs
index b7b63cf3..772eb460 100644
--- a/src/unit_tests/rules/binpacking_ilp.rs
+++ b/src/unit_tests/rules/binpacking_ilp.rs
@@ -141,3 +141,10 @@ fn test_solve_reduced() {
     assert!(problem.evaluate(&solution).is_valid());
     assert_eq!(problem.evaluate(&solution), Min(Some(3)));
 }
+
+#[test]
+fn test_binpacking_to_ilp_bf_vs_ilp() {
+    let problem = BinPacking::new(vec![3, 3, 2], 5);
+    let reduction: ReductionBPToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/bottlenecktravelingsalesman_ilp.rs b/src/unit_tests/rules/bottlenecktravelingsalesman_ilp.rs
index fbe2a0e4..70452a9e 100644
--- a/src/unit_tests/rules/bottlenecktravelingsalesman_ilp.rs
+++ b/src/unit_tests/rules/bottlenecktravelingsalesman_ilp.rs
@@ -96,3 +96,10 @@ fn test_no_hamiltonian_cycle_infeasible() {
         "Path graph should have no Hamiltonian cycle"
     );
 }
+
+#[test]
+fn test_bottlenecktravelingsalesman_to_ilp_bf_vs_ilp() {
+    let problem = k4_btsp();
+    let reduction: ReductionBTSPToILP = ReduceTo::<ILP<i32>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/boundedcomponentspanningforest_ilp.rs b/src/unit_tests/rules/boundedcomponentspanningforest_ilp.rs
index 08836b80..bd97a4a9 100644
--- a/src/unit_tests/rules/boundedcomponentspanningforest_ilp.rs
+++ b/src/unit_tests/rules/boundedcomponentspanningforest_ilp.rs
@@ -83,3 +83,10 @@ fn test_infeasible_instance() {
     let solver = ILPSolver::new();
     assert!(solver.solve(ilp).is_none());
 }
+
+#[test]
+fn test_boundedcomponentspanningforest_to_ilp_bf_vs_ilp() {
+    let source = small_instance();
+    let reduction: ReductionBCSFToILP = ReduceTo::<ILP<i32>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/capacityassignment_ilp.rs b/src/unit_tests/rules/capacityassignment_ilp.rs
index eae71474..a5efbb8b 100644
--- a/src/unit_tests/rules/capacityassignment_ilp.rs
+++ b/src/unit_tests/rules/capacityassignment_ilp.rs
@@ -101,3 +101,15 @@ fn test_capacityassignment_to_ilp_trivial() {
     let extracted = reduction.extract_solution(&ilp_solution);
     assert!(problem.evaluate(&extracted).0.is_some());
 }
+
+#[test]
+fn test_capacityassignment_to_ilp_bf_vs_ilp() {
+    let problem = CapacityAssignment::new(
+        vec![1, 2, 3],
+        vec![vec![1, 3, 6], vec![2, 4, 7], vec![1, 2, 5]],
+        vec![vec![8, 4, 1], vec![7, 3, 1], vec![6, 3, 1]],
+        12,
+    );
+    let reduction: ReductionCAToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/coloring_ilp.rs b/src/unit_tests/rules/coloring_ilp.rs
index f9cbfa0b..f436f39b 100644
--- a/src/unit_tests/rules/coloring_ilp.rs
+++ b/src/unit_tests/rules/coloring_ilp.rs
@@ -271,3 +271,10 @@ fn test_single_edge() {
     assert!(problem.evaluate(&extracted));
     assert_ne!(extracted[0], extracted[1]);
 }
+
+#[test]
+fn test_coloring_to_ilp_bf_vs_ilp() {
+    let problem = KColoring::<K3, _>::new(SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]));
+    let reduction = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/directedtwocommodityintegralflow_ilp.rs b/src/unit_tests/rules/directedtwocommodityintegralflow_ilp.rs
index a813325f..27b0972b 100644
--- a/src/unit_tests/rules/directedtwocommodityintegralflow_ilp.rs
+++ b/src/unit_tests/rules/directedtwocommodityintegralflow_ilp.rs
@@ -118,3 +118,10 @@ fn test_directedtwocommodityintegralflow_to_ilp_extract_solution() {
         "manually extracted solution should be valid"
     );
 }
+
+#[test]
+fn test_directedtwocommodityintegralflow_to_ilp_bf_vs_ilp() {
+    let problem = feasible_instance();
+    let reduction: ReductionD2CIFToILP = ReduceTo::<ILP<i32>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/disjointconnectingpaths_ilp.rs b/src/unit_tests/rules/disjointconnectingpaths_ilp.rs
index 645e0797..d7aab0c0 100644
--- a/src/unit_tests/rules/disjointconnectingpaths_ilp.rs
+++ b/src/unit_tests/rules/disjointconnectingpaths_ilp.rs
@@ -20,3 +20,13 @@ fn test_disjointconnectingpaths_to_ilp_closed_loop() {
         "DisjointConnectingPaths->ILP closed loop",
     );
 }
+
+#[test]
+fn test_disjointconnectingpaths_to_ilp_bf_vs_ilp() {
+    let source = DisjointConnectingPaths::new(
+        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);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/factoring_ilp.rs b/src/unit_tests/rules/factoring_ilp.rs
index 06f1fd7b..85bc8600 100644
--- a/src/unit_tests/rules/factoring_ilp.rs
+++ b/src/unit_tests/rules/factoring_ilp.rs
@@ -297,3 +297,10 @@ fn test_variable_count_formula() {
         );
     }
 }
+
+#[test]
+fn test_factoring_to_ilp_bf_vs_ilp() {
+    let problem = Factoring::new(2, 2, 6);
+    let reduction: ReductionFactoringToILP = ReduceTo::<ILP<i32>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/hamiltonianpath_ilp.rs b/src/unit_tests/rules/hamiltonianpath_ilp.rs
index bc25df0e..ce36c342 100644
--- a/src/unit_tests/rules/hamiltonianpath_ilp.rs
+++ b/src/unit_tests/rules/hamiltonianpath_ilp.rs
@@ -62,6 +62,13 @@ fn test_hamiltonianpath_to_ilp_cycle_graph() {
     assert_eq!(problem.evaluate(&extracted), Or(true));
 }
 
+#[test]
+fn test_hamiltonianpath_to_ilp_bf_vs_ilp() {
+    let problem = HamiltonianPath::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]));
+    let reduction: ReductionHamiltonianPathToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
+
 #[test]
 fn test_hamiltonianpath_to_ilp_no_path() {
     // Disconnected graph: no Hamiltonian path
diff --git a/src/unit_tests/rules/integralflowbundles_ilp.rs b/src/unit_tests/rules/integralflowbundles_ilp.rs
index 944755ef..6a3268eb 100644
--- a/src/unit_tests/rules/integralflowbundles_ilp.rs
+++ b/src/unit_tests/rules/integralflowbundles_ilp.rs
@@ -111,3 +111,10 @@ fn test_integral_flow_bundles_to_ilp_sink_requirement_constraint() {
     assert_eq!(sink_constraint.rhs, 1.0);
     assert_eq!(sink_constraint.terms, vec![(2, 1.0), (3, 1.0)]);
 }
+
+#[test]
+fn test_integralflowbundles_to_ilp_bf_vs_ilp() {
+    let problem = yes_instance();
+    let reduction: ReductionIFBToILP = ReduceTo::<ILP<i32>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/integralflowhomologousarcs_ilp.rs b/src/unit_tests/rules/integralflowhomologousarcs_ilp.rs
index 2975222a..4ddd5869 100644
--- a/src/unit_tests/rules/integralflowhomologousarcs_ilp.rs
+++ b/src/unit_tests/rules/integralflowhomologousarcs_ilp.rs
@@ -30,3 +30,17 @@ fn test_integralflowhomologousarcs_to_ilp_closed_loop() {
 
     assert!(source.evaluate(&extracted));
 }
+
+#[test]
+fn test_integralflowhomologousarcs_to_ilp_bf_vs_ilp() {
+    let source = IntegralFlowHomologousArcs::new(
+        DirectedGraph::new(4, vec![(0, 1), (0, 2), (1, 3), (2, 3)]),
+        vec![2, 2, 2, 2],
+        0,
+        3,
+        2,
+        vec![(0, 1)],
+    );
+    let reduction = ReduceTo::<ILP<i32>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/integralflowwithmultipliers_ilp.rs b/src/unit_tests/rules/integralflowwithmultipliers_ilp.rs
index 82693d36..35c1b0cb 100644
--- a/src/unit_tests/rules/integralflowwithmultipliers_ilp.rs
+++ b/src/unit_tests/rules/integralflowwithmultipliers_ilp.rs
@@ -29,3 +29,17 @@ fn test_integralflowwithmultipliers_to_ilp_closed_loop() {
 
     assert!(source.evaluate(&extracted));
 }
+
+#[test]
+fn test_integralflowwithmultipliers_to_ilp_bf_vs_ilp() {
+    let source = IntegralFlowWithMultipliers::new(
+        DirectedGraph::new(4, vec![(0, 1), (0, 2), (1, 3), (2, 3)]),
+        0,
+        3,
+        vec![1, 1, 1, 1],
+        vec![2, 2, 2, 2],
+        2,
+    );
+    let reduction = ReduceTo::<ILP<i32>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/lengthboundeddisjointpaths_ilp.rs b/src/unit_tests/rules/lengthboundeddisjointpaths_ilp.rs
index 4f3a2525..20674326 100644
--- a/src/unit_tests/rules/lengthboundeddisjointpaths_ilp.rs
+++ b/src/unit_tests/rules/lengthboundeddisjointpaths_ilp.rs
@@ -20,3 +20,15 @@ fn test_lengthboundeddisjointpaths_to_ilp_closed_loop() {
         "LengthBoundedDisjointPaths->ILP closed loop",
     );
 }
+
+#[test]
+fn test_lengthboundeddisjointpaths_to_ilp_bf_vs_ilp() {
+    let source = LengthBoundedDisjointPaths::new(
+        SimpleGraph::new(4, vec![(0, 1), (0, 2), (1, 3), (2, 3)]),
+        0,
+        3,
+        2,
+    );
+    let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/longestcircuit_ilp.rs b/src/unit_tests/rules/longestcircuit_ilp.rs
index 1f9ae4f9..b0c20b4a 100644
--- a/src/unit_tests/rules/longestcircuit_ilp.rs
+++ b/src/unit_tests/rules/longestcircuit_ilp.rs
@@ -89,3 +89,13 @@ fn test_solution_extraction() {
     let extracted = reduction.extract_solution(&ilp_solution);
     assert!(problem.evaluate(&extracted).0.is_some());
 }
+
+#[test]
+fn test_longestcircuit_to_ilp_bf_vs_ilp() {
+    let problem = LongestCircuit::new(
+        SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]),
+        vec![1, 1, 1],
+    );
+    let reduction: ReductionLongestCircuitToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/longestcommonsubsequence_ilp.rs b/src/unit_tests/rules/longestcommonsubsequence_ilp.rs
index 265926c9..62ecfcc7 100644
--- a/src/unit_tests/rules/longestcommonsubsequence_ilp.rs
+++ b/src/unit_tests/rules/longestcommonsubsequence_ilp.rs
@@ -93,3 +93,10 @@ fn test_lcs_to_ilp_single_position_all_padding() {
     let value = problem.evaluate(&extracted);
     assert_eq!(value, Max(Some(0)));
 }
+
+#[test]
+fn test_longestcommonsubsequence_to_ilp_bf_vs_ilp() {
+    let problem = LongestCommonSubsequence::new(2, vec![vec![0, 1, 0], vec![1, 0, 1]]);
+    let reduction: ReductionLCSToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/longestpath_ilp.rs b/src/unit_tests/rules/longestpath_ilp.rs
index d2aea430..288d5d17 100644
--- a/src/unit_tests/rules/longestpath_ilp.rs
+++ b/src/unit_tests/rules/longestpath_ilp.rs
@@ -106,3 +106,10 @@ fn test_source_equals_target_uses_empty_path() {
     assert_eq!(extracted, vec![0, 0, 0]);
     assert_eq!(problem.evaluate(&extracted), Max(Some(0)));
 }
+
+#[test]
+fn test_longestpath_to_ilp_bf_vs_ilp() {
+    let problem = simple_path_problem();
+    let reduction: ReductionLongestPathToILP = ReduceTo::<ILP<i32>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/maximumclique_ilp.rs b/src/unit_tests/rules/maximumclique_ilp.rs
index ce819c10..21d24c1a 100644
--- a/src/unit_tests/rules/maximumclique_ilp.rs
+++ b/src/unit_tests/rules/maximumclique_ilp.rs
@@ -306,3 +306,13 @@ fn test_star_graph() {
     assert!(is_valid_clique(&problem, &extracted));
     assert_eq!(clique_size(&problem, &extracted), 2);
 }
+
+#[test]
+fn test_maximumclique_to_ilp_bf_vs_ilp() {
+    let problem: MaximumClique<SimpleGraph, i32> = MaximumClique::new(
+        SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]),
+        vec![1; 4],
+    );
+    let reduction: ReductionCliqueToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/maximumindependentset_ilp.rs b/src/unit_tests/rules/maximumindependentset_ilp.rs
index 5d214637..ce3c165c 100644
--- a/src/unit_tests/rules/maximumindependentset_ilp.rs
+++ b/src/unit_tests/rules/maximumindependentset_ilp.rs
@@ -1,7 +1,7 @@
 use crate::models::algebraic::{ObjectiveSense, ILP};
 use crate::models::graph::MaximumIndependentSet;
 use crate::rules::{MinimizeSteps, ReductionChain, ReductionGraph, ReductionPath};
-use crate::solvers::{BruteForce, ILPSolver};
+use crate::solvers::{BruteForce, ILPSolver, Solver};
 use crate::topology::SimpleGraph;
 use crate::traits::Problem;
 use crate::types::{Max, ProblemSize};
@@ -62,15 +62,11 @@ fn test_maximumindependentset_to_ilp_via_path_closed_loop() {
     let (_, chain) = reduce_mis_to_ilp(&problem);
     let ilp: &ILP<bool> = chain.target_problem();
 
-    let bf = BruteForce::new();
     let ilp_solver = ILPSolver::new();
-    let bf_solutions = bf.find_all_witnesses(&problem);
     let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be solvable");
     let extracted = chain.extract_solution(&ilp_solution);
 
-    let bf_size: usize = bf_solutions[0].iter().sum();
     let ilp_size: usize = extracted.iter().sum();
-    assert_eq!(bf_size, 2);
     assert_eq!(ilp_size, 2);
     assert!(problem.evaluate(&extracted).is_valid());
 }
@@ -89,3 +85,17 @@ fn test_maximumindependentset_to_ilp_via_path_weighted() {
     assert_eq!(problem.evaluate(&extracted), Max(Some(100)));
     assert_eq!(extracted, vec![0, 1, 0]);
 }
+
+#[test]
+fn test_maximumindependentset_to_ilp_bf_vs_ilp() {
+    let problem = MaximumIndependentSet::new(
+        SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]),
+        vec![1i32; 4],
+    );
+    let (_, chain) = reduce_mis_to_ilp(&problem);
+    let ilp: &ILP<bool> = chain.target_problem();
+    let bf_value = BruteForce::new().solve(&problem);
+    let ilp_solution = ILPSolver::new().solve(ilp).expect("ILP should be solvable");
+    let extracted = chain.extract_solution(&ilp_solution);
+    assert_eq!(problem.evaluate(&extracted), bf_value);
+}
diff --git a/src/unit_tests/rules/maximummatching_ilp.rs b/src/unit_tests/rules/maximummatching_ilp.rs
index dab0c168..02c9c606 100644
--- a/src/unit_tests/rules/maximummatching_ilp.rs
+++ b/src/unit_tests/rules/maximummatching_ilp.rs
@@ -248,3 +248,11 @@ fn test_solve_reduced() {
     assert!(problem.evaluate(&solution).is_valid());
     assert_eq!(problem.evaluate(&solution), Max(Some(2)));
 }
+
+#[test]
+fn test_maximummatching_to_ilp_bf_vs_ilp() {
+    let problem =
+        MaximumMatching::<_, i32>::unit_weights(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]));
+    let reduction: ReductionMatchingToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/maximumsetpacking_ilp.rs b/src/unit_tests/rules/maximumsetpacking_ilp.rs
index ca288083..54daaed0 100644
--- a/src/unit_tests/rules/maximumsetpacking_ilp.rs
+++ b/src/unit_tests/rules/maximumsetpacking_ilp.rs
@@ -127,3 +127,10 @@ fn test_solve_reduced() {
     assert!(problem.evaluate(&solution).is_valid());
     assert_eq!(problem.evaluate(&solution), Max(Some(2)));
 }
+
+#[test]
+fn test_maximumsetpacking_to_ilp_bf_vs_ilp() {
+    let problem = MaximumSetPacking::<i32>::new(vec![vec![0, 1], vec![1, 2], vec![2, 3]]);
+    let reduction: ReductionSPToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/minimumcutintoboundedsets_ilp.rs b/src/unit_tests/rules/minimumcutintoboundedsets_ilp.rs
index 718693d1..1dbe73c4 100644
--- a/src/unit_tests/rules/minimumcutintoboundedsets_ilp.rs
+++ b/src/unit_tests/rules/minimumcutintoboundedsets_ilp.rs
@@ -66,3 +66,10 @@ fn test_larger_instance() {
         "MinCutBS larger instance",
     );
 }
+
+#[test]
+fn test_minimumcutintoboundedsets_to_ilp_bf_vs_ilp() {
+    let source = small_instance();
+    let reduction: ReductionMinCutBSToILP = ReduceTo::<ILP<bool>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/minimumdominatingset_ilp.rs b/src/unit_tests/rules/minimumdominatingset_ilp.rs
index 073c304c..42c4f403 100644
--- a/src/unit_tests/rules/minimumdominatingset_ilp.rs
+++ b/src/unit_tests/rules/minimumdominatingset_ilp.rs
@@ -241,3 +241,13 @@ fn test_cycle_graph() {
 
     assert!(problem.evaluate(&extracted).is_valid());
 }
+
+#[test]
+fn test_minimumdominatingset_to_ilp_bf_vs_ilp() {
+    let problem = MinimumDominatingSet::new(
+        SimpleGraph::new(4, vec![(0, 1), (0, 2), (0, 3)]),
+        vec![1i32; 4],
+    );
+    let reduction: ReductionDSToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/minimumfeedbackvertexset_ilp.rs b/src/unit_tests/rules/minimumfeedbackvertexset_ilp.rs
index 762157e7..74f12365 100644
--- a/src/unit_tests/rules/minimumfeedbackvertexset_ilp.rs
+++ b/src/unit_tests/rules/minimumfeedbackvertexset_ilp.rs
@@ -193,3 +193,11 @@ fn test_solution_extraction() {
     // Verify this is a valid FVS (removing vertex 0 breaks the 3-cycle)
     assert!(problem.evaluate(&extracted).is_valid());
 }
+
+#[test]
+fn test_minimumfeedbackvertexset_to_ilp_bf_vs_ilp() {
+    let graph = DirectedGraph::new(3, vec![(0, 1), (1, 2), (2, 0)]);
+    let problem = MinimumFeedbackVertexSet::new(graph, vec![1i32; 3]);
+    let reduction: ReductionMFVSToILP = ReduceTo::<ILP<i32>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/minimummultiwaycut_ilp.rs b/src/unit_tests/rules/minimummultiwaycut_ilp.rs
index 4ed31f8b..99260a2a 100644
--- a/src/unit_tests/rules/minimummultiwaycut_ilp.rs
+++ b/src/unit_tests/rules/minimummultiwaycut_ilp.rs
@@ -137,3 +137,10 @@ fn test_solve_reduced() {
     assert!(problem.evaluate(&solution).is_valid());
     assert_eq!(problem.evaluate(&solution), Min(Some(8)));
 }
+
+#[test]
+fn test_minimummultiwaycut_to_ilp_bf_vs_ilp() {
+    let problem = canonical_instance();
+    let reduction: ReductionMMCToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/minimumsetcovering_ilp.rs b/src/unit_tests/rules/minimumsetcovering_ilp.rs
index eda04570..cd16428a 100644
--- a/src/unit_tests/rules/minimumsetcovering_ilp.rs
+++ b/src/unit_tests/rules/minimumsetcovering_ilp.rs
@@ -225,3 +225,10 @@ fn test_constraint_structure() {
     assert!(!vars2.contains(&1));
     assert!(vars2.contains(&2));
 }
+
+#[test]
+fn test_minimumsetcovering_to_ilp_bf_vs_ilp() {
+    let problem = MinimumSetCovering::<i32>::new(3, vec![vec![0, 1], vec![1, 2], vec![0, 2]]);
+    let reduction: ReductionSCToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/minimumvertexcover_ilp.rs b/src/unit_tests/rules/minimumvertexcover_ilp.rs
index 57f47c50..736072a6 100644
--- a/src/unit_tests/rules/minimumvertexcover_ilp.rs
+++ b/src/unit_tests/rules/minimumvertexcover_ilp.rs
@@ -59,15 +59,11 @@ fn test_minimumvertexcover_to_ilp_via_path_closed_loop() {
     let (_, chain) = reduce_vc_to_ilp(&problem);
     let ilp: &ILP<bool> = chain.target_problem();
 
-    let bf = BruteForce::new();
     let ilp_solver = ILPSolver::new();
-    let bf_solutions = bf.find_all_witnesses(&problem);
     let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be solvable");
     let extracted = chain.extract_solution(&ilp_solution);
 
-    let bf_size: usize = bf_solutions[0].iter().sum();
     let ilp_size: usize = extracted.iter().sum();
-    assert_eq!(bf_size, 2);
     assert_eq!(ilp_size, 2);
     assert!(problem.evaluate(&extracted).is_valid());
 }
@@ -86,3 +82,18 @@ fn test_minimumvertexcover_to_ilp_via_path_weighted() {
     assert_eq!(problem.evaluate(&extracted), Min(Some(1)));
     assert_eq!(extracted, vec![0, 1, 0]);
 }
+
+#[test]
+fn test_minimumvertexcover_to_ilp_bf_vs_ilp() {
+    let problem = MinimumVertexCover::new(
+        SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]),
+        vec![1i32; 4],
+    );
+    let (_, chain) = reduce_vc_to_ilp(&problem);
+    let ilp: &ILP<bool> = chain.target_problem();
+    let bf_solutions = BruteForce::new().find_all_witnesses(&problem);
+    let bf_value = problem.evaluate(&bf_solutions[0]);
+    let ilp_solution = ILPSolver::new().solve(ilp).expect("ILP should be solvable");
+    let extracted = chain.extract_solution(&ilp_solution);
+    assert_eq!(problem.evaluate(&extracted), bf_value);
+}
diff --git a/src/unit_tests/rules/optimallineararrangement_ilp.rs b/src/unit_tests/rules/optimallineararrangement_ilp.rs
index 2e92b517..661b5056 100644
--- a/src/unit_tests/rules/optimallineararrangement_ilp.rs
+++ b/src/unit_tests/rules/optimallineararrangement_ilp.rs
@@ -64,36 +64,20 @@ fn test_optimallineararrangement_to_ilp_with_chords() {
 }
 
 #[test]
-fn test_optimallineararrangement_to_ilp_optimization() {
-    // Path P4: optimal cost is 3
+fn test_solution_extraction() {
     let problem = OptimalLinearArrangement::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]));
     let reduction: ReductionOLAToILP = ReduceTo::<ILP<i32>>::reduce_to(&problem);
-
-    // Cannot brute-force ILP<i32> (integer domain too large), so compare BF source vs ILP solver
-    let bf = BruteForce::new();
-    use crate::Solver;
-    let bf_value = bf.solve(&problem);
-
     let ilp_solver = ILPSolver::new();
     let ilp_solution = ilp_solver
         .solve(reduction.target_problem())
-        .expect("ILP should be solvable");
+        .expect("solvable");
     let extracted = reduction.extract_solution(&ilp_solution);
-    let ilp_value = problem.evaluate(&extracted);
-    assert_eq!(
-        bf_value, ilp_value,
-        "BF and ILP should agree on optimal value"
-    );
+    assert!(problem.evaluate(&extracted).0.is_some());
 }
 
 #[test]
-fn test_solution_extraction() {
+fn test_optimallineararrangement_to_ilp_bf_vs_ilp() {
     let problem = OptimalLinearArrangement::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]));
     let reduction: ReductionOLAToILP = ReduceTo::<ILP<i32>>::reduce_to(&problem);
-    let ilp_solver = ILPSolver::new();
-    let ilp_solution = ilp_solver
-        .solve(reduction.target_problem())
-        .expect("solvable");
-    let extracted = reduction.extract_solution(&ilp_solution);
-    assert!(problem.evaluate(&extracted).0.is_some());
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
 }
diff --git a/src/unit_tests/rules/pathconstrainednetworkflow_ilp.rs b/src/unit_tests/rules/pathconstrainednetworkflow_ilp.rs
index 98757b34..a6f97132 100644
--- a/src/unit_tests/rules/pathconstrainednetworkflow_ilp.rs
+++ b/src/unit_tests/rules/pathconstrainednetworkflow_ilp.rs
@@ -29,3 +29,17 @@ fn test_pathconstrainednetworkflow_to_ilp_closed_loop() {
 
     assert!(source.evaluate(&extracted));
 }
+
+#[test]
+fn test_pathconstrainednetworkflow_to_ilp_bf_vs_ilp() {
+    let source = PathConstrainedNetworkFlow::new(
+        DirectedGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]),
+        vec![1, 1, 1],
+        0,
+        2,
+        vec![vec![0, 1], vec![2]],
+        2,
+    );
+    let reduction = ReduceTo::<ILP<i32>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/precedenceconstrainedscheduling_ilp.rs b/src/unit_tests/rules/precedenceconstrainedscheduling_ilp.rs
index b92d00f3..4f4e3a36 100644
--- a/src/unit_tests/rules/precedenceconstrainedscheduling_ilp.rs
+++ b/src/unit_tests/rules/precedenceconstrainedscheduling_ilp.rs
@@ -77,3 +77,10 @@ fn test_precedenceconstrainedscheduling_to_ilp_extract_solution() {
         "manually constructed solution should be valid"
     );
 }
+
+#[test]
+fn test_precedenceconstrainedscheduling_to_ilp_bf_vs_ilp() {
+    let problem = feasible_instance();
+    let reduction: ReductionPCSToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/quadraticassignment_ilp.rs b/src/unit_tests/rules/quadraticassignment_ilp.rs
index fd0bade7..d7a648d0 100644
--- a/src/unit_tests/rules/quadraticassignment_ilp.rs
+++ b/src/unit_tests/rules/quadraticassignment_ilp.rs
@@ -105,3 +105,10 @@ fn test_quadraticassignment_to_ilp_rectangular() {
     assert!(ilp_value.is_valid());
     assert_eq!(ilp_value, bf_value);
 }
+
+#[test]
+fn test_quadraticassignment_to_ilp_bf_vs_ilp() {
+    let problem = small_qap();
+    let reduction: ReductionQAPToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/ruralpostman_ilp.rs b/src/unit_tests/rules/ruralpostman_ilp.rs
index e2d2a525..8798cd6e 100644
--- a/src/unit_tests/rules/ruralpostman_ilp.rs
+++ b/src/unit_tests/rules/ruralpostman_ilp.rs
@@ -56,3 +56,14 @@ fn test_ruralpostman_to_ilp_optimization() {
         "ILP optimum must match brute-force optimum"
     );
 }
+
+#[test]
+fn test_ruralpostman_to_ilp_bf_vs_ilp() {
+    let source = RuralPostman::new(
+        SimpleGraph::new(3, vec![(0, 1), (1, 2), (0, 2)]),
+        vec![1, 1, 1],
+        vec![0],
+    );
+    let reduction = ReduceTo::<ILP<i32>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/schedulingwithindividualdeadlines_ilp.rs b/src/unit_tests/rules/schedulingwithindividualdeadlines_ilp.rs
index 884ee8c4..569da137 100644
--- a/src/unit_tests/rules/schedulingwithindividualdeadlines_ilp.rs
+++ b/src/unit_tests/rules/schedulingwithindividualdeadlines_ilp.rs
@@ -78,3 +78,10 @@ fn test_schedulingwithindividualdeadlines_to_ilp_extract_solution() {
         "manually constructed solution is valid"
     );
 }
+
+#[test]
+fn test_schedulingwithindividualdeadlines_to_ilp_bf_vs_ilp() {
+    let problem = feasible_instance();
+    let reduction: ReductionSWIDToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/sequencingtominimizeweightedcompletiontime_ilp.rs b/src/unit_tests/rules/sequencingtominimizeweightedcompletiontime_ilp.rs
index 3f39efa5..5f599cb0 100644
--- a/src/unit_tests/rules/sequencingtominimizeweightedcompletiontime_ilp.rs
+++ b/src/unit_tests/rules/sequencingtominimizeweightedcompletiontime_ilp.rs
@@ -157,3 +157,10 @@ fn test_solve_reduced_matches_source_optimum() {
     assert_eq!(source_solution, vec![1, 2, 0, 1, 0]);
     assert_eq!(problem.evaluate(&source_solution), Min(Some(46)));
 }
+
+#[test]
+fn test_sequencingtominimizeweightedcompletiontime_to_ilp_bf_vs_ilp() {
+    let problem = SequencingToMinimizeWeightedCompletionTime::new(vec![2, 1], vec![3, 5], vec![]);
+    let reduction: ReductionSTMWCTToILP = ReduceTo::<ILP<i32>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/sequencingwithinintervals_ilp.rs b/src/unit_tests/rules/sequencingwithinintervals_ilp.rs
index 767c24a9..fa04ef22 100644
--- a/src/unit_tests/rules/sequencingwithinintervals_ilp.rs
+++ b/src/unit_tests/rules/sequencingwithinintervals_ilp.rs
@@ -89,3 +89,10 @@ fn test_sequencingwithinintervals_to_ilp_extract_solution() {
         "manually constructed solution is valid"
     );
 }
+
+#[test]
+fn test_sequencingwithinintervals_to_ilp_bf_vs_ilp() {
+    let problem = feasible_instance();
+    let reduction: ReductionSWIToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/stackercrane_ilp.rs b/src/unit_tests/rules/stackercrane_ilp.rs
index ca7e7d1a..d4d6ff22 100644
--- a/src/unit_tests/rules/stackercrane_ilp.rs
+++ b/src/unit_tests/rules/stackercrane_ilp.rs
@@ -14,3 +14,10 @@ fn test_stackercrane_to_ilp_closed_loop() {
         "StackerCrane->ILP closed loop",
     );
 }
+
+#[test]
+fn test_stackercrane_to_ilp_bf_vs_ilp() {
+    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);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/steinertree_ilp.rs b/src/unit_tests/rules/steinertree_ilp.rs
index 24a7436a..7925f7ed 100644
--- a/src/unit_tests/rules/steinertree_ilp.rs
+++ b/src/unit_tests/rules/steinertree_ilp.rs
@@ -95,3 +95,10 @@ fn test_reduction_rejects_zero_weights() {
     let problem = SteinerTree::new(graph, vec![0, 0, 0], vec![0, 1]);
     let _ = ReduceTo::<ILP<bool>>::reduce_to(&problem);
 }
+
+#[test]
+fn test_steinertree_to_ilp_bf_vs_ilp() {
+    let problem = canonical_instance();
+    let reduction: ReductionSteinerTreeToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/steinertreeingraphs_ilp.rs b/src/unit_tests/rules/steinertreeingraphs_ilp.rs
index 7f07c540..397b9a48 100644
--- a/src/unit_tests/rules/steinertreeingraphs_ilp.rs
+++ b/src/unit_tests/rules/steinertreeingraphs_ilp.rs
@@ -21,3 +21,14 @@ fn test_steinertreeingraphs_to_ilp_closed_loop() {
         "SteinerTreeInGraphs->ILP closed loop",
     );
 }
+
+#[test]
+fn test_steinertreeingraphs_to_ilp_bf_vs_ilp() {
+    let source = SteinerTreeInGraphs::new(
+        SimpleGraph::new(3, vec![(0, 1), (1, 2)]),
+        vec![0, 2],
+        vec![1, 1],
+    );
+    let reduction = ReduceTo::<ILP<bool>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/strongconnectivityaugmentation_ilp.rs b/src/unit_tests/rules/strongconnectivityaugmentation_ilp.rs
index cb765f5c..924fcc0e 100644
--- a/src/unit_tests/rules/strongconnectivityaugmentation_ilp.rs
+++ b/src/unit_tests/rules/strongconnectivityaugmentation_ilp.rs
@@ -92,3 +92,10 @@ fn test_infeasible_budget() {
     let solver = ILPSolver::new();
     assert!(solver.solve(ilp).is_none());
 }
+
+#[test]
+fn test_strongconnectivityaugmentation_to_ilp_bf_vs_ilp() {
+    let source = small_instance();
+    let reduction: ReductionSCAToILP = ReduceTo::<ILP<i32>>::reduce_to(&source);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&source, &reduction);
+}
diff --git a/src/unit_tests/rules/subgraphisomorphism_ilp.rs b/src/unit_tests/rules/subgraphisomorphism_ilp.rs
index ffab5916..a662292f 100644
--- a/src/unit_tests/rules/subgraphisomorphism_ilp.rs
+++ b/src/unit_tests/rules/subgraphisomorphism_ilp.rs
@@ -94,3 +94,12 @@ fn test_solution_extraction() {
     let extracted = reduction.extract_solution(&ilp_solution);
     assert_eq!(problem.evaluate(&extracted), Or(true));
 }
+
+#[test]
+fn test_subgraphisomorphism_to_ilp_bf_vs_ilp() {
+    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 problem = SubgraphIsomorphism::new(host, pattern);
+    let reduction: ReductionSubIsoToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/travelingsalesman_ilp.rs b/src/unit_tests/rules/travelingsalesman_ilp.rs
index c81a477f..cb004003 100644
--- a/src/unit_tests/rules/travelingsalesman_ilp.rs
+++ b/src/unit_tests/rules/travelingsalesman_ilp.rs
@@ -147,3 +147,13 @@ fn test_solve_reduced() {
     let bf_solutions = bf.find_all_witnesses(&problem);
     assert_eq!(metric, problem.evaluate(&bf_solutions[0]));
 }
+
+#[test]
+fn test_travelingsalesman_to_ilp_bf_vs_ilp() {
+    let problem = TravelingSalesman::<_, i32>::unit_weights(SimpleGraph::new(
+        4,
+        vec![(0, 1), (1, 2), (2, 3), (3, 0)],
+    ));
+    let reduction: ReductionTSPToILP = ReduceTo::<ILP<bool>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/undirectedflowlowerbounds_ilp.rs b/src/unit_tests/rules/undirectedflowlowerbounds_ilp.rs
index 38a0a3c3..2969919d 100644
--- a/src/unit_tests/rules/undirectedflowlowerbounds_ilp.rs
+++ b/src/unit_tests/rules/undirectedflowlowerbounds_ilp.rs
@@ -94,3 +94,10 @@ fn test_undirectedflowlowerbounds_to_ilp_extract_solution() {
         "manually extracted orientation should be valid"
     );
 }
+
+#[test]
+fn test_undirectedflowlowerbounds_to_ilp_bf_vs_ilp() {
+    let problem = feasible_instance();
+    let reduction: ReductionUFLBToILP = ReduceTo::<ILP<i32>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}
diff --git a/src/unit_tests/rules/undirectedtwocommodityintegralflow_ilp.rs b/src/unit_tests/rules/undirectedtwocommodityintegralflow_ilp.rs
index 1968700f..398f8c48 100644
--- a/src/unit_tests/rules/undirectedtwocommodityintegralflow_ilp.rs
+++ b/src/unit_tests/rules/undirectedtwocommodityintegralflow_ilp.rs
@@ -129,3 +129,10 @@ fn test_undirectedtwocommodityintegralflow_to_ilp_extract_solution() {
         "manually extracted solution should be valid"
     );
 }
+
+#[test]
+fn test_undirectedtwocommodityintegralflow_to_ilp_bf_vs_ilp() {
+    let problem = feasible_instance();
+    let reduction: ReductionU2CIFToILP = ReduceTo::<ILP<i32>>::reduce_to(&problem);
+    crate::rules::test_helpers::assert_bf_vs_ilp(&problem, &reduction);
+}