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. For NO-instances, the extracted
31    /// vector may be non-satisfying, which is expected for an `Or -> Min` rule.
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_solution(self.target_problem(), target_solution)?;
37
38        Ok({
39            let set_offset = self.source_universe_size;
40            (0..self.source_num_subsets)
41                .map(|j| target_solution[set_offset + j])
42                .collect()
43        })
44    }
45}
46
47#[reduction(
48    transform = exact {
49        num_sentences = "universe_size + num_subsets",
50        num_true_sentences = "universe_size + num_subsets",
51        num_implications = "4 * num_subsets",
52    })]
53impl ReduceTo<MinimumAxiomSet> for ExactCoverBy3Sets {
54    type Result = ReductionXC3SToMinimumAxiomSet;
55
56    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
57        let universe_size = self.universe_size();
58        let num_subsets = self.num_subsets();
59        let num_sentences = universe_size + num_subsets;
60
61        let mut implications = Vec::with_capacity(4 * num_subsets);
62        for (j, subset) in self.subsets().iter().enumerate() {
63            let set_sentence = universe_size + j;
64            for &element in subset {
65                implications.push((vec![set_sentence], element));
66            }
67            implications.push((subset.to_vec(), set_sentence));
68        }
69
70        let target =
71            MinimumAxiomSet::new(num_sentences, (0..num_sentences).collect(), implications);
72
73        Ok(ReductionXC3SToMinimumAxiomSet {
74            target,
75            source_universe_size: universe_size,
76            source_num_subsets: num_subsets,
77        })
78    }
79}
80
81#[cfg(feature = "example-db")]
82pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
83    use crate::export::SolutionPair;
84
85    vec![crate::example_db::specs::RuleExampleSpec {
86        id: "exactcoverby3sets_to_minimumaxiomset",
87        build: || {
88            let source = ExactCoverBy3Sets::new(
89                6,
90                vec![[0, 1, 2], [0, 3, 4], [2, 4, 5], [1, 3, 5], [0, 2, 4]],
91            );
92            crate::example_db::specs::rule_example_with_witness::<_, MinimumAxiomSet>(
93                source,
94                SolutionPair {
95                    source_config: serde_json::json!(vec![false, false, false, true, true]),
96                    target_config: serde_json::json!(vec![
97                        false, false, false, false, false, false, false, false, false, true, true
98                    ]),
99                },
100            )
101        },
102    }]
103}
104
105#[cfg(test)]
106#[path = "../unit_tests/rules/exactcoverby3sets_minimumaxiomset.rs"]
107mod tests;
problemreductions/rules/exactcoverby3sets_minimumaxiomset.rs

problemreductions/rules/
exactcoverby3sets_minimumaxiomset.rs
