Fix #143: [Model] NAESatisfiability

docs/paper/reductions.typ

@@ -92,6 +92,7 @@
   "Knapsack": [Knapsack],
   "PartiallyOrderedKnapsack": [Partially Ordered Knapsack],
   "Satisfiability": [SAT],
+  "NAESatisfiability": [NAE-SAT],
   "KSatisfiability": [$k$-SAT],
   "CircuitSAT": [CircuitSAT],
   "ConjunctiveQueryFoldability": [Conjunctive Query Foldability],
@@ -2396,6 +2397,29 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76],
   ]
 }
 
+#{
+  let x = load-model-example("NAESatisfiability")
+  let n = x.instance.num_vars
+  let m = x.instance.clauses.len()
+  let clauses = x.instance.clauses
+  let sol = (config: x.optimal_config, metric: x.optimal_value)
+  let assign = sol.config
+  let complement = assign.map(v => 1 - v)
+  let fmt-lit(l) = if l > 0 { $x_#l$ } else { $not x_#(-l)$ }
+  let fmt-clause(c) = $paren.l #c.literals.map(fmt-lit).join($or$) paren.r$
+  let eval-lit(l) = if l > 0 { assign.at(l - 1) } else { 1 - assign.at(-l - 1) }
+  let clause-values(c) = c.literals.map(l => str(eval-lit(l)))
+  [
+    #problem-def("NAESatisfiability")[
+      Given a CNF formula $phi = and.big_(j=1)^m C_j$ with $m$ clauses over $n$ Boolean variables, where each clause $C_j = or.big_i ell_(j i)$ is a disjunction of literals, find an assignment $bold(x) in {0, 1}^n$ such that every clause contains at least one true literal and at least one false literal.
+    ][
+    Not-All-Equal Satisfiability (NAE-SAT) is a canonical variant in Schaefer's dichotomy theorem @schaefer1978. Unlike ordinary SAT, each clause forbids the all-true and all-false patterns, giving the problem a complement symmetry: if an assignment is NAE-satisfying, then flipping every bit is also NAE-satisfying. This makes NAE-SAT a natural intermediate for cut and partition reductions such as Max-Cut. A straightforward exact algorithm enumerates all $2^n$ assignments; complement symmetry can halve the search space in practice by fixing one variable, but the asymptotic worst-case bound remains $O^*(2^n)$.
+
+    *Example.* Consider $phi = #clauses.map(fmt-clause).join($and$)$ with $n = #n$ variables and $m = #m$ clauses. The assignment $(#range(n).map(i => $x_#(i + 1)$).join(",")) = (#assign.map(v => str(v)).join(", "))$ is NAE-satisfying because each clause evaluates to a tuple containing both $0$ and $1$: #clauses.enumerate().map(((j, c)) => $C_#(j + 1) = paren.l #clause-values(c).join(", ") paren.r$).join(", "). The complementary assignment $(#range(n).map(i => $x_#(i + 1)$).join(",")) = (#complement.map(v => str(v)).join(", "))$ is therefore also NAE-satisfying, illustrating the paired-solution structure characteristic of NAE-SAT.
+    ]
+  ]
+}
+
 #{
   let x = load-model-example("KSatisfiability")
   let n = x.instance.num_vars

problemreductions-cli/src/cli.rs

@@ -219,7 +219,8 @@ Flags by problem type:
   MaxCut, MaxMatching, TSP        --graph, --edge-weights
   ShortestWeightConstrainedPath   --graph, --edge-lengths, --edge-weights, --source-vertex, --target-vertex, --length-bound, --weight-bound
   MaximalIS                       --graph, --weights
-  SAT, KSAT                       --num-vars, --clauses [--k]
+  SAT, NAESAT                     --num-vars, --clauses
+  KSAT                            --num-vars, --clauses [--k]
   QUBO                            --matrix
   SpinGlass                       --graph, --couplings, --fields
   KColoring                       --graph, --k

problemreductions-cli/src/commands/create.rs

@@ -413,6 +413,7 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str {
             "--graph 0-1,1-2,2-3 --potential-edges 0-2:3,0-3:4,1-3:2 --budget 5"
         }
         "Satisfiability" => "--num-vars 3 --clauses \"1,2;-1,3\"",
+        "NAESatisfiability" => "--num-vars 3 --clauses \"1,2,-3;-1,2,3\"",
         "QuantifiedBooleanFormulas" => {
             "--num-vars 3 --clauses \"1,2;-1,3\" --quantifiers \"E,A,E\""
         }
@@ -1389,6 +1390,19 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> {
                 resolved_variant.clone(),
             )
         }
+        "NAESatisfiability" => {
+            let num_vars = args.num_vars.ok_or_else(|| {
+                anyhow::anyhow!(
+                    "NAESatisfiability requires --num-vars\n\n\
+                     Usage: pred create NAESAT --num-vars 3 --clauses \"1,2,-3;-1,2,3\""
+                )
+            })?;
+            let clauses = parse_clauses(args)?;
+            (
+                ser(NAESatisfiability::try_new(num_vars, clauses).map_err(anyhow::Error::msg)?)?,
+                resolved_variant.clone(),
+            )
+        }
         "KSatisfiability" => {
             let num_vars = args.num_vars.ok_or_else(|| {
                 anyhow::anyhow!(

src/lib.rs

@@ -44,7 +44,8 @@ pub mod prelude {
     // Problem types
     pub use crate::models::algebraic::{QuadraticAssignment, BMF, QUBO};
     pub use crate::models::formula::{
-        CNFClause, CircuitSAT, KSatisfiability, QuantifiedBooleanFormulas, Satisfiability,
+        CNFClause, CircuitSAT, KSatisfiability, NAESatisfiability, QuantifiedBooleanFormulas,
+        Satisfiability,
     };
     pub use crate::models::graph::{
         BalancedCompleteBipartiteSubgraph, BicliqueCover, BiconnectivityAugmentation,

src/models/formula/mod.rs

@@ -2,24 +2,28 @@
 //!
 //! Problems whose input is a boolean formula or circuit:
 //! - [`Satisfiability`]: Boolean satisfiability (SAT) with CNF clauses
+//! - [`NAESatisfiability`]: Not-All-Equal satisfiability with CNF clauses
 //! - [`KSatisfiability`]: K-SAT where each clause has exactly K literals
 //! - [`CircuitSAT`]: Boolean circuit satisfiability
 //! - [`QuantifiedBooleanFormulas`]: Quantified Boolean Formulas (QBF) — PSPACE-complete
 
 pub(crate) mod circuit;
 pub(crate) mod ksat;
+pub(crate) mod nae_satisfiability;
 pub(crate) mod qbf;
 pub(crate) mod sat;
 
 pub use circuit::{Assignment, BooleanExpr, BooleanOp, Circuit, CircuitSAT};
 pub use ksat::KSatisfiability;
+pub use nae_satisfiability::NAESatisfiability;
 pub use qbf::{QuantifiedBooleanFormulas, Quantifier};
 pub use sat::{CNFClause, Satisfiability};
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
     let mut specs = Vec::new();
     specs.extend(sat::canonical_model_example_specs());
+    specs.extend(nae_satisfiability::canonical_model_example_specs());
     specs.extend(ksat::canonical_model_example_specs());
     specs.extend(circuit::canonical_model_example_specs());
     specs.extend(qbf::canonical_model_example_specs());

src/models/formula/nae_satisfiability.rs

@@ -0,0 +1,208 @@
+//! Not-All-Equal Boolean Satisfiability (NAE-SAT) problem implementation.
+//!
+//! NAE-SAT asks whether a CNF formula has an assignment such that each clause
+//! contains at least one true literal and at least one false literal.
+
+use crate::registry::{FieldInfo, ProblemSchemaEntry};
+use crate::traits::{Problem, SatisfactionProblem};
+use serde::{Deserialize, Serialize};
+
+use super::CNFClause;
+
+inventory::submit! {
+    ProblemSchemaEntry {
+        name: "NAESatisfiability",
+        display_name: "Not-All-Equal Satisfiability",
+        aliases: &["NAESAT"],
+        dimensions: &[],
+        module_path: module_path!(),
+        description: "Find an assignment where every CNF clause has both a true and a false literal",
+        fields: &[
+            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
+            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "Clauses in conjunctive normal form with at least two literals each" },
+        ],
+    }
+}
+
+/// Not-All-Equal Boolean Satisfiability (NAE-SAT) in CNF form.
+///
+/// Given a Boolean formula in conjunctive normal form (CNF), determine whether
+/// there exists an assignment such that every clause contains at least one
+/// true literal and at least one false literal.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+#[serde(try_from = "NAESatisfiabilityDef")]
+pub struct NAESatisfiability {
+    /// Number of variables.
+    num_vars: usize,
+    /// Clauses in CNF, each with at least two literals.
+    clauses: Vec<CNFClause>,
+}
+
+impl NAESatisfiability {
+    /// Create a new NAE-SAT problem.
+    ///
+    /// # Panics
+    /// Panics if any clause has fewer than two literals.
+    pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
+        Self::try_new(num_vars, clauses).unwrap_or_else(|err| panic!("{err}"))
+    }
+
+    /// Create a new NAE-SAT problem, returning an error instead of panicking
+    /// when a clause has fewer than two literals.
+    pub fn try_new(num_vars: usize, clauses: Vec<CNFClause>) -> Result<Self, String> {
+        validate_clause_lengths(&clauses)?;
+        Ok(Self { num_vars, clauses })
+    }
+
+    /// Get the number of variables.
+    pub fn num_vars(&self) -> usize {
+        self.num_vars
+    }
+
+    /// Get the number of clauses.
+    pub fn num_clauses(&self) -> usize {
+        self.clauses.len()
+    }
+
+    /// Get the total number of literal occurrences across all clauses.
+    pub fn num_literals(&self) -> usize {
+        self.clauses.iter().map(|c| c.len()).sum()
+    }
+
+    /// Get the clauses.
+    pub fn clauses(&self) -> &[CNFClause] {
+        &self.clauses
+    }
+
+    /// Get a specific clause.
+    pub fn get_clause(&self, index: usize) -> Option<&CNFClause> {
+        self.clauses.get(index)
+    }
+
+    /// Count how many clauses satisfy the NAE condition under an assignment.
+    pub fn count_nae_satisfied(&self, assignment: &[bool]) -> usize {
+        self.clauses
+            .iter()
+            .filter(|clause| Self::clause_is_nae_satisfied(clause, assignment))
+            .count()
+    }
+
+    /// Check whether all clauses satisfy the NAE condition under an assignment.
+    pub fn is_nae_satisfying(&self, assignment: &[bool]) -> bool {
+        self.clauses
+            .iter()
+            .all(|clause| Self::clause_is_nae_satisfied(clause, assignment))
+    }
+
+    /// Check if a solution (config) is valid.
+    pub fn is_valid_solution(&self, config: &[usize]) -> bool {
+        self.evaluate(config)
+    }
+
+    fn config_to_assignment(config: &[usize]) -> Vec<bool> {
+        config.iter().map(|&v| v == 1).collect()
+    }
+
+    fn literal_value(lit: i32, assignment: &[bool]) -> bool {
+        let var = lit.unsigned_abs() as usize - 1;
+        let value = assignment.get(var).copied().unwrap_or(false);
+        if lit > 0 {
+            value
+        } else {
+            !value
+        }
+    }
+
+    fn clause_is_nae_satisfied(clause: &CNFClause, assignment: &[bool]) -> bool {
+        let mut has_true = false;
+        let mut has_false = false;
+
+        for &lit in &clause.literals {
+            if Self::literal_value(lit, assignment) {
+                has_true = true;
+            } else {
+                has_false = true;
+            }
+
+            if has_true && has_false {
+                return true;
+            }
+        }
+
+        false
+    }
+}
+
+impl Problem for NAESatisfiability {
+    const NAME: &'static str = "NAESatisfiability";
+    type Metric = bool;
+
+    fn dims(&self) -> Vec<usize> {
+        vec![2; self.num_vars]
+    }
+
+    fn evaluate(&self, config: &[usize]) -> bool {
+        let assignment = Self::config_to_assignment(config);
+        self.is_nae_satisfying(&assignment)
+    }
+
+    fn variant() -> Vec<(&'static str, &'static str)> {
+        crate::variant_params![]
+    }
+}
+
+impl SatisfactionProblem for NAESatisfiability {}
+
+crate::declare_variants! {
+    default sat NAESatisfiability => "2^num_variables",
+}
+
+#[derive(Debug, Clone, Deserialize)]
+struct NAESatisfiabilityDef {
+    num_vars: usize,
+    clauses: Vec<CNFClause>,
+}
+
+impl TryFrom<NAESatisfiabilityDef> for NAESatisfiability {
+    type Error = String;
+
+    fn try_from(value: NAESatisfiabilityDef) -> Result<Self, Self::Error> {
+        Self::try_new(value.num_vars, value.clauses)
+    }
+}
+
+fn validate_clause_lengths(clauses: &[CNFClause]) -> Result<(), String> {
+    for (index, clause) in clauses.iter().enumerate() {
+        if clause.len() < 2 {
+            return Err(format!(
+                "Clause {} has {} literals, expected at least 2",
+                index,
+                clause.len()
+            ));
+        }
+    }
+    Ok(())
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
+    vec![crate::example_db::specs::ModelExampleSpec {
+        id: "nae_satisfiability",
+        instance: Box::new(NAESatisfiability::new(
+            5,
+            vec![
+                CNFClause::new(vec![1, 2, -3]),
+                CNFClause::new(vec![-1, 3, 4]),
+                CNFClause::new(vec![2, -4, 5]),
+                CNFClause::new(vec![-2, 3, -5]),
+                CNFClause::new(vec![1, -3, 5]),
+            ],
+        )),
+        optimal_config: vec![0, 0, 0, 1, 1],
+        optimal_value: serde_json::json!(true),
+    }]
+}
+
+#[cfg(test)]
+#[path = "../../unit_tests/models/formula/nae_satisfiability.rs"]
+mod tests;

src/models/mod.rs

@@ -14,7 +14,8 @@ pub use algebraic::{
     QuadraticAssignment, BMF, ILP, QUBO,
 };
 pub use formula::{
-    CNFClause, CircuitSAT, KSatisfiability, QuantifiedBooleanFormulas, Quantifier, Satisfiability,
+    CNFClause, CircuitSAT, KSatisfiability, NAESatisfiability, QuantifiedBooleanFormulas,
+    Quantifier, Satisfiability,
 };
 pub use graph::{
     BalancedCompleteBipartiteSubgraph, BicliqueCover, BiconnectivityAugmentation,