problemreductions/models/formula/
nae_satisfiability.rs

1//! Not-All-Equal Boolean Satisfiability (NAE-SAT) problem implementation.
2//!
3//! NAE-SAT asks whether a CNF formula has an assignment such that each clause
4//! contains at least one true literal and at least one false literal.
5
6use crate::registry::{FieldInfo, ProblemSchemaEntry};
7use crate::traits::Problem;
8use serde::{Deserialize, Serialize};
9
10use super::CNFClause;
11
12inventory::submit! {
13    ProblemSchemaEntry {
14        name: "NAESatisfiability",
15        display_name: "Not-All-Equal Satisfiability",
16        aliases: &["NAESAT"],
17        dimensions: &[],
18        module_path: module_path!(),
19        description: "Find an assignment where every CNF clause has both a true and a false literal",
20        fields: &[
21            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
22            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Clauses in conjunctive normal form with at least two literals each" },
23        ],
24    }
25}
26
27/// Not-All-Equal Boolean Satisfiability (NAE-SAT) in CNF form.
28///
29/// Given a Boolean formula in conjunctive normal form (CNF), determine whether
30/// there exists an assignment such that every clause contains at least one
31/// true literal and at least one false literal.
32#[derive(Debug, Clone, Serialize, Deserialize)]
33#[serde(try_from = "NAESatisfiabilityDef")]
34pub struct NAESatisfiability {
35    /// Number of variables.
36    num_vars: usize,
37    /// Clauses in CNF, each with at least two literals.
38    clauses: Vec<CNFClause>,
39}
40
41impl NAESatisfiability {
42    /// Create a new NAE-SAT problem.
43    ///
44    /// # Panics
45    /// Panics if any clause has fewer than two literals.
46    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
47        Self::try_new(num_vars, clauses).unwrap_or_else(|err| panic!("{err}"))
48    }
49
50    /// Create a new NAE-SAT problem, returning an error instead of panicking
51    /// when a clause has fewer than two literals.
52    pub fn try_new(num_vars: usize, clauses: Vec<CNFClause>) -> Result<Self, String> {
53        validate_clause_lengths(&clauses)?;
54        Ok(Self { num_vars, clauses })
55    }
56
57    /// Get the number of variables.
58    pub fn num_vars(&self) -> usize {
59        self.num_vars
60    }
61
62    /// Get the number of clauses.
63    pub fn num_clauses(&self) -> usize {
64        self.clauses.len()
65    }
66
67    /// Get the total number of literal occurrences across all clauses.
68    pub fn num_literals(&self) -> usize {
69        self.clauses.iter().map(|c| c.len()).sum()
70    }
71
72    /// Get the total number of literal pairs across all clauses.
73    ///
74    /// For each clause with k literals, this contributes C(k,2) = k*(k-1)/2 pairs.
75    pub fn num_literal_pairs(&self) -> usize {
76        self.clauses
77            .iter()
78            .map(|c| c.len() * (c.len() - 1) / 2)
79            .sum()
80    }
81
82    /// Get the clauses.
83    pub fn clauses(&self) -> &[CNFClause] {
84        &self.clauses
85    }
86
87    /// Get a specific clause.
88    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
89        self.clauses.get(index)
90    }
91
92    /// Count how many clauses satisfy the NAE condition under an assignment.
93    pub fn count_nae_satisfied(&self, assignment: &[bool]) -> usize {
94        self.clauses
95            .iter()
96            .filter(|clause| Self::clause_is_nae_satisfied(clause, assignment))
97            .count()
98    }
99
100    /// Check whether all clauses satisfy the NAE condition under an assignment.
101    pub fn is_nae_satisfying(&self, assignment: &[bool]) -> bool {
102        self.clauses
103            .iter()
104            .all(|clause| Self::clause_is_nae_satisfied(clause, assignment))
105    }
106
107    /// Check if a solution (config) is valid.
108    pub fn is_valid_solution(&self, config: &[usize]) -> bool {
109        self.evaluate(config).0
110    }
111
112    fn literal_value(lit: i32, assignment: &[bool]) -> bool {
113        let var = lit.unsigned_abs() as usize - 1;
114        let value = assignment.get(var).copied().unwrap_or(false);
115        if lit > 0 {
116            value
117        } else {
118            !value
119        }
120    }
121
122    fn clause_is_nae_satisfied(clause: &CNFClause, assignment: &[bool]) -> bool {
123        let mut has_true = false;
124        let mut has_false = false;
125
126        for &lit in &clause.literals {
127            if Self::literal_value(lit, assignment) {
128                has_true = true;
129            } else {
130                has_false = true;
131            }
132
133            if has_true && has_false {
134                return true;
135            }
136        }
137
138        false
139    }
140}
141
142impl Problem for NAESatisfiability {
143    const NAME: &'static str = "NAESatisfiability";
144    type Value = crate::types::Or;
145
146    fn dims(&self) -> Vec<usize> {
147        vec![2; self.num_vars]
148    }
149
150    fn evaluate(&self, config: &[usize]) -> crate::types::Or {
151        crate::types::Or({
152            let assignment = super::config_to_assignment(config);
153            self.is_nae_satisfying(&assignment)
154        })
155    }
156
157    fn variant() -> Vec<(&'static str, &'static str)> {
158        crate::variant_params![]
159    }
160}
161
162crate::declare_variants! {
163    default NAESatisfiability => "2^num_variables",
164}
165
166#[derive(Debug, Clone, Deserialize)]
167struct NAESatisfiabilityDef {
168    num_vars: usize,
169    clauses: Vec<CNFClause>,
170}
171
172impl TryFrom<NAESatisfiabilityDef> for NAESatisfiability {
173    type Error = String;
174
175    fn try_from(value: NAESatisfiabilityDef) -> Result<Self, Self::Error> {
176        Self::try_new(value.num_vars, value.clauses)
177    }
178}
179
180fn validate_clause_lengths(clauses: &[CNFClause]) -> Result<(), String> {
181    for (index, clause) in clauses.iter().enumerate() {
182        if clause.len() < 2 {
183            return Err(format!(
184                "Clause {} has {} literals, expected at least 2",
185                index,
186                clause.len()
187            ));
188        }
189    }
190    Ok(())
191}
192
193#[cfg(feature = "example-db")]
194pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
195    vec![crate::example_db::specs::ModelExampleSpec {
196        id: "nae_satisfiability",
197        instance: Box::new(NAESatisfiability::new(
198            5,
199            vec![
200                CNFClause::new(vec![1, 2, -3]),
201                CNFClause::new(vec![-1, 3, 4]),
202                CNFClause::new(vec![2, -4, 5]),
203                CNFClause::new(vec![-2, 3, -5]),
204                CNFClause::new(vec![1, -3, 5]),
205            ],
206        )),
207        optimal_config: vec![0, 0, 0, 1, 1],
208        optimal_value: serde_json::json!(true),
209    }]
210}
211
212#[cfg(test)]
213#[path = "../../unit_tests/models/formula/nae_satisfiability.rs"]
214mod tests;
problemreductions/models/formula/nae_satisfiability.rs

problemreductions/models/formula/
nae_satisfiability.rs
