From f16ad3c5e0a86e4f919bdb154798444ac89d99a3 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Mon, 2 Nov 2026 00:29:23 -0800 Subject: [PATCH 1/2] Add ThreeDimensionalMatching to ExactCoverBy3Sets reduction (#1103) Map each triple (w, x, y) to the subset {w, q + x, 2q + y} of the tagged disjoint union {0, ..., 3q-1}; the selection vector is shared, so extraction is the identity after validating the target witness. Exact transform: universe_size = 3 * universe_size, num_subsets = num_triples. Includes the canonical example, unit tests and the paper entry. --- docs/paper/reductions.typ | 49 ++++ src/models/set/exact_cover_by_3_sets.rs | 3 +- src/rules/mod.rs | 2 + ...eedimensionalmatching_exactcoverby3sets.rs | 100 +++++++ ...eedimensionalmatching_exactcoverby3sets.rs | 243 ++++++++++++++++++ 5 files changed, 396 insertions(+), 1 deletion(-) create mode 100644 src/rules/threedimensionalmatching_exactcoverby3sets.rs create mode 100644 src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 8e0462b7a..4f2551111 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -19847,6 +19847,55 @@ The following table shows concrete target-variable counts for example instances, _Solution extraction._ Return the ILP solution vector directly: $x_l = 1$ iff triple $m_l$ is selected. ] +#let tdm_x3c = load-example("ThreeDimensionalMatching", "ExactCoverBy3Sets") +#let tdm_x3c_sol = tdm_x3c.solutions.at(0) +#reduction-rule("ThreeDimensionalMatching", "ExactCoverBy3Sets", + example: true, + example-caption: [$q = #tdm_x3c.source.instance.universe_size$, $t = #tdm_x3c.source.instance.triples.len()$ triples $arrow.r$ #tdm_x3c.target.instance.subsets.len() subsets over $3q = #tdm_x3c.target.instance.universe_size$ elements], + extra: [ + #pred-commands( + "pred create --example " + rule-spec(tdm_x3c) + " -o three-dimensional-matching.json", + "pred reduce three-dimensional-matching.json --via route.json -o bundle.json", + "pred solve bundle.json", + "pred evaluate three-dimensional-matching.json --config " + cli-config(tdm_x3c_sol.source_config), + ) + + #{ + let q = tdm_x3c.source.instance.universe_size + let triples = tdm_x3c.source.instance.triples + let subsets = tdm_x3c.target.instance.subsets + let selected = tdm_x3c_sol.source_config.enumerate().filter(((i, x)) => x).map(((i, x)) => i) + [ + *Step 1 -- Source instance.* The canonical source has $q = #q$ and $t = #triples.len()$ triples: #triples.map(tr => "(" + fmt-values(tr) + ")").join(", "). + + *Step 2 -- Tag the coordinates.* The target universe is ${0, dots, #(3 * q - 1)}$: $W$ occupies $0, dots, #(q - 1)$, $X$ occupies $#q, dots, #(2 * q - 1)$ and $Y$ occupies $#(2 * q), dots, #(3 * q - 1)$. Triple $(w, x, y)$ becomes ${w, #q + x, #(2 * q) + y}$, giving the subsets #subsets.enumerate().map(((i, s)) => $S_#i = {#fmt-values(s)}$).join(", "). + + *Step 3 -- Verify the witness.* The configuration $(#fmt-values(tdm_x3c_sol.target_config))$ selects #selected.map(i => $S_#i$).join(", "), which are pairwise disjoint and cover all $#(3 * q)$ elements #sym.checkmark. The identical source configuration selects the diagonal triples, a perfect matching #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical witness, and it is the only exact cover: element $#(q - 1)$ ($w = #(q - 1)$) lies only in $S_2$, element $#q$ ($x = 0$) only in $S_0$, and element $#(2 * q + 1)$ ($y = 1$) only in $S_1$, so every exact cover contains $S_0, S_1, S_2$, which already cover $U$. The cross subsets $S_3$ and $S_4$ are disjoint, but no third subset completes them. + ] + } + ], +)[ + Karp's 3DM and X3C @karp1972 @garey1979 are related by tagging: the three coordinate domains $W = X = Y = {0, dots, q - 1}$ become the disjoint blocks of a $3q$-element universe, and each triple becomes one 3-element subset. The target has $3q$ elements and $t$ subsets, and the selection vector is unchanged. +][ + _Construction._ Let the source have universe size $q$ and triples $m_l = (a_l, b_l, c_l)$ for $l = 0, dots, t - 1$, with $a_l, b_l, c_l in {0, dots, q - 1}$. Set $U = {0, dots, 3q - 1}$ and $S_l = {a_l, q + b_l, 2q + c_l}$. Since $a_l < q <= q + b_l < 2q <= 2q + c_l < 3q$, each $S_l$ has three distinct elements of $U$, even when $a_l$, $b_l$, $c_l$ are numerically equal, and $|U|$ is divisible by 3; so $(U, (S_0, dots, S_(t-1)))$ is a valid X3C instance. Duplicate triples give duplicate subsets at their own positions. + + The map $tau(d, v) = d q + v$ from tagged coordinates (domain $d in {0, 1, 2}$, value $v < q$) to $U$ is a bijection, and $S_l = tau({(0, a_l), (1, b_l), (2, c_l)})$. + + _Correctness._ Fix a selection $J subset.eq {0, dots, t - 1}$. + + ($arrow.r.double$) Suppose ${m_l : l in J}$ is a perfect matching: $|J| = q$ and no two selected triples share a coordinate in any domain. If two selected subsets $S_l, S_k$ shared an element $u$, then $u = tau(d, v)$ for a unique $(d, v)$, so both triples would have value $v$ in domain $d$, a contradiction; the selected subsets are pairwise disjoint. Their union then has $3q = |U|$ elements, so it is $U$, and $J$ is an exact cover. + + ($arrow.l.double$) Suppose ${S_l : l in J}$ is an exact cover: $|J| = q$ and every element of $U$ lies in exactly one selected subset. If two selected triples agreed in domain $d$ with value $v$, both subsets would contain $tau(d, v)$, contradicting disjointness. So $|J| = q$ and no coordinate repeats: $J$ selects a perfect matching. + + Both problems also reject a selection whose length differs from $t$, so the two instances have exactly the same solution vectors. + + _Solution extraction._ Return the target selection vector unchanged after checking that it is an exact cover. + + _NO example._ Take $q = 3$ and the five triples $(0, 0, 0)$, $(1, 1, 1)$, $(2, 1, 2)$, $(2, 0, 2)$, $(1, 0, 1)$. The construction gives $U = {0, dots, 8}$ and the subsets ${0, 3, 6}$, ${1, 4, 7}$, ${2, 4, 8}$, ${2, 3, 8}$, ${1, 3, 7}$. On the source side, the $X$-value $2$ occurs in no triple; any $3$ selected triples with pairwise distinct $X$-values would have to use all of $0, 1, 2$, so no selection is a perfect matching. On the target side, the tagged element $q + 2 = 5$ lies in no subset, so no selection covers $U$ and no exact cover exists. Both instances therefore have no solution, as the correctness argument requires. +] + #let tdm_mwd = load-example("ThreeDimensionalMatching", "MinimumWeightDecoding") #let tdm_mwd_sol = tdm_mwd.solutions.at(0) #reduction-rule("ThreeDimensionalMatching", "MinimumWeightDecoding", diff --git a/src/models/set/exact_cover_by_3_sets.rs b/src/models/set/exact_cover_by_3_sets.rs index aac527cb3..9363229f1 100644 --- a/src/models/set/exact_cover_by_3_sets.rs +++ b/src/models/set/exact_cover_by_3_sets.rs @@ -86,7 +86,8 @@ impl ExactCoverBy3Sets { Self::try_new(universe_size, subsets).unwrap_or_else(|error| panic!("{error}")) } - fn try_new( + /// Fallible constructor shared by [`Self::new`], serde, and reductions. + pub(crate) fn try_new( universe_size: usize, mut subsets: Vec<[usize; 3]>, ) -> Result { diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 7606f4923..8b3e7bdf0 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -181,6 +181,7 @@ pub(crate) mod test_helpers; #[cfg(test)] #[path = "../unit_tests/rules/aggregate_contracts.rs"] mod aggregate_contracts; +pub(crate) mod threedimensionalmatching_exactcoverby3sets; pub(crate) mod threedimensionalmatching_minimumweightdecoding; pub(crate) mod threedimensionalmatching_threepartition; pub(crate) mod threepartition_resourceconstrainedscheduling; @@ -466,6 +467,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec &Self::Target { + &self.target + } + + /// Target subset `i` is the tagged image of source triple `i`, so an exact + /// cover selects exactly the triples of a perfect matching. + fn extract_solution( + &self, + target_solution: &::Solution, + ) -> crate::rules::ExtractionResult<::Solution> { + crate::rules::traits::validate_target_witness( + self.target_problem(), + target_solution, + |value| value.0, + "target witness is not an exact cover", + )?; + + Ok(target_solution.clone()) + } +} + +#[crate::aggregate_reduction(identity)] +impl crate::rules::AggregateReductionResult + for ReductionThreeDimensionalMatchingToExactCoverBy3Sets +{ +} + +#[reduction(transform = exact { + universe_size = "3 * universe_size", + num_subsets = "num_triples", +})] +impl ReduceTo for ThreeDimensionalMatching { + type Result = ReductionThreeDimensionalMatchingToExactCoverBy3Sets; + + fn reduce_to(&self) -> Result { + let q = self.universe_size(); + let target_universe_size = q.checked_mul(3).ok_or_else(|| { + crate::rules::ReductionError::integer_overflow::( + "computing the tagged universe size 3 * universe_size", + ) + })?; + // Every coordinate is below q, so each tagged element is below 3q and + // the additions cannot overflow once 3q fits in usize. + let subsets = self + .triples() + .iter() + .map(|&(w, x, y)| [w, q + x, 2 * q + y]) + .collect(); + let target = ExactCoverBy3Sets::try_new(target_universe_size, subsets) + .map_err(>::target_construction)?; + + Ok(ReductionThreeDimensionalMatchingToExactCoverBy3Sets { target }) + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "threedimensionalmatching_to_exactcoverby3sets", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, ExactCoverBy3Sets>( + ThreeDimensionalMatching::new( + 3, + vec![(0, 0, 0), (1, 1, 1), (2, 2, 2), (0, 1, 2), (1, 2, 0)], + ), + SolutionPair { + source_config: serde_json::json!(vec![true, true, true, false, false]), + target_config: serde_json::json!(vec![true, true, true, false, false]), + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs"] +mod tests; diff --git a/src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs b/src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs new file mode 100644 index 000000000..8b3a64e1e --- /dev/null +++ b/src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs @@ -0,0 +1,243 @@ +use super::*; +use crate::rules::ReductionError; +use crate::rules::test_helpers::{ + assert_parameter_predictions, assert_satisfaction_round_trip_from_satisfaction_target, +}; +use crate::solvers::BruteForce; +use crate::traits::Problem; +use crate::types::Or; + +fn reduce( + source: &ThreeDimensionalMatching, +) -> ReductionThreeDimensionalMatchingToExactCoverBy3Sets { + ReduceTo::::reduce_to(source).expect("reduction should succeed") +} + +/// Every selection vector of length `n`, in lexicographic bit order. +fn all_configs(n: usize) -> impl Iterator> { + (0..1usize << n).map(move |bits| (0..n).map(|i| bits >> i & 1 == 1).collect()) +} + +/// The source and target agree on every selection vector, and every target +/// exact cover extracts to itself. +fn assert_identical_feasibility(source: &ThreeDimensionalMatching) { + let reduction = reduce(source); + let target = reduction.target_problem(); + assert_parameter_predictions(source, &reduction); + for config in all_configs(source.num_triples()) { + let source_value = source.evaluate(&config).unwrap(); + assert_eq!( + source_value, + target.evaluate(&config).unwrap(), + "triples {:?}, config {config:?}", + source.triples() + ); + match reduction.extract_solution(&config) { + Ok(extracted) => { + assert!(source_value.0); + assert_eq!(extracted, config); + } + Err(_) => assert!(!source_value.0), + } + } +} + +#[test] +fn test_threedimensionalmatching_to_exactcoverby3sets_closed_loop() { + // The issue's example: the diagonal is the unique perfect matching. + let source = ThreeDimensionalMatching::new( + 3, + vec![(0, 0, 0), (1, 1, 1), (2, 2, 2), (0, 1, 2), (1, 2, 0)], + ); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(target.universe_size(), 9); + assert_eq!( + target.subsets(), + &[[0, 3, 6], [1, 4, 7], [2, 5, 8], [0, 4, 8], [1, 5, 6]] + ); + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "ThreeDimensionalMatching -> ExactCoverBy3Sets closed loop", + ); + + let covers = BruteForce::new().find_all_witnesses(target).unwrap(); + assert_eq!(covers, vec![vec![true, true, true, false, false]]); + assert_eq!( + reduction.extract_solution(&covers[0]).unwrap(), + vec![true, true, true, false, false] + ); + // The two cross triples are disjoint but cannot be completed. + let partial = vec![false, false, false, true, true]; + assert_eq!(target.evaluate(&partial).unwrap(), Or(false)); + assert!(reduction.extract_solution(&partial).is_err()); + assert_identical_feasibility(&source); +} + +#[test] +fn test_threedimensionalmatching_to_exactcoverby3sets_every_family_q2() { + // All 8 triples over {0,1}^3; each of the 256 families is checked on every + // selection vector, so witness sets agree exactly. + let all_triples: Vec<(usize, usize, usize)> = (0..8) + .map(|t| (t & 1, (t >> 1) & 1, (t >> 2) & 1)) + .collect(); + let mut feasible_families = 0; + for family in 0..1usize << all_triples.len() { + let triples: Vec<_> = (0..all_triples.len()) + .filter(|&i| family >> i & 1 == 1) + .map(|i| all_triples[i]) + .collect(); + let source = ThreeDimensionalMatching::new(2, triples); + assert_identical_feasibility(&source); + + let source_witnesses = BruteForce::new().find_all_witnesses(&source).unwrap(); + let reduction = reduce(&source); + let target_witnesses = BruteForce::new() + .find_all_witnesses(reduction.target_problem()) + .unwrap(); + assert_eq!(source_witnesses, target_witnesses); + feasible_families += usize::from(!source_witnesses.is_empty()); + } + // The perfect matchings are the 4 disjoint pairs {(0,a,b), (1,1-a,1-b)}, + // which partition the 8 triples. A family is infeasible iff it misses at + // least one triple of every pair: 3^4 = 81 families. + assert_eq!(feasible_families, 256 - 81); +} + +#[test] +fn test_threedimensionalmatching_to_exactcoverby3sets_empty() { + let source = ThreeDimensionalMatching::new(0, vec![]); + let reduction = reduce(&source); + let target = reduction.target_problem(); + assert_eq!(target.universe_size(), 0); + assert_eq!(target.num_subsets(), 0); + assert_eq!(target.evaluate(&vec![]).unwrap(), Or(true)); + assert_eq!( + reduction.extract_solution(&vec![]).unwrap(), + Vec::::new() + ); + assert_identical_feasibility(&source); +} + +#[test] +fn test_threedimensionalmatching_to_exactcoverby3sets_duplicate_triples() { + let source = ThreeDimensionalMatching::new(2, vec![(0, 1, 0), (0, 1, 0), (1, 0, 1)]); + let reduction = reduce(&source); + assert_eq!( + reduction.target_problem().subsets(), + &[[0, 3, 4], [0, 3, 4], [1, 2, 5]] + ); + // Selecting both copies reuses every element. + assert_eq!( + reduction + .target_problem() + .evaluate(&vec![true, true, false]) + .unwrap(), + Or(false) + ); + let mut witnesses = BruteForce::new() + .find_all_witnesses(reduction.target_problem()) + .unwrap(); + witnesses.sort(); + assert_eq!( + witnesses, + vec![vec![false, true, true], vec![true, false, true]] + ); + assert_identical_feasibility(&source); +} + +#[test] +fn test_threedimensionalmatching_to_exactcoverby3sets_unused_coordinate_is_infeasible() { + // X coordinate 2 never occurs, so no perfect matching and no exact cover. + let source = ThreeDimensionalMatching::new( + 3, + vec![(0, 0, 0), (1, 1, 1), (2, 1, 2), (2, 0, 2), (1, 0, 1)], + ); + let reduction = reduce(&source); + assert_eq!(BruteForce::new().solve(&source).unwrap(), None); + assert_eq!( + BruteForce::new().solve(reduction.target_problem()).unwrap(), + None + ); + assert_identical_feasibility(&source); +} + +#[test] +fn test_threedimensionalmatching_to_exactcoverby3sets_tags_equal_coordinates() { + // Equal numeric coordinates in different domains become distinct elements. + let source = ThreeDimensionalMatching::new(4, vec![(3, 3, 3), (0, 2, 1)]); + let reduction = reduce(&source); + assert_eq!(reduction.target_problem().universe_size(), 12); + assert_eq!( + reduction.target_problem().subsets(), + &[[3, 7, 11], [0, 6, 9]] + ); + assert_identical_feasibility(&source); +} + +#[test] +fn test_threedimensionalmatching_to_exactcoverby3sets_extraction_rejects_non_covers() { + let source = ThreeDimensionalMatching::new(2, vec![(0, 0, 0), (1, 1, 1), (0, 1, 1)]); + let reduction = reduce(&source); + assert_eq!( + reduction + .extract_solution(&vec![true, true, false]) + .unwrap(), + vec![true, true, false] + ); + // Too few subsets. + assert!( + reduction + .extract_solution(&vec![true, false, false]) + .is_err() + ); + // Right count but overlapping. + assert!( + reduction + .extract_solution(&vec![true, false, true]) + .is_err() + ); + // Too many subsets. + assert!(reduction.extract_solution(&vec![true, true, true]).is_err()); + // Wrong length is malformed rather than infeasible. + assert!(reduction.extract_solution(&vec![true, true]).is_err()); + assert!( + reduction + .extract_solution(&vec![true, true, false, false]) + .is_err() + ); +} + +#[test] +fn test_threedimensionalmatching_to_exactcoverby3sets_aggregate_identity() { + for triples in [ + vec![(0, 0, 0), (1, 1, 1)], + vec![(0, 0, 0), (0, 1, 1), (1, 0, 1)], + ] { + let source = ThreeDimensionalMatching::new(2, triples); + let reduction = reduce(&source); + let source_value = Or(BruteForce::new().solve(&source).unwrap().is_some()); + let target_value = Or(BruteForce::new() + .solve(ReductionResult::target_problem(&reduction)) + .unwrap() + .is_some()); + assert_eq!( + crate::rules::AggregateReductionResult::extract_value(&reduction, target_value), + source_value + ); + } +} + +#[test] +fn test_threedimensionalmatching_to_exactcoverby3sets_universe_overflow() { + // The largest q whose tagged universe 3q fits in usize still reduces. + let largest = usize::MAX / 3; + let reduction = reduce(&ThreeDimensionalMatching::new(largest, vec![])); + assert_eq!(reduction.target_problem().universe_size(), 3 * largest); + // One more is rejected with a typed overflow error rather than a panic. + let source = ThreeDimensionalMatching::new(largest + 1, vec![]); + let error = ReduceTo::::reduce_to(&source).unwrap_err(); + assert!(matches!(error, ReductionError::IntegerOverflow { .. })); +} From e88f9ac67727033d7ef8dff86d9fe57c8a313103 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Mon, 2 Nov 2026 00:47:11 -0800 Subject: [PATCH 2/2] Derive the 3DM -> X3C example's witness and uniqueness text from the fixture The selected triples and the element that forces each selected subset are now computed from the loaded example, and the build fails if the uniqueness argument no longer applies. --- docs/paper/reductions.typ | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 4f2551111..f8c5bbb72 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -19865,14 +19865,18 @@ The following table shows concrete target-variable counts for example instances, let triples = tdm_x3c.source.instance.triples let subsets = tdm_x3c.target.instance.subsets let selected = tdm_x3c_sol.source_config.enumerate().filter(((i, x)) => x).map(((i, x)) => i) + // For each selected subset, an element that no other subset contains. + let private = selected.map(i => (i, subsets.at(i).find(e => subsets.filter(s => s.contains(e)).len() == 1))) + assert(private.all(((i, e)) => e != none), message: "the uniqueness argument needs a private element in every selected subset") + let domains = ($w$, $x$, $y$) [ *Step 1 -- Source instance.* The canonical source has $q = #q$ and $t = #triples.len()$ triples: #triples.map(tr => "(" + fmt-values(tr) + ")").join(", "). *Step 2 -- Tag the coordinates.* The target universe is ${0, dots, #(3 * q - 1)}$: $W$ occupies $0, dots, #(q - 1)$, $X$ occupies $#q, dots, #(2 * q - 1)$ and $Y$ occupies $#(2 * q), dots, #(3 * q - 1)$. Triple $(w, x, y)$ becomes ${w, #q + x, #(2 * q) + y}$, giving the subsets #subsets.enumerate().map(((i, s)) => $S_#i = {#fmt-values(s)}$).join(", "). - *Step 3 -- Verify the witness.* The configuration $(#fmt-values(tdm_x3c_sol.target_config))$ selects #selected.map(i => $S_#i$).join(", "), which are pairwise disjoint and cover all $#(3 * q)$ elements #sym.checkmark. The identical source configuration selects the diagonal triples, a perfect matching #sym.checkmark. + *Step 3 -- Verify the witness.* The configuration $(#fmt-values(tdm_x3c_sol.target_config))$ selects #selected.map(i => $S_#i$).join(", "), which are pairwise disjoint and cover all $#(3 * q)$ elements #sym.checkmark. The identical source configuration selects the triples #selected.map(i => "(" + fmt-values(triples.at(i)) + ")").join(", "), a perfect matching #sym.checkmark. - *Multiplicity:* The fixture stores one canonical witness, and it is the only exact cover: element $#(q - 1)$ ($w = #(q - 1)$) lies only in $S_2$, element $#q$ ($x = 0$) only in $S_0$, and element $#(2 * q + 1)$ ($y = 1$) only in $S_1$, so every exact cover contains $S_0, S_1, S_2$, which already cover $U$. The cross subsets $S_3$ and $S_4$ are disjoint, but no third subset completes them. + *Multiplicity:* The fixture stores one canonical witness, and it is the only exact cover: #private.map(((i, e)) => [element $#e$ ($#domains.at(calc.quo(e, q)) = #calc.rem(e, q)$) lies only in $S_#i$]).join(", "), so every exact cover contains #selected.map(i => $S_#i$).join(", "), which already cover $U$. ] } ],