From 6ff40ae5b0be3dadd187536da0928100255f6360 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:39:50 +0800 Subject: [PATCH 1/5] Add plan for #1103: ThreeDimensionalMatching to ExactCoverBy3Sets --- ...imensionalmatching-to-exactcoverby3sets.md | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 docs/plans/2026-08-02-threedimensionalmatching-to-exactcoverby3sets.md diff --git a/docs/plans/2026-08-02-threedimensionalmatching-to-exactcoverby3sets.md b/docs/plans/2026-08-02-threedimensionalmatching-to-exactcoverby3sets.md new file mode 100644 index 000000000..06980ff89 --- /dev/null +++ b/docs/plans/2026-08-02-threedimensionalmatching-to-exactcoverby3sets.md @@ -0,0 +1,26 @@ +# ThreeDimensionalMatching to ExactCoverBy3Sets + +Implement issue #1103 as a witness-preserving `Or -> Or` reduction on top of commit `a9067297`. The construction maps each indexed source triple `(w, x, y)` over three size-`q` coordinate domains to `[w, q + x, 2 * q + y]` in a tagged universe of size `3q`; target and source configuration vectors have identical indexing. + +References: Richard M. Karp, “Reducibility Among Combinatorial Problems” (1972), DOI `10.1007/978-1-4684-2001-2_9`; Garey and Johnson, *Computers and Intractability* (1979), Appendix A, SP1–SP2. + +## Batch 1 — Reduction, registration, tests, and canonical example + +Follow `.claude/skills/add-rule/SKILL.md` Steps 1–5. + +1. Carry forward the completed mathematical verification: the tagged blocks make every target subset a valid three-element set; a source perfect matching selects `q` coordinate-disjoint triples iff the corresponding sets form an exact cover of all `3q` tagged elements. Solution extraction is the identity vector. Preserve duplicate triple indices. The verified feasible example is `q=3` with triples `[(0,0,0),(1,1,1),(2,2,2),(0,1,2),(1,2,0)]`; the verified infeasible example is `q=3` with `[(0,0,0),(0,1,1),(1,2,2)]`. +2. Add `src/rules/threedimensionalmatching_exactcoverby3sets.rs` with a direct `ReductionResult` implementation and `ReduceTo for ThreeDimensionalMatching`. Construct the target as `ExactCoverBy3Sets::new(3 * self.universe_size(), tagged_subsets)`. Use exact overhead metadata `universe_size = "3 * universe_size"`, `num_subsets = "num_triples"`, and `num_sets = "num_triples"`. Do not introduce adapters, registries, compatibility paths, or mapping state that identity extraction does not need. +3. Register the module directly in `src/rules/mod.rs` in the existing set-rule section. +4. Add `src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs`. Include the semantically named closed-loop test, exact target tagging and overhead assertions, infeasible/no-witness behavior, empty `q=0`, duplicate triples, unused coordinates, equal numeric coordinates across domains, and identity extraction. Keep every test under five seconds and use focused assertions rather than snapshots. +5. Add the canonical rule example using the current per-rule `canonical_rule_example_specs()` pattern in the rule module. Use the issue’s five-triple `q=3` instance and canonical witness `[1,1,1,0,0]`; ensure it is discovered through the existing example-db aggregation. +6. Run focused formatting and tests for the new rule, then `cargo run --example export_graph` to confirm the primitive edge and overhead metadata appear exactly once. + +## Batch 2 — Paper documentation, generated fixtures, and final verification + +Follow `.claude/skills/add-rule/SKILL.md` Steps 6–7 after Batch 1 is complete. + +1. Add `load-example("ThreeDimensionalMatching", "ExactCoverBy3Sets")` bindings and a mandatory `reduction-rule("ThreeDimensionalMatching", "ExactCoverBy3Sets", ...)` entry near the existing ThreeDimensionalMatching reductions in `docs/paper/reductions.typ`. +2. Make the theorem self-contained: define `q`, the indexed triple list, the three tagged blocks, and the target sets; prove both directions independently; state identity extraction and exact size overhead. Cite Karp/Garey–Johnson using existing bibliography keys when available. +3. Add a tutorial-style `extra:` block starting with `pred-commands()` derived from `problem-spec()` and `target-spec()` on the loaded fixture. Walk through the exact five tagged subsets, verify the diagonal witness end-to-end, and explain that the two cross triples are mutually disjoint but cannot be extended by any available third triple. State that the fixture stores one canonical witness. +4. Regenerate the graph/schema exports and canonical example fixture with the repository commands. Commit only tracked artifacts required by the rule and paper; do not include ignored exports or temporary verification files. +5. Run `make paper`, `make test`, `make clippy`, formatting checks, and the repository’s coverage command. Inspect the final diff and working tree, remove the temporary plan file as required by `issue-to-pr`, and report any deviation from this plan in the PR implementation summary. From 755f9112623894978c571a15232578a5c316d5c7 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:53:17 +0800 Subject: [PATCH 2/5] Implement ThreeDimensionalMatching to ExactCoverBy3Sets reduction --- src/rules/mod.rs | 2 + ...eedimensionalmatching_exactcoverby3sets.rs | 75 +++++++++++ ...eedimensionalmatching_exactcoverby3sets.rs | 121 ++++++++++++++++++ 3 files changed, 198 insertions(+) create mode 100644 src/rules/threedimensionalmatching_exactcoverby3sets.rs create mode 100644 src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 95eb5f477..f8762f38b 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -147,6 +147,7 @@ pub(crate) mod subsetsum_integerknapsack; pub(crate) mod subsetsum_partition; #[cfg(test)] pub(crate) mod test_helpers; +pub(crate) mod threedimensionalmatching_exactcoverby3sets; pub(crate) mod threedimensionalmatching_minimumweightdecoding; pub(crate) mod threedimensionalmatching_threematroidintersection; pub(crate) mod threedimensionalmatching_threepartition; @@ -522,6 +523,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[reduction(overhead = { + universe_size = "3 * universe_size", + num_subsets = "num_triples", + num_sets = "num_triples", +})] +impl ReduceTo for ThreeDimensionalMatching { + type Result = ReductionThreeDimensionalMatchingToExactCoverBy3Sets; + + fn reduce_to(&self) -> Self::Result { + let q = self.universe_size(); + let tagged_subsets = self + .triples() + .iter() + .map(|&(w, x, y)| [w, q + x, 2 * q + y]) + .collect(); + + ReductionThreeDimensionalMatchingToExactCoverBy3Sets { + target: ExactCoverBy3Sets::new(3 * q, tagged_subsets), + } + } +} + +#[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: vec![1, 1, 1, 0, 0], + target_config: vec![1, 1, 1, 0, 0], + }, + ) + }, + }] +} + +#[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..58265ce40 --- /dev/null +++ b/src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs @@ -0,0 +1,121 @@ +use super::*; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::solvers::BruteForce; +use crate::traits::Problem; + +#[test] +fn test_threedimensionalmatching_to_exactcoverby3sets_closed_loop() { + let source = ThreeDimensionalMatching::new( + 3, + vec![(0, 0, 0), (1, 1, 1), (2, 2, 2), (0, 1, 2), (1, 2, 0)], + ); + let reduction = ReduceTo::::reduce_to(&source); + let target_witnesses = BruteForce::new().find_all_witnesses(reduction.target_problem()); + + assert!(!target_witnesses.is_empty()); + for target_witness in target_witnesses { + let source_witness = reduction.extract_solution(&target_witness); + assert!(source.evaluate(&source_witness).0); + assert_eq!(source_witness, target_witness); + } +} + +#[test] +fn test_target_tagging_and_overhead() { + let source = ThreeDimensionalMatching::new(3, vec![(0, 2, 1), (2, 0, 2)]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.universe_size(), 9); + assert_eq!(target.subsets(), &[[0, 5, 7], [2, 3, 8]]); + assert_eq!(target.num_subsets(), 2); + assert_eq!(target.num_sets(), 2); + + let entries: Vec<_> = inventory::iter::() + .filter(|entry| { + entry.source_name == "ThreeDimensionalMatching" + && entry.target_name == "ExactCoverBy3Sets" + }) + .collect(); + assert_eq!(entries.len(), 1); + let overhead = (entries[0].overhead_eval_fn)(&source as &dyn std::any::Any); + assert_eq!(overhead.get("universe_size"), Some(9)); + assert_eq!(overhead.get("num_subsets"), Some(2)); + assert_eq!(overhead.get("num_sets"), Some(2)); +} + +#[test] +fn test_infeasible_instance_has_no_target_witness() { + let source = ThreeDimensionalMatching::new(3, vec![(0, 0, 0), (0, 1, 1), (1, 2, 2)]); + let reduction = ReduceTo::::reduce_to(&source); + + assert!(BruteForce::new().find_witness(&source).is_none()); + assert!(BruteForce::new() + .find_witness(reduction.target_problem()) + .is_none()); +} + +#[test] +fn test_empty_universe_preserves_empty_witness() { + let source = ThreeDimensionalMatching::new(0, vec![]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.universe_size(), 0); + assert!(target.subsets().is_empty()); + let target_witness = BruteForce::new().find_witness(target).unwrap(); + assert!(target_witness.is_empty()); + assert!( + source + .evaluate(&reduction.extract_solution(&target_witness)) + .0 + ); +} + +#[test] +fn test_duplicate_triples_preserve_indices() { + let source = ThreeDimensionalMatching::new(2, vec![(0, 0, 0), (0, 0, 0), (1, 1, 1)]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!( + reduction.target_problem().subsets(), + &[[0, 2, 4], [0, 2, 4], [1, 3, 5]] + ); + let witnesses = BruteForce::new().find_all_witnesses(reduction.target_problem()); + assert_eq!(witnesses, vec![vec![0, 1, 1], vec![1, 0, 1]]); + for witness in witnesses { + assert!(source.evaluate(&reduction.extract_solution(&witness)).0); + } +} + +#[test] +fn test_unused_coordinate_makes_both_instances_infeasible() { + let source = ThreeDimensionalMatching::new(2, vec![(0, 0, 0), (1, 0, 1)]); + let reduction = ReduceTo::::reduce_to(&source); + + assert!(BruteForce::new().find_witness(&source).is_none()); + assert!(BruteForce::new() + .find_witness(reduction.target_problem()) + .is_none()); +} + +#[test] +fn test_equal_numeric_coordinates_are_distinct_across_domains() { + let source = ThreeDimensionalMatching::new(2, vec![(0, 0, 0), (1, 1, 1)]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!( + reduction.target_problem().subsets(), + &[[0, 2, 4], [1, 3, 5]] + ); + assert!(reduction.target_problem().evaluate(&[1, 1]).0); + assert!(source.evaluate(&reduction.extract_solution(&[1, 1])).0); +} + +#[test] +fn test_solution_extraction_is_identity() { + let source = ThreeDimensionalMatching::new(2, vec![(0, 0, 0), (1, 1, 1)]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!(reduction.extract_solution(&[1, 0]), vec![1, 0]); +} From 9a611082f8bcb8734cc043cfad0033956808566e Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 15:11:21 +0800 Subject: [PATCH 3/5] Document ThreeDimensionalMatching to ExactCoverBy3Sets reduction --- docs/paper/reductions.typ | 51 ++++++++++++++++++++++++++++++++ src/unit_tests/rules/analysis.rs | 2 ++ 2 files changed, 53 insertions(+) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 88cd07556..5d70e79cc 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -19165,6 +19165,57 @@ The following table shows concrete variable overhead for example instances, take #let tdm_tp_sol = tdm_tp.solutions.at(0) #let tdm_tmi = load-example("ThreeDimensionalMatching", "ThreeMatroidIntersection") #let tdm_tmi_sol = tdm_tmi.solutions.at(0) +#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$, #tdm_x3c.source.instance.triples.len() triples $arrow.r$ #tdm_x3c.target.instance.subsets.len() tagged 3-sets], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(tdm_x3c.source) + " -o three-dimensional-matching.json", + "pred reduce three-dimensional-matching.json --to " + target-spec(tdm_x3c) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate three-dimensional-matching.json --config " + tdm_x3c_sol.source_config.map(str).join(","), + ) + + #{ + let q = tdm_x3c.source.instance.universe_size + let triples = tdm_x3c.source.instance.triples + let subsets = tdm_x3c.target.instance.subsets + let witness-indices = tdm_x3c_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => i) + let witness-elements = witness-indices.map(i => subsets.at(i)).flatten().sorted() + let cross-indices = (triples.len() - 2, triples.len() - 1) + let cross-elements = cross-indices.map(i => subsets.at(i)).flatten().sorted() + let uncovered = range(3 * q).filter(element => not cross-elements.contains(element)) + [ + *Step 1 -- Read the indexed 3DM instance.* The three coordinate domains each have size $q = #q$. The fixture's indexed triple list is #triples.enumerate().map(((i, triple)) => "$t_" + str(i) + " = (" + triple.map(str).join(", ") + ")$").join([; ]). + + *Step 2 -- Tag the coordinate domains.* Put the first, second, and third coordinates in disjoint numeric blocks $[0, q)$, $[q, 2q)$, and $[2q, 3q)$. Thus triple $t_j = (a_j, b_j, c_j)$ becomes $S_j = {a_j, q + b_j, 2q + c_j}$. The exact five target subsets are #subsets.enumerate().map(((i, subset)) => "$S_" + str(i) + " = {" + subset.map(str).join(", ") + "}$").join([; ]). The target therefore has universe size $#tdm_x3c.target.instance.universe_size = 3 q$ and one subset per source triple. + + *Step 3 -- Verify the diagonal witness end-to-end.* The canonical source configuration is $(#tdm_x3c_sol.source_config.map(str).join(", "))$, selecting triple indices $#witness-indices.map(str).join(", ")$. Their target subsets have sorted union ${#witness-elements.map(str).join(", ")}$, which is every element of the tagged universe exactly once. The target configuration is the identical vector $(#tdm_x3c_sol.target_config.map(str).join(", "))$, so exact-cover feasibility maps back to the diagonal perfect matching #sym.checkmark. + + *Step 4 -- Understand the cross triples.* The final two triples map to $S_#cross-indices.at(0) = {#subsets.at(cross-indices.at(0)).map(str).join(", ")}$ and $S_#cross-indices.at(1) = {#subsets.at(cross-indices.at(1)).map(str).join(", ")}$. These two sets are mutually disjoint, but together they leave ${#uncovered.map(str).join(", ")}$ uncovered. None of the five available subsets is contained in that remaining three-element set, so the pair cannot be extended by any available third triple to an exact cover. + + *Multiplicity:* The fixture stores one canonical witness. + ] + } + ], +)[ + This $O(q + t)$ reduction @karp1972 @garey1979[SP1--SP2] embeds the three coordinate domains of a Three-Dimensional Matching instance into three disjoint tagged blocks. For $t$ indexed source triples it constructs an Exact Cover by 3-Sets instance with exactly $3q$ universe elements and $t$ subsets (hence $t$ subset variables). +][ + _Construction._ Let $q in NN$ and let the source contain the indexed list $T = (t_0, dots, t_(t - 1))$, where $t_j = (a_j, b_j, c_j) in W times X times Y$ and $W = X = Y = {0, dots, q - 1}$. Form the disjoint tagged blocks + $ W' = {0, dots, q - 1}, quad X' = {q, dots, 2q - 1}, quad Y' = {2q, dots, 3q - 1}, $ + and target universe $U' = W' union X' union Y'$. For every indexed triple $t_j$, create the three-element target subset + $ S_j = {a_j, q + b_j, 2q + c_j}. $ + The target family is the indexed list $(S_0, dots, S_(t - 1))$; in particular, duplicate source triples remain distinct subset variables. The exact target sizes are $|U'| = 3q$ and $|cal(S)| = t$. + + _Correctness._ ($arrow.r.double$) Suppose source indices $J subset.eq {0, dots, t - 1}$ form a perfect three-dimensional matching. Every coordinate value occurs in exactly one selected triple. Therefore every element of $W'$, $X'$, and $Y'$ occurs in exactly one set $S_j$ with $j in J$. The selected sets are pairwise disjoint and their union is $U'$, so they form an exact cover. + + ($arrow.l.double$) Conversely, suppose target indices $J$ select an exact cover of $U'$. Each $S_j$ contains exactly one element from each of the three tagged blocks. Exact coverage of $W'$ implies that the first coordinates of the selected triples contain every value in $W$ exactly once; exact coverage of $X'$ and $Y'$ gives the same conclusion for the second and third coordinates. Hence the source triples indexed by $J$ are pairwise coordinate-disjoint and cover all three domains, so they form a perfect three-dimensional matching. + + _Solution extraction._ Return the target's binary subset-indicator vector unchanged: target variable $j$ and source variable $j$ both refer to the same indexed triple. +] + #reduction-rule("ThreeDimensionalMatching", "ThreeMatroidIntersection", example: true, example-caption: [$q = 3$, $t = 5$ triples], diff --git a/src/unit_tests/rules/analysis.rs b/src/unit_tests/rules/analysis.rs index 6088d9d38..f9ccf18b6 100644 --- a/src/unit_tests/rules/analysis.rs +++ b/src/unit_tests/rules/analysis.rs @@ -302,6 +302,8 @@ fn test_find_dominated_rules_returns_known_set() { ), // ExactCoverBy3Sets → MaxSetPacking → ILP is better than direct ExactCoverBy3Sets → ILP ("ExactCoverBy3Sets", "ILP {variable: \"bool\"}"), + // ThreeDimensionalMatching → ExactCoverBy3Sets → ILP is better than direct ThreeDimensionalMatching → ILP + ("ThreeDimensionalMatching", "ILP {variable: \"bool\"}"), // GraphPartitioning → MaxCut → SpinGlass → QUBO is better than direct GraphPartitioning → QUBO ( "GraphPartitioning {graph: \"SimpleGraph\"}", From c35339389c41bb5f511a61e51d7557b20f91bd30 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 15:11:21 +0800 Subject: [PATCH 4/5] chore: remove plan file after implementation --- ...imensionalmatching-to-exactcoverby3sets.md | 26 ------------------- 1 file changed, 26 deletions(-) delete mode 100644 docs/plans/2026-08-02-threedimensionalmatching-to-exactcoverby3sets.md diff --git a/docs/plans/2026-08-02-threedimensionalmatching-to-exactcoverby3sets.md b/docs/plans/2026-08-02-threedimensionalmatching-to-exactcoverby3sets.md deleted file mode 100644 index 06980ff89..000000000 --- a/docs/plans/2026-08-02-threedimensionalmatching-to-exactcoverby3sets.md +++ /dev/null @@ -1,26 +0,0 @@ -# ThreeDimensionalMatching to ExactCoverBy3Sets - -Implement issue #1103 as a witness-preserving `Or -> Or` reduction on top of commit `a9067297`. The construction maps each indexed source triple `(w, x, y)` over three size-`q` coordinate domains to `[w, q + x, 2 * q + y]` in a tagged universe of size `3q`; target and source configuration vectors have identical indexing. - -References: Richard M. Karp, “Reducibility Among Combinatorial Problems” (1972), DOI `10.1007/978-1-4684-2001-2_9`; Garey and Johnson, *Computers and Intractability* (1979), Appendix A, SP1–SP2. - -## Batch 1 — Reduction, registration, tests, and canonical example - -Follow `.claude/skills/add-rule/SKILL.md` Steps 1–5. - -1. Carry forward the completed mathematical verification: the tagged blocks make every target subset a valid three-element set; a source perfect matching selects `q` coordinate-disjoint triples iff the corresponding sets form an exact cover of all `3q` tagged elements. Solution extraction is the identity vector. Preserve duplicate triple indices. The verified feasible example is `q=3` with triples `[(0,0,0),(1,1,1),(2,2,2),(0,1,2),(1,2,0)]`; the verified infeasible example is `q=3` with `[(0,0,0),(0,1,1),(1,2,2)]`. -2. Add `src/rules/threedimensionalmatching_exactcoverby3sets.rs` with a direct `ReductionResult` implementation and `ReduceTo for ThreeDimensionalMatching`. Construct the target as `ExactCoverBy3Sets::new(3 * self.universe_size(), tagged_subsets)`. Use exact overhead metadata `universe_size = "3 * universe_size"`, `num_subsets = "num_triples"`, and `num_sets = "num_triples"`. Do not introduce adapters, registries, compatibility paths, or mapping state that identity extraction does not need. -3. Register the module directly in `src/rules/mod.rs` in the existing set-rule section. -4. Add `src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs`. Include the semantically named closed-loop test, exact target tagging and overhead assertions, infeasible/no-witness behavior, empty `q=0`, duplicate triples, unused coordinates, equal numeric coordinates across domains, and identity extraction. Keep every test under five seconds and use focused assertions rather than snapshots. -5. Add the canonical rule example using the current per-rule `canonical_rule_example_specs()` pattern in the rule module. Use the issue’s five-triple `q=3` instance and canonical witness `[1,1,1,0,0]`; ensure it is discovered through the existing example-db aggregation. -6. Run focused formatting and tests for the new rule, then `cargo run --example export_graph` to confirm the primitive edge and overhead metadata appear exactly once. - -## Batch 2 — Paper documentation, generated fixtures, and final verification - -Follow `.claude/skills/add-rule/SKILL.md` Steps 6–7 after Batch 1 is complete. - -1. Add `load-example("ThreeDimensionalMatching", "ExactCoverBy3Sets")` bindings and a mandatory `reduction-rule("ThreeDimensionalMatching", "ExactCoverBy3Sets", ...)` entry near the existing ThreeDimensionalMatching reductions in `docs/paper/reductions.typ`. -2. Make the theorem self-contained: define `q`, the indexed triple list, the three tagged blocks, and the target sets; prove both directions independently; state identity extraction and exact size overhead. Cite Karp/Garey–Johnson using existing bibliography keys when available. -3. Add a tutorial-style `extra:` block starting with `pred-commands()` derived from `problem-spec()` and `target-spec()` on the loaded fixture. Walk through the exact five tagged subsets, verify the diagonal witness end-to-end, and explain that the two cross triples are mutually disjoint but cannot be extended by any available third triple. State that the fixture stores one canonical witness. -4. Regenerate the graph/schema exports and canonical example fixture with the repository commands. Commit only tracked artifacts required by the rule and paper; do not include ignored exports or temporary verification files. -5. Run `make paper`, `make test`, `make clippy`, formatting checks, and the repository’s coverage command. Inspect the final diff and working tree, remove the temporary plan file as required by `issue-to-pr`, and report any deviation from this plan in the PR implementation summary. From e5493c294f4aafdd80558eefdaff5e10dee3f6ca Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 15:41:24 +0800 Subject: [PATCH 5/5] fix: address PR #1112 review comments - exhaust all q=2 triple families and compare exact witness sets - use the shared satisfaction round-trip helper - compare duplicate witnesses without relying on enumeration order --- ...eedimensionalmatching_exactcoverby3sets.rs | 47 +++++++++++++++---- 1 file changed, 39 insertions(+), 8 deletions(-) diff --git a/src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs b/src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs index 58265ce40..2782b6ac1 100644 --- a/src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs +++ b/src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs @@ -1,7 +1,9 @@ use super::*; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; use crate::rules::traits::{ReduceTo, ReductionResult}; use crate::solvers::BruteForce; use crate::traits::Problem; +use std::collections::HashSet; #[test] fn test_threedimensionalmatching_to_exactcoverby3sets_closed_loop() { @@ -10,13 +12,39 @@ fn test_threedimensionalmatching_to_exactcoverby3sets_closed_loop() { vec![(0, 0, 0), (1, 1, 1), (2, 2, 2), (0, 1, 2), (1, 2, 0)], ); let reduction = ReduceTo::::reduce_to(&source); - let target_witnesses = BruteForce::new().find_all_witnesses(reduction.target_problem()); + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "ThreeDimensionalMatching -> ExactCoverBy3Sets", + ); +} - assert!(!target_witnesses.is_empty()); - for target_witness in target_witnesses { - let source_witness = reduction.extract_solution(&target_witness); - assert!(source.evaluate(&source_witness).0); - assert_eq!(source_witness, target_witness); +#[test] +fn test_all_q2_triple_families_preserve_exact_witnesses() { + let triples: Vec<_> = (0..2) + .flat_map(|w| (0..2).flat_map(move |x| (0..2).map(move |y| (w, x, y)))) + .collect(); + let solver = BruteForce::new(); + + for family_mask in 0..(1usize << triples.len()) { + let family: Vec<_> = triples + .iter() + .enumerate() + .filter_map(|(index, &triple)| ((family_mask >> index) & 1 == 1).then_some(triple)) + .collect(); + let source = ThreeDimensionalMatching::new(2, family); + let reduction = ReduceTo::::reduce_to(&source); + let source_witnesses: HashSet<_> = solver.find_all_witnesses(&source).into_iter().collect(); + let extracted_witnesses: HashSet<_> = solver + .find_all_witnesses(reduction.target_problem()) + .into_iter() + .map(|witness| reduction.extract_solution(&witness)) + .collect(); + + assert_eq!( + extracted_witnesses, source_witnesses, + "witness mismatch for family mask {family_mask:#010b}" + ); } } @@ -81,8 +109,11 @@ fn test_duplicate_triples_preserve_indices() { reduction.target_problem().subsets(), &[[0, 2, 4], [0, 2, 4], [1, 3, 5]] ); - let witnesses = BruteForce::new().find_all_witnesses(reduction.target_problem()); - assert_eq!(witnesses, vec![vec![0, 1, 1], vec![1, 0, 1]]); + let witnesses: HashSet<_> = BruteForce::new() + .find_all_witnesses(reduction.target_problem()) + .into_iter() + .collect(); + assert_eq!(witnesses, HashSet::from([vec![0, 1, 1], vec![1, 0, 1]])); for witness in witnesses { assert!(source.evaluate(&reduction.extract_solution(&witness)).0); }