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_witness(
34            self.target_problem(),
35            target_solution,
36            |value| value.0,
37            "target witness is not satisfying",
38        )?;
39
40        Ok(target_solution.to_vec())
41    }
42}
43
44fn product_biguint<I>(values: I) -> BigUint
45where
46    I: IntoIterator<Item = u64>,
47{
48    values.into_iter().fold(BigUint::one(), |product, value| {
49        product * BigUint::from(value)
50    })
51}
52
53fn assigned_primes(universe_size: usize) -> Vec<u64> {
54    match universe_size {
55        0 => Vec::new(),
56        1 => vec![2],
57        _ => {
58            let mut primes = Vec::with_capacity(universe_size);
59            primes.push(2);
60            primes.extend(first_n_odd_primes(universe_size - 1));
61            primes
62        }
63    }
64}
65
66#[crate::aggregate_reduction(identity)]
67impl crate::rules::AggregateReductionResult for ReductionX3CToSubsetProduct {}
68
69#[reduction(
70    transform = exact {
71        num_elements = "num_subsets",
72    })]
73impl ReduceTo<SubsetProduct> for ExactCoverBy3Sets {
74    type Result = ReductionX3CToSubsetProduct;
75
76    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
77        let primes = assigned_primes(self.universe_size());
78        let values = self
79            .sets()
80            .iter()
81            .map(|set| product_biguint(set.iter().map(|&element| primes[element])))
82            .collect();
83        let target = product_biguint(primes.iter().copied());
84
85        Ok(ReductionX3CToSubsetProduct {
86            target: SubsetProduct::new(values, target),
87        })
88    }
89}
90
91#[cfg(feature = "example-db")]
92pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
93    use crate::export::SolutionPair;
94
95    vec![crate::example_db::specs::RuleExampleSpec {
96        id: "exactcoverby3sets_to_subsetproduct",
97        build: || {
98            crate::example_db::specs::rule_example_with_witness::<_, SubsetProduct>(
99                ExactCoverBy3Sets::new(6, vec![[0, 1, 2], [3, 4, 5], [0, 3, 4]]),
100                SolutionPair {
101                    source_config: serde_json::json!(vec![true, true, false]),
102                    target_config: serde_json::json!(vec![true, true, false]),
103                },
104            )
105        },
106    }]
107}
108
109#[cfg(test)]
110#[path = "../unit_tests/rules/exactcoverby3sets_subsetproduct.rs"]
111mod tests;
problemreductions/rules/exactcoverby3sets_subsetproduct.rs

problemreductions/rules/
exactcoverby3sets_subsetproduct.rs
