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

problemreductions/models/formula/
nae_satisfiability.rs
