problemreductions/rules/
exactcoverby3sets_subsetproduct.rs

1//! Reduction from ExactCoverBy3Sets to SubsetProduct.
2//!
3//! Assign a distinct prime to each universe element. Each triple becomes the
4//! product of its three primes, and the target is the product of all universe
5//! primes. Unique factorization then makes exact covers correspond exactly to
6//! subsets whose product matches the target.
7
8use crate::models::formula::ksat::first_n_odd_primes;
9use crate::models::misc::SubsetProduct;
10use crate::models::set::ExactCoverBy3Sets;
11use crate::reduction;
12use crate::rules::traits::{ReduceTo, ReductionResult};
13use num_bigint::BigUint;
14use num_traits::One;
15
16#[derive(Debug, Clone)]
17pub struct ReductionX3CToSubsetProduct {
18    target: SubsetProduct,
19}
20
21impl ReductionResult for ReductionX3CToSubsetProduct {
22    type Source = ExactCoverBy3Sets;
23    type Target = SubsetProduct;
24
25    fn target_problem(&self) -> &Self::Target {
26        &self.target
27    }
28
29    fn extract_solution(
30        &self,
31        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
32    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
33        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
34
35        Ok(target_solution.to_vec())
36    }
37}
38
39fn product_biguint<I>(values: I) -> BigUint
40where
41    I: IntoIterator<Item = u64>,
42{
43    values.into_iter().fold(BigUint::one(), |product, value| {
44        product * BigUint::from(value)
45    })
46}
47
48fn assigned_primes(universe_size: usize) -> Vec<u64> {
49    match universe_size {
50        0 => Vec::new(),
51        1 => vec![2],
52        _ => {
53            let mut primes = Vec::with_capacity(universe_size);
54            primes.push(2);
55            primes.extend(first_n_odd_primes(universe_size - 1));
56            primes
57        }
58    }
59}
60
61#[reduction(
62    transform = exact {
63        num_elements = "num_sets",
64    })]
65impl ReduceTo<SubsetProduct> for ExactCoverBy3Sets {
66    type Result = ReductionX3CToSubsetProduct;
67
68    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
69        let primes = assigned_primes(self.universe_size());
70        let values = self
71            .sets()
72            .iter()
73            .map(|set| product_biguint(set.iter().map(|&element| primes[element])))
74            .collect();
75        let target = product_biguint(primes.iter().copied());
76
77        Ok(ReductionX3CToSubsetProduct {
78            target: SubsetProduct::new(values, target),
79        })
80    }
81}
82
83#[cfg(feature = "example-db")]
84pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
85    use crate::export::SolutionPair;
86
87    vec![crate::example_db::specs::RuleExampleSpec {
88        id: "exactcoverby3sets_to_subsetproduct",
89        build: || {
90            crate::example_db::specs::rule_example_with_witness::<_, SubsetProduct>(
91                ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]),
92                SolutionPair {
93                    source_config: serde_json::json!(vec![true, true, false]),
94                    target_config: serde_json::json!(vec![true, true, false]),
95                },
96            )
97        },
98    }]
99}
100
101#[cfg(test)]
102#[path = "../unit_tests/rules/exactcoverby3sets_subsetproduct.rs"]
103mod tests;
problemreductions/rules/exactcoverby3sets_subsetproduct.rs

problemreductions/rules/
exactcoverby3sets_subsetproduct.rs
