problemreductions/rules/
naesatisfiability_setsplitting.rs

1//! Reduction from NAE-Satisfiability to Set Splitting.
2//!
3//! Create one universe element for each positive literal `x_i` and one for each
4//! negative literal `¬x_i`. Add a 2-element subset `{x_i, ¬x_i}` for every
5//! variable to force opposite colors. Each clause becomes a subset of its
6//! literal-elements, so non-monochromatic subsets correspond exactly to
7//! not-all-equal clauses.
8
9use crate::models::formula::NAESatisfiability;
10use crate::models::set::SetSplitting;
11use crate::reduction;
12use crate::rules::traits::{ReduceTo, ReductionResult};
13
14#[derive(Debug, Clone)]
15pub struct ReductionNAESATToSetSplitting {
16    target: SetSplitting,
17    num_source_variables: usize,
18}
19
20impl ReductionResult for ReductionNAESATToSetSplitting {
21    type Source = NAESatisfiability;
22    type Target = SetSplitting;
23
24    fn target_problem(&self) -> &SetSplitting {
25        &self.target
26    }
27
28    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
29        assert!(
30            target_solution.len() >= self.num_source_variables,
31            "SetSplitting solution has {} variables but source requires {}",
32            target_solution.len(),
33            self.num_source_variables,
34        );
35        target_solution[..self.num_source_variables].to_vec()
36    }
37}
38
39fn literal_element_index(lit: i32, num_vars: usize) -> usize {
40    let var_index = lit.unsigned_abs() as usize - 1;
41    if lit > 0 {
42        var_index
43    } else {
44        num_vars + var_index
45    }
46}
47
48#[reduction(
49    overhead = {
50        universe_size = "2 * num_vars",
51        num_subsets = "num_vars + num_clauses",
52    }
53)]
54impl ReduceTo<SetSplitting> for NAESatisfiability {
55    type Result = ReductionNAESATToSetSplitting;
56
57    fn reduce_to(&self) -> Self::Result {
58        let num_vars = self.num_vars();
59        let mut subsets = Vec::with_capacity(num_vars + self.num_clauses());
60
61        for var_index in 0..num_vars {
62            subsets.push(vec![var_index, num_vars + var_index]);
63        }
64
65        for clause in self.clauses() {
66            subsets.push(
67                clause
68                    .literals
69                    .iter()
70                    .map(|&lit| literal_element_index(lit, num_vars))
71                    .collect(),
72            );
73        }
74
75        ReductionNAESATToSetSplitting {
76            target: SetSplitting::new(2 * num_vars, subsets),
77            num_source_variables: num_vars,
78        }
79    }
80}
81
82#[cfg(feature = "example-db")]
83pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
84    use crate::export::SolutionPair;
85    use crate::models::formula::CNFClause;
86
87    vec![crate::example_db::specs::RuleExampleSpec {
88        id: "naesatisfiability_to_setsplitting",
89        build: || {
90            crate::example_db::specs::rule_example_with_witness::<_, SetSplitting>(
91                NAESatisfiability::new(
92                    3,
93                    vec![
94                        CNFClause::new(vec![1, -2, 3]),
95                        CNFClause::new(vec![-1, 2, -3]),
96                    ],
97                ),
98                SolutionPair {
99                    source_config: vec![1, 1, 1],
100                    target_config: vec![1, 1, 1, 0, 0, 0],
101                },
102            )
103        },
104    }]
105}
106
107#[cfg(test)]
108#[path = "../unit_tests/rules/naesatisfiability_setsplitting.rs"]
109mod tests;
problemreductions/rules/naesatisfiability_setsplitting.rs

problemreductions/rules/
naesatisfiability_setsplitting.rs
