problemreductions/rules/
satisfiability_naesatisfiability.rs

1//! Reduction from Satisfiability to NAE-Satisfiability.
2//!
3//! Given a SAT instance with n variables and m clauses, we construct an
4//! equisatisfiable NAE-SAT instance by adding a fresh sentinel variable s.
5//! Each SAT clause C_j = (l_1 ∨ ... ∨ l_k) becomes NAE clause
6//! C'_j = (l_1, ..., l_k, s). The sentinel ensures that each NAE clause
7//! has at least one false literal (the sentinel itself when s=false, or
8//! the complement of the original satisfied literal when s=true).
9
10use crate::models::formula::{CNFClause, NAESatisfiability, Satisfiability};
11use crate::reduction;
12use crate::rules::sat_helpers::SatVariableAllocator;
13use crate::rules::traits::{ReduceTo, ReductionResult};
14
15/// Result of reducing Satisfiability to NAE-Satisfiability.
16#[derive(Debug, Clone)]
17pub struct ReductionSATToNAESAT {
18    /// Number of original variables in the source problem.
19    source_num_vars: usize,
20    /// The target NAE-SAT problem.
21    target: NAESatisfiability,
22}
23
24impl ReductionResult for ReductionSATToNAESAT {
25    type Source = Satisfiability;
26    type Target = NAESatisfiability;
27
28    fn target_problem(&self) -> &Self::Target {
29        &self.target
30    }
31
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| value.0,
40            "target assignment does not satisfy NAE clauses",
41        )?;
42
43        let n = self.source_num_vars;
44        let sentinel = target_solution[n];
45        Ok(target_solution[..n]
46            .iter()
47            .map(|&value| value ^ sentinel)
48            .collect())
49    }
50}
51
52#[crate::aggregate_reduction(identity)]
53impl crate::rules::AggregateReductionResult for ReductionSATToNAESAT {}
54
55#[reduction(transform = {
56    exact {
57        num_vars = "num_vars + 1",
58        num_clauses = "num_clauses",
59    },
60    upper_bound {
61        // Nonempty clauses add one fresh sentinel; empty clauses use (s,s).
62        num_clause_variables = "num_literals + num_clauses",
63        num_literals = "num_literals + 2 * num_clauses",
64        // Nonempty length l contributes l(l+1)/2; an empty clause contributes
65        // one pair. Sum l^2 <= (sum l)^2, including repeated literals.
66        num_literal_pairs = "num_literals * (num_literals + 1) / 2 + num_clauses",
67    },
68})]
69impl ReduceTo<NAESatisfiability> for Satisfiability {
70    type Result = ReductionSATToNAESAT;
71
72    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
73        let n = self.num_vars();
74        let mut variables = SatVariableAllocator::new("Satisfiability -> NAESatisfiability", n)
75            .map_err(
76                crate::rules::ReductionError::construction::<Satisfiability, NAESatisfiability>,
77            )?;
78        let sentinel_lit = variables.allocate().map_err(
79            crate::rules::ReductionError::construction::<Satisfiability, NAESatisfiability>,
80        )?;
81
82        let nae_clauses: Vec<CNFClause> = self
83            .clauses()
84            .iter()
85            .map(|clause| {
86                if clause.literals.is_empty() {
87                    // SAT allows empty clauses, which make the instance unsatisfiable.
88                    // Map to a fixed unsatisfiable NAE clause (s, s) of length 2.
89                    CNFClause::new(vec![sentinel_lit, sentinel_lit])
90                } else {
91                    let mut lits = clause.literals.clone();
92                    lits.push(sentinel_lit);
93                    CNFClause::new(lits)
94                }
95            })
96            .collect();
97
98        let target = NAESatisfiability::new(variables.num_vars(), nae_clauses);
99
100        Ok(ReductionSATToNAESAT {
101            source_num_vars: n,
102            target,
103        })
104    }
105}
106
107#[cfg(feature = "example-db")]
108pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
109    use crate::export::SolutionPair;
110
111    vec![crate::example_db::specs::RuleExampleSpec {
112        id: "satisfiability_to_naesatisfiability",
113        build: || {
114            let source = Satisfiability::new(
115                3,
116                vec![
117                    CNFClause::new(vec![1, 2]),
118                    CNFClause::new(vec![-1, 3]),
119                    CNFClause::new(vec![-2, -3]),
120                ],
121            );
122            crate::example_db::specs::rule_example_with_witness::<_, NAESatisfiability>(
123                source,
124                SolutionPair {
125                    source_config: serde_json::json!(vec![false, true, false]),
126                    target_config: serde_json::json!(vec![false, true, false, false]),
127                },
128            )
129        },
130    }]
131}
132
133#[cfg(test)]
134#[path = "../unit_tests/rules/satisfiability_naesatisfiability.rs"]
135mod tests;
problemreductions/rules/satisfiability_naesatisfiability.rs

problemreductions/rules/
satisfiability_naesatisfiability.rs
