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::traits::{ReduceTo, ReductionResult};
13
14/// Result of reducing Satisfiability to NAE-Satisfiability.
15#[derive(Debug, Clone)]
16pub struct ReductionSATToNAESAT {
17    /// Number of original variables in the source problem.
18    source_num_vars: usize,
19    /// The target NAE-SAT problem.
20    target: NAESatisfiability,
21}
22
23impl ReductionResult for ReductionSATToNAESAT {
24    type Source = Satisfiability;
25    type Target = NAESatisfiability;
26
27    fn target_problem(&self) -> &Self::Target {
28        &self.target
29    }
30
31    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
32        let n = self.source_num_vars;
33        if target_solution.len() <= n {
34            return vec![0; n];
35        }
36        // The sentinel variable is the last variable (index n).
37        let sentinel_value = target_solution[n];
38        if sentinel_value == 0 {
39            // Sentinel is false: return first n variables as-is.
40            target_solution[..n].to_vec()
41        } else {
42            // Sentinel is true: return complement of first n variables.
43            target_solution[..n].iter().map(|&v| 1 - v).collect()
44        }
45    }
46}
47
48#[reduction(overhead = {
49    num_vars = "num_vars + 1",
50    num_clauses = "num_clauses",
51    num_literals = "num_literals + num_clauses",
52})]
53impl ReduceTo<NAESatisfiability> for Satisfiability {
54    type Result = ReductionSATToNAESAT;
55
56    fn reduce_to(&self) -> Self::Result {
57        let n = self.num_vars();
58        // Sentinel variable has 0-indexed position n, so its 1-indexed literal is n+1.
59        let sentinel_lit = (n + 1) as i32;
60
61        let nae_clauses: Vec<CNFClause> = self
62            .clauses()
63            .iter()
64            .map(|clause| {
65                if clause.literals.is_empty() {
66                    // SAT allows empty clauses, which make the instance unsatisfiable.
67                    // Map to a fixed unsatisfiable NAE clause (s, s) of length 2.
68                    CNFClause::new(vec![sentinel_lit, sentinel_lit])
69                } else {
70                    let mut lits = clause.literals.clone();
71                    lits.push(sentinel_lit);
72                    CNFClause::new(lits)
73                }
74            })
75            .collect();
76
77        let target = NAESatisfiability::new(n + 1, nae_clauses);
78
79        ReductionSATToNAESAT {
80            source_num_vars: n,
81            target,
82        }
83    }
84}
85
86#[cfg(feature = "example-db")]
87pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
88    use crate::export::SolutionPair;
89
90    vec![crate::example_db::specs::RuleExampleSpec {
91        id: "satisfiability_to_naesatisfiability",
92        build: || {
93            let source = Satisfiability::new(
94                3,
95                vec![
96                    CNFClause::new(vec![1, 2]),
97                    CNFClause::new(vec![-1, 3]),
98                    CNFClause::new(vec![-2, -3]),
99                ],
100            );
101            crate::example_db::specs::rule_example_with_witness::<_, NAESatisfiability>(
102                source,
103                SolutionPair {
104                    source_config: vec![0, 1, 0],
105                    target_config: vec![0, 1, 0, 0],
106                },
107            )
108        },
109    }]
110}
111
112#[cfg(test)]
113#[path = "../unit_tests/rules/satisfiability_naesatisfiability.rs"]
114mod tests;
problemreductions/rules/satisfiability_naesatisfiability.rs

problemreductions/rules/
satisfiability_naesatisfiability.rs
