problemreductions/rules/
exactcoverby3sets_minimumaxiomset.rs

1//! Reduction from ExactCoverBy3Sets to MinimumAxiomSet.
2//!
3//! Universe elements become element-sentences, source subsets become set-sentences,
4//! and the target optimum hits q = |U| / 3 exactly when the source has an exact cover.
5
6use crate::models::misc::MinimumAxiomSet;
7use crate::models::set::ExactCoverBy3Sets;
8use crate::reduction;
9use crate::rules::traits::{ReduceTo, ReductionResult};
10
11/// Result of reducing ExactCoverBy3Sets to MinimumAxiomSet.
12#[derive(Debug, Clone)]
13pub struct ReductionXC3SToMinimumAxiomSet {
14    target: MinimumAxiomSet,
15    source_universe_size: usize,
16    source_num_subsets: usize,
17}
18
19impl ReductionResult for ReductionXC3SToMinimumAxiomSet {
20    type Source = ExactCoverBy3Sets;
21    type Target = MinimumAxiomSet;
22
23    fn target_problem(&self) -> &Self::Target {
24        &self.target
25    }
26
27    /// Extract the chosen source subsets from the set-sentence coordinates.
28    ///
29    /// For YES-instances, every optimal target witness of value q consists only of
30    /// q set-sentences, which form an exact cover. Witnesses outside this bound
31    /// are rejected; the completed optimum maps to YES/NO via `extract_value`.
32    fn extract_solution(
33        &self,
34        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
35    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
36        crate::rules::traits::validate_target_witness(
37            self.target_problem(),
38            target_solution,
39            |value| crate::rules::AggregateReductionResult::extract_value(self, value).0,
40            "target witness does not certify a YES answer for the source",
41        )?;
42
43        Ok({
44            let set_offset = self.source_universe_size;
45            (0..self.source_num_subsets)
46                .map(|j| target_solution[set_offset + j])
47                .collect()
48        })
49    }
50}
51
52#[crate::aggregate_reduction]
53impl crate::rules::AggregateReductionResult for ReductionXC3SToMinimumAxiomSet {
54    type Source = ExactCoverBy3Sets;
55    type Target = MinimumAxiomSet;
56
57    fn target_problem(&self) -> &Self::Target {
58        &self.target
59    }
60
61    fn extract_value(&self, value: crate::types::Min<i64>) -> crate::types::Or {
62        crate::types::Or(
63            value
64                .0
65                .is_some_and(|count| i128::from(count) == self.source_universe_size as i128 / 3),
66        )
67    }
68}
69
70#[reduction(
71    transform = exact {
72        num_sentences = "universe_size + num_subsets",
73        num_true_sentences = "universe_size + num_subsets",
74        num_implications = "4 * num_subsets",
75    })]
76impl ReduceTo<MinimumAxiomSet> for ExactCoverBy3Sets {
77    type Result = ReductionXC3SToMinimumAxiomSet;
78
79    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
80        let universe_size = self.universe_size();
81        let num_subsets = self.num_subsets();
82        let num_sentences = universe_size + num_subsets;
83
84        let mut implications = Vec::with_capacity(4 * num_subsets);
85        for (j, subset) in self.subsets().iter().enumerate() {
86            let set_sentence = universe_size + j;
87            for &element in subset {
88                implications.push((vec![set_sentence], element));
89            }
90            implications.push((subset.to_vec(), set_sentence));
91        }
92
93        let target =
94            MinimumAxiomSet::new(num_sentences, (0..num_sentences).collect(), implications);
95
96        Ok(ReductionXC3SToMinimumAxiomSet {
97            target,
98            source_universe_size: universe_size,
99            source_num_subsets: num_subsets,
100        })
101    }
102}
103
104#[cfg(feature = "example-db")]
105pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
106    use crate::export::SolutionPair;
107
108    vec![crate::example_db::specs::RuleExampleSpec {
109        id: "exactcoverby3sets_to_minimumaxiomset",
110        build: || {
111            let source = ExactCoverBy3Sets::new(
112                6,
113                vec![[0, 1, 2], [0, 3, 4], [2, 4, 5], [1, 3, 5], [0, 2, 4]],
114            );
115            crate::example_db::specs::rule_example_with_witness::<_, MinimumAxiomSet>(
116                source,
117                SolutionPair {
118                    source_config: serde_json::json!(vec![false, false, false, true, true]),
119                    target_config: serde_json::json!(vec![
120                        false, false, false, false, false, false, false, false, false, true, true
121                    ]),
122                },
123            )
124        },
125    }]
126}
127
128#[cfg(test)]
129#[path = "../unit_tests/rules/exactcoverby3sets_minimumaxiomset.rs"]
130mod tests;
problemreductions/rules/exactcoverby3sets_minimumaxiomset.rs

problemreductions/rules/
exactcoverby3sets_minimumaxiomset.rs
