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(&self, target_solution: &[usize]) -> Vec<usize> {
33        let set_offset = self.source_universe_size;
34        (0..self.source_num_subsets)
35            .map(|j| usize::from(target_solution.get(set_offset + j).copied().unwrap_or(0) > 0))
36            .collect()
37    }
38}
39
40#[reduction(overhead = {
41    num_sentences = "universe_size + num_subsets",
42    num_true_sentences = "universe_size + num_subsets",
43    num_implications = "4 * num_subsets",
44})]
45impl ReduceTo<MinimumAxiomSet> for ExactCoverBy3Sets {
46    type Result = ReductionXC3SToMinimumAxiomSet;
47
48    fn reduce_to(&self) -> Self::Result {
49        let universe_size = self.universe_size();
50        let num_subsets = self.num_subsets();
51        let num_sentences = universe_size + num_subsets;
52
53        let mut implications = Vec::with_capacity(4 * num_subsets);
54        for (j, subset) in self.subsets().iter().enumerate() {
55            let set_sentence = universe_size + j;
56            for &element in subset {
57                implications.push((vec![set_sentence], element));
58            }
59            implications.push((subset.to_vec(), set_sentence));
60        }
61
62        let target =
63            MinimumAxiomSet::new(num_sentences, (0..num_sentences).collect(), implications);
64
65        ReductionXC3SToMinimumAxiomSet {
66            target,
67            source_universe_size: universe_size,
68            source_num_subsets: num_subsets,
69        }
70    }
71}
72
73#[cfg(feature = "example-db")]
74pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
75    use crate::export::SolutionPair;
76
77    vec![crate::example_db::specs::RuleExampleSpec {
78        id: "exactcoverby3sets_to_minimumaxiomset",
79        build: || {
80            let source = ExactCoverBy3Sets::new(
81                6,
82                vec![[0, 1, 2], [0, 3, 4], [2, 4, 5], [1, 3, 5], [0, 2, 4]],
83            );
84            crate::example_db::specs::rule_example_with_witness::<_, MinimumAxiomSet>(
85                source,
86                SolutionPair {
87                    source_config: vec![0, 0, 0, 1, 1],
88                    target_config: vec![0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1],
89                },
90            )
91        },
92    }]
93}
94
95#[cfg(test)]
96#[path = "../unit_tests/rules/exactcoverby3sets_minimumaxiomset.rs"]
97mod tests;
problemreductions/rules/exactcoverby3sets_minimumaxiomset.rs

problemreductions/rules/
exactcoverby3sets_minimumaxiomset.rs
