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    /// Sum of the distinct Boolean variables appearing in each clause.
78    ///
79    /// Signs and repeated occurrences do not change membership. Computing this
80    /// statistic takes expected linear time in the number of literal occurrences.
81    pub fn num_clause_variables(&self) -> usize {
82        self.clauses
83            .iter()
84            .map(|clause| {
85                clause
86                    .literals
87                    .iter()
88                    .map(|lit| lit.unsigned_abs())
89                    .collect::<std::collections::HashSet<_>>()
90                    .len()
91            })
92            .sum()
93    }
94
95    /// Get the total number of literal pairs across all clauses.
96    ///
97    /// For each clause with k literals, this contributes C(k,2) = k*(k-1)/2 pairs.
98    pub fn num_literal_pairs(&self) -> usize {
99        self.clauses
100            .iter()
101            .map(|c| c.len() * (c.len() - 1) / 2)
102            .sum()
103    }
104
105    /// Get the clauses.
106    pub fn clauses(&self) -> &[CNFClause] {
107        &self.clauses
108    }
109
110    /// Get a specific clause.
111    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
112        self.clauses.get(index)
113    }
114
115    /// Count how many clauses satisfy the NAE condition under an assignment.
116    pub fn count_nae_satisfied(
117        &self,
118        assignment: &[bool],
119    ) -> Result<i64, crate::traits::EvaluationError> {
120        let count = self
121            .clauses
122            .iter()
123            .filter(|clause| Self::clause_is_nae_satisfied(clause, assignment))
124            .count();
125        i64::try_from(count).map_err(|_| {
126            crate::traits::EvaluationError::IntegerOverflow(
127                "converting NAE-satisfied-clause count to i64".into(),
128            )
129        })
130    }
131
132    /// Check whether all clauses satisfy the NAE condition under an assignment.
133    pub fn is_nae_satisfying(&self, assignment: &[bool]) -> bool {
134        self.clauses
135            .iter()
136            .all(|clause| Self::clause_is_nae_satisfied(clause, assignment))
137    }
138
139    /// Check if a solution (config) is valid.
140    pub fn is_valid_solution(
141        &self,
142        config: &[bool],
143    ) -> Result<bool, crate::traits::EvaluationError> {
144        if config.len() != self.num_vars {
145            return Err(crate::traits::EvaluationError::InvalidConfiguration(
146                "assignment length does not match the formula variables".into(),
147            ));
148        }
149        Ok(self.is_nae_satisfying(config))
150    }
151
152    fn literal_value(lit: i64, assignment: &[bool]) -> bool {
153        let var = lit.unsigned_abs() as usize - 1;
154        let value = assignment.get(var).copied().unwrap_or(false);
155        if lit > 0 {
156            value
157        } else {
158            !value
159        }
160    }
161
162    fn clause_is_nae_satisfied(clause: &CNFClause, assignment: &[bool]) -> bool {
163        let mut has_true = false;
164        let mut has_false = false;
165
166        for &lit in &clause.literals {
167            if Self::literal_value(lit, assignment) {
168                has_true = true;
169            } else {
170                has_false = true;
171            }
172
173            if has_true && has_false {
174                return true;
175            }
176        }
177
178        false
179    }
180}
181
182impl Problem for NAESatisfiability {
183    const NAME: &'static str = "NAESatisfiability";
184    type Solution = Vec<bool>;
185    type Value = crate::types::Or;
186
187    crate::problem_parameters![
188        ("num_clauses", num_clauses),
189        ("num_clause_variables", num_clause_variables),
190        ("num_literal_pairs", num_literal_pairs),
191        ("num_literals", num_literals),
192        ("num_vars", num_vars),
193    ];
194
195    fn evaluate(
196        &self,
197        config: &Self::Solution,
198    ) -> Result<crate::types::Or, crate::traits::EvaluationError> {
199        Ok(crate::types::Or(self.is_valid_solution(config)?))
200    }
201
202    fn variant() -> Vec<(&'static str, &'static str)> {
203        crate::variant_params![]
204    }
205}
206
207impl crate::solvers::BruteForceProblem for NAESatisfiability {
208    fn dimensions(&self) -> Vec<usize> {
209        vec![2; self.num_vars]
210    }
211}
212
213crate::declare_variants! {
214    default NAESatisfiability => "2^num_vars",
215}
216
217crate::register_brute_force! {
218    NAESatisfiability decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
219}
220
221#[derive(Debug, Clone, Deserialize)]
222struct NAESatisfiabilityDef {
223    num_vars: usize,
224    clauses: Vec<CNFClause>,
225}
226
227impl TryFrom<NAESatisfiabilityDef> for NAESatisfiability {
228    type Error = crate::registry::ConstructionError;
229
230    fn try_from(value: NAESatisfiabilityDef) -> Result<Self, Self::Error> {
231        Self::try_new(value.num_vars, value.clauses)
232    }
233}
234
235fn validate_clause_lengths(
236    clauses: &[CNFClause],
237) -> Result<(), crate::registry::ConstructionError> {
238    for (index, clause) in clauses.iter().enumerate() {
239        if clause.len() < 2 {
240            return Err(format!(
241                "Clause {} has {} literals, expected at least 2",
242                index,
243                clause.len()
244            )
245            .into());
246        }
247    }
248    Ok(())
249}
250
251#[cfg(feature = "example-db")]
252pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
253    vec![crate::example_db::specs::ModelExampleSpec {
254        id: "nae_satisfiability",
255        instance: Box::new(NAESatisfiability::new(
256            5,
257            vec![
258                CNFClause::new(vec![1, 2, -3]),
259                CNFClause::new(vec![-1, 3, 4]),
260                CNFClause::new(vec![2, -4, 5]),
261                CNFClause::new(vec![-2, 3, -5]),
262                CNFClause::new(vec![1, -3, 5]),
263            ],
264        )),
265        optimal_config: serde_json::json!(vec![false, false, false, true, true]),
266        optimal_value: serde_json::json!(true),
267    }]
268}
269
270#[cfg(test)]
271#[path = "../../unit_tests/models/formula/nae_satisfiability.rs"]
272mod tests;
problemreductions/models/formula/nae_satisfiability.rs

problemreductions/models/formula/
nae_satisfiability.rs
