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(
29        &self,
30        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
31    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
32        crate::rules::traits::validate_target_witness(
33            self.target_problem(),
34            target_solution,
35            |value| value.0,
36            "target witness does not satisfy the target problem",
37        )?;
38
39        Ok(target_solution[..self.num_source_variables].to_vec())
40    }
41}
42
43fn literal_element_index(lit: i64, num_vars: usize) -> usize {
44    let var_index = lit.unsigned_abs() as usize - 1;
45    if lit > 0 {
46        var_index
47    } else {
48        num_vars + var_index
49    }
50}
51
52#[crate::aggregate_reduction(identity)]
53impl crate::rules::AggregateReductionResult for ReductionNAESATToSetSplitting {}
54
55#[reduction(
56    transform = exact {
57        universe_size = "2 * num_vars",
58        num_subsets = "num_vars + num_clauses",
59    }
60)]
61impl ReduceTo<SetSplitting> for NAESatisfiability {
62    type Result = ReductionNAESATToSetSplitting;
63
64    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
65        let num_vars = self.num_vars();
66        let mut subsets = Vec::with_capacity(num_vars + self.num_clauses());
67
68        for var_index in 0..num_vars {
69            subsets.push(vec![var_index, num_vars + var_index]);
70        }
71
72        for clause in self.clauses() {
73            subsets.push(
74                clause
75                    .literals
76                    .iter()
77                    .map(|&lit| literal_element_index(lit, num_vars))
78                    .collect(),
79            );
80        }
81
82        Ok(ReductionNAESATToSetSplitting {
83            target: SetSplitting::new(2 * num_vars, subsets),
84            num_source_variables: num_vars,
85        })
86    }
87}
88
89#[cfg(feature = "example-db")]
90pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
91    use crate::export::SolutionPair;
92    use crate::models::formula::CNFClause;
93
94    vec![crate::example_db::specs::RuleExampleSpec {
95        id: "naesatisfiability_to_setsplitting",
96        build: || {
97            crate::example_db::specs::rule_example_with_witness::<_, SetSplitting>(
98                NAESatisfiability::new(
99                    3,
100                    vec![
101                        CNFClause::new(vec![1, -2, 3]),
102                        CNFClause::new(vec![-1, 2, -3]),
103                    ],
104                ),
105                SolutionPair {
106                    source_config: serde_json::json!(vec![true, true, true]),
107                    target_config: serde_json::json!(vec![true, true, true, false, false, false]),
108                },
109            )
110        },
111    }]
112}
113
114#[cfg(test)]
115#[path = "../unit_tests/rules/naesatisfiability_setsplitting.rs"]
116mod tests;
problemreductions/rules/naesatisfiability_setsplitting.rs

problemreductions/rules/
naesatisfiability_setsplitting.rs
