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_solution(self.target_problem(), target_solution)?;
37
38        let n = self.source_num_vars;
39        if target_solution.len() != n + 1 {
40            return Err(crate::rules::ExtractionError::invalid(format!(
41                "expected {} target truth values, got {}",
42                n + 1,
43                target_solution.len()
44            )));
45        }
46        let sentinel = target_solution[n];
47        Ok(target_solution[..n]
48            .iter()
49            .map(|&value| value ^ sentinel)
50            .collect())
51    }
52}
53
54#[reduction(
55    transform = exact {
56        num_vars = "num_vars + 1",
57        num_clauses = "num_clauses",
58        num_literals = "num_literals + num_clauses",
59    },
60    unavailable = {
61        num_literal_pairs = "the exact target parameter is not represented by this reduction's symbolic transform",
62    }
63)]
64impl ReduceTo<NAESatisfiability> for Satisfiability {
65    type Result = ReductionSATToNAESAT;
66
67    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
68        let n = self.num_vars();
69        let mut variables = SatVariableAllocator::new("Satisfiability -> NAESatisfiability", n)
70            .map_err(
71                crate::rules::ReductionError::construction::<Satisfiability, NAESatisfiability>,
72            )?;
73        let sentinel_lit = variables.allocate().map_err(
74            crate::rules::ReductionError::construction::<Satisfiability, NAESatisfiability>,
75        )?;
76
77        let nae_clauses: Vec<CNFClause> = self
78            .clauses()
79            .iter()
80            .map(|clause| {
81                if clause.literals.is_empty() {
82                    // SAT allows empty clauses, which make the instance unsatisfiable.
83                    // Map to a fixed unsatisfiable NAE clause (s, s) of length 2.
84                    CNFClause::new(vec![sentinel_lit, sentinel_lit])
85                } else {
86                    let mut lits = clause.literals.clone();
87                    lits.push(sentinel_lit);
88                    CNFClause::new(lits)
89                }
90            })
91            .collect();
92
93        let target = NAESatisfiability::new(variables.num_vars(), nae_clauses);
94
95        Ok(ReductionSATToNAESAT {
96            source_num_vars: n,
97            target,
98        })
99    }
100}
101
102#[cfg(feature = "example-db")]
103pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
104    use crate::export::SolutionPair;
105
106    vec![crate::example_db::specs::RuleExampleSpec {
107        id: "satisfiability_to_naesatisfiability",
108        build: || {
109            let source = Satisfiability::new(
110                3,
111                vec![
112                    CNFClause::new(vec![1, 2]),
113                    CNFClause::new(vec![-1, 3]),
114                    CNFClause::new(vec![-2, -3]),
115                ],
116            );
117            crate::example_db::specs::rule_example_with_witness::<_, NAESatisfiability>(
118                source,
119                SolutionPair {
120                    source_config: serde_json::json!(vec![false, true, false]),
121                    target_config: serde_json::json!(vec![false, true, false, false]),
122                },
123            )
124        },
125    }]
126}
127
128#[cfg(test)]
129#[path = "../unit_tests/rules/satisfiability_naesatisfiability.rs"]
130mod tests;
problemreductions/rules/satisfiability_naesatisfiability.rs

problemreductions/rules/
satisfiability_naesatisfiability.rs
