From 6c48987997a3fc0de1134e7e2b23e76bc847a25f Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sat, 21 Mar 2026 03:27:40 +0800 Subject: [PATCH 1/3] Add plan for #143: [Model] NAESatisfiability --- .../2026-03-21-nae-satisfiability-model.md | 253 ++++++++++++++++++ 1 file changed, 253 insertions(+) create mode 100644 docs/plans/2026-03-21-nae-satisfiability-model.md diff --git a/docs/plans/2026-03-21-nae-satisfiability-model.md b/docs/plans/2026-03-21-nae-satisfiability-model.md new file mode 100644 index 000000000..9e32f2c25 --- /dev/null +++ b/docs/plans/2026-03-21-nae-satisfiability-model.md @@ -0,0 +1,253 @@ +# NAESatisfiability Implementation Plan + +> **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task. + +**Goal:** Add the `NAESatisfiability` formula model, wire it into the registry/CLI/example-db/paper flows, and cover the issue’s worked example and NAE-specific semantics with tests. + +**Architecture:** Implement `NAESatisfiability` as a sibling of `Satisfiability`, reusing `CNFClause` but giving the model its own clause-evaluation logic: every clause must contain at least one true literal and at least one false literal. Keep the registration path fully registry-backed so the CLI, exports, and paper all discover the new model through the normal model/example mechanisms. + +**Tech Stack:** Rust workspace, serde, inventory registry, `declare_variants!`, cargo tests, Typst paper, GitHub issue `#143`. + +--- + +**Issue:** `#143` `[Model] NAESatisfiability` +**Implementation skill:** repo-local `add-model` +**Execution mode:** batch the paper work separately after the Rust implementation and example-db wiring are stable. + +## Information Checklist + +| # | Item | Value | +|---|------|-------| +| 1 | Problem name | `NAESatisfiability` | +| 2 | Mathematical definition | Given a CNF formula, find an assignment such that every clause has at least one true literal and at least one false literal | +| 3 | Problem type | Satisfaction (`Metric = bool`) | +| 4 | Type parameters | None | +| 5 | Struct fields | `num_vars: usize`, `clauses: Vec` | +| 6 | Configuration space | `vec![2; num_vars]` | +| 7 | Feasibility check | Convert config to Boolean assignment; each clause must contain both truth values among its literal occurrences | +| 8 | Objective function | `bool` | +| 9 | Best known exact algorithm | brute-force, issue gives `2^num_vars`; for `declare_variants!` use the repo’s accepted getter name (`2^num_variables` if `num_vars` is rejected at compile time) | +| 10 | Solving strategy | existing `BruteForce` solver | +| 11 | Category | `src/models/formula/` | +| 12 | Expected outcome | issue example assignment `[0, 0, 0, 1, 1]` is satisfying; complement `[1, 1, 1, 0, 0]` is also satisfying; total satisfying assignments = `10` | + +## Associated Rule Check + +- Existing cross-reference: GitHub issue `#382` `[Rule] NOT-ALL-EQUAL 3SAT to SET SPLITTING` +- Planned follow-ons in the issue body: `Satisfiability -> NAESatisfiability`, `NAESatisfiability -> MaxCut` +- Result: safe to proceed; this model is not an orphan. + +## Design Notes + +- Reuse [`src/models/formula/sat.rs`](/Users/jinguomini/rcode/problem-reductions/.worktrees/issue-143/src/models/formula/sat.rs) for the struct/registry/test pattern, but do not reuse `CNFClause::is_satisfied()` for model semantics. +- Add model-local helpers such as `count_nae_satisfied`, `is_nae_satisfying`, and a literal-evaluation helper that works on literal occurrences, not deduplicated variables. +- Enforce the issue schema invariant that each clause has at least two literals in the constructor. Empty formulas remain valid; empty or unit clauses inside a formula should be rejected at construction time. +- No new CLI flags should be necessary: existing `--num-vars` and `--clauses` are enough. +- CLI alias resolution is registry-backed in the current codebase, so prefer defining aliases in `ProblemSchemaEntry` over adding manual alias tables unless implementation proves otherwise. + +## Batch Plan + +- **Batch 1:** model implementation, registration, CLI create support, example-db, and Rust tests +- **Batch 2:** paper entry, paper-example alignment, final verification + +## Batch 1 + +### Task 1: Add failing model tests first + +**Files:** +- Create: `src/unit_tests/models/formula/nae_satisfiability.rs` + +**Step 1: Write the failing tests** + +Add tests that lock down the issue semantics before implementation: +- `test_nae_satisfiability_creation` +- `test_nae_clause_requires_true_and_false_literals` +- `test_nae_satisfying_example_from_issue` +- `test_nae_complement_symmetry_for_issue_example` +- `test_nae_solver_counts_ten_solutions_for_issue_example` +- `test_nae_empty_formula_is_trivially_satisfying` +- `test_nae_constructor_rejects_short_clauses` +- `test_nae_get_clause_and_num_literals` +- `test_nae_serialization_round_trip` + +Use the exact issue example with 5 variables and 5 clauses. The solver-count test should assert that `BruteForce::find_all_satisfying()` returns `10` satisfying assignments and contains both the issue assignment and its complement. + +**Step 2: Run the targeted test file and confirm it fails** + +Run: +```bash +cargo test nae_satisfiability --lib +``` + +Expected: compile failure because the model module does not exist yet. + +### Task 2: Implement the new model + +**Files:** +- Create: `src/models/formula/nae_satisfiability.rs` +- Modify: `src/models/formula/mod.rs` +- Modify: `src/models/mod.rs` +- Modify: `src/lib.rs` + +**Step 1: Implement the model file** + +Mirror the structure of `sat.rs`: +- `inventory::submit!` with `ProblemSchemaEntry` +- `#[derive(Debug, Clone, Serialize, Deserialize)]` +- fields `num_vars`, `clauses` +- getters `num_vars()`, `num_clauses()`, `num_literals()`, `clauses()`, `get_clause()` +- `Problem` impl with `Metric = bool`, `dims()`, `evaluate()`, `variant()` +- `impl SatisfactionProblem` +- `declare_variants!` entry for the default variant +- `#[cfg(feature = "example-db")]` canonical example spec +- `#[cfg(test)]` path link to the new test file + +Add model-local helpers: +- `config_to_assignment(config: &[usize]) -> Vec` +- `literal_value(lit: i32, assignment: &[bool]) -> bool` +- `clause_is_nae_satisfied(clause: &CNFClause, assignment: &[bool]) -> bool` +- `is_nae_satisfying(&self, assignment: &[bool]) -> bool` +- `count_nae_satisfied(&self, assignment: &[bool]) -> usize` + +`clause_is_nae_satisfied` should evaluate every literal occurrence, then return `true` iff at least one evaluated literal is `true` and at least one is `false`. + +**Step 2: Register the model** + +Update module exports: +- `src/models/formula/mod.rs`: add module declaration, public re-export, and include its example specs in the formula example chain +- `src/models/mod.rs`: add `NAESatisfiability` to the formula re-export block +- `src/lib.rs`: add `NAESatisfiability` to the public formula exports + +**Step 3: Run the new targeted tests** + +Run: +```bash +cargo test nae_satisfiability --lib +``` + +Expected: the new test file passes or exposes only the remaining registration/example-db gaps. + +### Task 3: Wire CLI creation and example-db + +**Files:** +- Modify: `problemreductions-cli/src/commands/create.rs` +- Modify: `src/models/formula/mod.rs` + +**Step 1: Add CLI create support** + +In `problemreductions-cli/src/commands/create.rs`: +- add an `example_for("NAESatisfiability")` usage string beside the SAT entries +- add a `create()` match arm for `"NAESatisfiability"` reusing the existing clause parser and `--num-vars` +- import the new model if the file needs it + +Do not add new flags unless the existing parser proves insufficient. + +**Step 2: Confirm example-db discovery** + +Ensure the new model file exposes `canonical_model_example_specs()` and that `src/models/formula/mod.rs` includes it in the aggregated example spec list. `src/example_db/model_builders.rs` should then pick it up automatically through the existing formula chain, so no direct edit is expected there. + +**Step 3: Run CLI/example-focused tests** + +Run: +```bash +cargo test nae_satisfiability --lib +cargo test create --package problemreductions-cli +``` + +Expected: the new model can be constructed by the CLI path and the model tests still pass. + +### Task 4: Full Rust verification for Batch 1 + +**Files:** +- No new files; verification only + +**Step 1: Run focused formatting/build checks** + +Run: +```bash +cargo fmt --all +cargo test nae_satisfiability --lib +cargo test --package problemreductions-cli create +``` + +**Step 2: Commit Batch 1** + +Run: +```bash +git add src/models/formula/nae_satisfiability.rs src/models/formula/mod.rs src/models/mod.rs src/lib.rs src/unit_tests/models/formula/nae_satisfiability.rs problemreductions-cli/src/commands/create.rs +git commit -m "Add NAESatisfiability model" +``` + +## Batch 2 + +### Task 5: Add the paper entry and align the worked example + +**Files:** +- Modify: `docs/paper/reductions.typ` + +**Step 1: Add display name** + +Insert a display-name entry for `NAESatisfiability` near the other formula problems. + +**Step 2: Add `problem-def("NAESatisfiability")`** + +Use the SAT and K-SAT entries as the reference pattern. The body should include: +- a short explanation of NAE-SAT and complement symmetry +- the brute-force complexity statement with citation already present in `references.bib` +- the exact 5-variable issue example +- a sentence showing why `[0,0,0,1,1]` satisfies every clause +- a note that `[1,1,1,0,0]` is also satisfying by complement symmetry + +Prefer to load the canonical example from example-db rather than duplicating raw data. + +### Task 6: Add/finish the paper-example test and run paper verification + +**Files:** +- Modify: `src/unit_tests/models/formula/nae_satisfiability.rs` +- Modify: `docs/paper/reductions.typ` + +**Step 1: Ensure there is a dedicated paper-example test** + +Add `test_nae_satisfiability_paper_example` that: +- constructs the exact issue/paper instance +- asserts the issue solution evaluates to `true` +- asserts the complement evaluates to `true` +- asserts the satisfying-solution count is `10` + +**Step 2: Build the paper** + +Run: +```bash +make paper +``` + +Expected: Typst compiles without errors and the new problem definition is included. + +### Task 7: Final verification + +**Files:** +- No new files; verification only + +**Step 1: Run project verification** + +Run: +```bash +make test +make clippy +``` + +If either command surfaces unrelated pre-existing failures, capture them explicitly before proceeding. + +**Step 2: Commit Batch 2** + +Run: +```bash +git add docs/paper/reductions.typ src/unit_tests/models/formula/nae_satisfiability.rs +git commit -m "Document NAESatisfiability" +``` + +## Handoff Notes for Execution + +- Keep the implementation close to `Satisfiability`; avoid premature abstractions shared between SAT and NAE-SAT in this PR. +- Treat the issue’s 5-variable example as the source of truth for the canonical example, test data, and paper write-up. +- Before final push, verify the plan file itself is deleted from the branch as required by `issue-to-pr`. From 75ad4964b26ad8c944bb9f911ff144990a991005 Mon Sep 17 00:00:00 2001 From: Jinguo Liu Date: Sat, 21 Mar 2026 03:43:39 +0800 Subject: [PATCH 2/3] Implement #143: [Model] NAESatisfiability --- docs/paper/reductions.typ | 24 ++ problemreductions-cli/src/cli.rs | 3 +- problemreductions-cli/src/commands/create.rs | 14 ++ src/lib.rs | 3 +- src/models/formula/mod.rs | 4 + src/models/formula/nae_satisfiability.rs | 208 ++++++++++++++++++ src/models/mod.rs | 3 +- .../models/formula/nae_satisfiability.rs | 143 ++++++++++++ 8 files changed, 399 insertions(+), 3 deletions(-) create mode 100644 src/models/formula/nae_satisfiability.rs create mode 100644 src/unit_tests/models/formula/nae_satisfiability.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index a412a3a29..a425fc168 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -91,6 +91,7 @@ "Knapsack": [Knapsack], "PartiallyOrderedKnapsack": [Partially Ordered Knapsack], "Satisfiability": [SAT], + "NAESatisfiability": [NAE-SAT], "KSatisfiability": [$k$-SAT], "CircuitSAT": [CircuitSAT], "ConjunctiveQueryFoldability": [Conjunctive Query Foldability], @@ -2339,6 +2340,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 diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs index 5c3bae2d1..a220af595 100644 --- a/problemreductions-cli/src/cli.rs +++ b/problemreductions-cli/src/cli.rs @@ -218,7 +218,8 @@ Flags by problem type: MIS, MVC, MaxClique, MinDomSet --graph, --weights MaxCut, MaxMatching, TSP --graph, --edge-weights 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 diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index 85fb53849..e88ea305e 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/problemreductions-cli/src/commands/create.rs @@ -396,6 +396,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\"" } @@ -1305,6 +1306,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!( diff --git a/src/lib.rs b/src/lib.rs index 34ca7f66a..179f50300 100644 --- a/src/lib.rs +++ b/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, diff --git a/src/models/formula/mod.rs b/src/models/formula/mod.rs index 568dc0760..5f9417872 100644 --- a/src/models/formula/mod.rs +++ b/src/models/formula/mod.rs @@ -2,17 +2,20 @@ //! //! 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}; @@ -20,6 +23,7 @@ pub use sat::{CNFClause, Satisfiability}; pub(crate) fn canonical_model_example_specs() -> Vec { 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()); diff --git a/src/models/formula/nae_satisfiability.rs b/src/models/formula/nae_satisfiability.rs new file mode 100644 index 000000000..54e896a4a --- /dev/null +++ b/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", 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, +} + +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) -> 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) -> Result { + 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 { + 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 { + 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, +} + +impl TryFrom for NAESatisfiability { + type Error = String; + + fn try_from(value: NAESatisfiabilityDef) -> Result { + 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 { + 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; diff --git a/src/models/mod.rs b/src/models/mod.rs index a3eb9ef14..3c3f59eb8 100644 --- a/src/models/mod.rs +++ b/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, diff --git a/src/unit_tests/models/formula/nae_satisfiability.rs b/src/unit_tests/models/formula/nae_satisfiability.rs new file mode 100644 index 000000000..9b38f88f5 --- /dev/null +++ b/src/unit_tests/models/formula/nae_satisfiability.rs @@ -0,0 +1,143 @@ +use super::*; +use crate::solvers::{BruteForce, Solver}; +use crate::traits::Problem; +use std::collections::HashSet; + +fn issue_problem() -> NAESatisfiability { + 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]), + ], + ) +} + +#[test] +fn test_nae_satisfiability_creation() { + let problem = issue_problem(); + + assert_eq!(problem.num_vars(), 5); + assert_eq!(problem.num_clauses(), 5); + assert_eq!(problem.num_literals(), 15); + assert_eq!(problem.num_variables(), 5); +} + +#[test] +fn test_nae_clause_requires_true_and_false_literals() { + let problem = NAESatisfiability::new(3, vec![CNFClause::new(vec![1, 2, -3])]); + + assert!(problem.evaluate(&[0, 0, 0])); + assert!(!problem.evaluate(&[1, 1, 0])); + assert!(!problem.evaluate(&[0, 0, 1])); +} + +#[test] +fn test_nae_clause_with_literal_and_negation_is_always_satisfied() { + let problem = NAESatisfiability::new(1, vec![CNFClause::new(vec![1, -1])]); + + assert!(problem.evaluate(&[0])); + assert!(problem.evaluate(&[1])); +} + +#[test] +fn test_nae_satisfying_example_from_issue() { + let problem = issue_problem(); + + assert!(problem.evaluate(&[0, 0, 0, 1, 1])); + assert!(problem.is_valid_solution(&[0, 0, 0, 1, 1])); +} + +#[test] +fn test_nae_complement_symmetry_for_issue_example() { + let problem = issue_problem(); + + assert!(problem.evaluate(&[0, 0, 0, 1, 1])); + assert!(problem.evaluate(&[1, 1, 1, 0, 0])); +} + +#[test] +fn test_nae_solver_counts_ten_solutions_for_issue_example() { + let problem = issue_problem(); + let solver = BruteForce::new(); + + let solutions = solver.find_all_satisfying(&problem); + let set: HashSet> = solutions.into_iter().collect(); + + assert_eq!(set.len(), 10); + assert!(set.contains(&vec![0, 0, 0, 1, 1])); + assert!(set.contains(&vec![1, 1, 1, 0, 0])); +} + +#[test] +fn test_nae_empty_formula_is_trivially_satisfying() { + let problem = NAESatisfiability::new(0, vec![]); + let solver = BruteForce::new(); + + assert!(problem.evaluate(&[])); + assert_eq!(solver.find_satisfying(&problem), Some(vec![])); + assert_eq!( + solver.find_all_satisfying(&problem), + vec![Vec::::new()] + ); +} + +#[test] +fn test_nae_constructor_rejects_short_clauses() { + let result = + std::panic::catch_unwind(|| NAESatisfiability::new(1, vec![CNFClause::new(vec![1])])); + + assert!(result.is_err()); +} + +#[test] +fn test_nae_try_new_rejects_short_clauses() { + let result = NAESatisfiability::try_new(1, vec![CNFClause::new(vec![1])]); + + assert!(result.is_err()); +} + +#[test] +fn test_nae_get_clause_and_num_literals() { + let problem = issue_problem(); + + assert_eq!(problem.get_clause(0), Some(&CNFClause::new(vec![1, 2, -3]))); + assert_eq!(problem.get_clause(5), None); + assert_eq!( + problem.count_nae_satisfied(&[false, false, false, true, true]), + 5 + ); +} + +#[test] +fn test_nae_serialization_round_trip() { + let problem = issue_problem(); + let json = serde_json::to_string(&problem).unwrap(); + let round_trip: NAESatisfiability = serde_json::from_str(&json).unwrap(); + + assert_eq!(round_trip.num_vars(), problem.num_vars()); + assert_eq!(round_trip.num_clauses(), problem.num_clauses()); + assert_eq!(round_trip.num_literals(), problem.num_literals()); + assert!(round_trip.evaluate(&[0, 0, 0, 1, 1])); +} + +#[test] +fn test_nae_deserialization_rejects_short_clauses() { + let json = r#"{"num_vars":1,"clauses":[{"literals":[1]}]}"#; + let result: Result = serde_json::from_str(json); + + assert!(result.is_err()); +} + +#[test] +fn test_nae_satisfiability_paper_example() { + let problem = issue_problem(); + let solver = BruteForce::new(); + + assert!(problem.evaluate(&[0, 0, 0, 1, 1])); + assert!(problem.evaluate(&[1, 1, 1, 0, 0])); + assert_eq!(solver.find_all_satisfying(&problem).len(), 10); +} From 9824fca1b811e91baef570a5889ac8d192531928 Mon Sep 17 00:00:00 2001 From: Jinguo Liu Date: Sat, 21 Mar 2026 03:44:22 +0800 Subject: [PATCH 3/3] chore: remove plan file after implementation --- .../2026-03-21-nae-satisfiability-model.md | 253 ------------------ 1 file changed, 253 deletions(-) delete mode 100644 docs/plans/2026-03-21-nae-satisfiability-model.md diff --git a/docs/plans/2026-03-21-nae-satisfiability-model.md b/docs/plans/2026-03-21-nae-satisfiability-model.md deleted file mode 100644 index 9e32f2c25..000000000 --- a/docs/plans/2026-03-21-nae-satisfiability-model.md +++ /dev/null @@ -1,253 +0,0 @@ -# NAESatisfiability Implementation Plan - -> **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task. - -**Goal:** Add the `NAESatisfiability` formula model, wire it into the registry/CLI/example-db/paper flows, and cover the issue’s worked example and NAE-specific semantics with tests. - -**Architecture:** Implement `NAESatisfiability` as a sibling of `Satisfiability`, reusing `CNFClause` but giving the model its own clause-evaluation logic: every clause must contain at least one true literal and at least one false literal. Keep the registration path fully registry-backed so the CLI, exports, and paper all discover the new model through the normal model/example mechanisms. - -**Tech Stack:** Rust workspace, serde, inventory registry, `declare_variants!`, cargo tests, Typst paper, GitHub issue `#143`. - ---- - -**Issue:** `#143` `[Model] NAESatisfiability` -**Implementation skill:** repo-local `add-model` -**Execution mode:** batch the paper work separately after the Rust implementation and example-db wiring are stable. - -## Information Checklist - -| # | Item | Value | -|---|------|-------| -| 1 | Problem name | `NAESatisfiability` | -| 2 | Mathematical definition | Given a CNF formula, find an assignment such that every clause has at least one true literal and at least one false literal | -| 3 | Problem type | Satisfaction (`Metric = bool`) | -| 4 | Type parameters | None | -| 5 | Struct fields | `num_vars: usize`, `clauses: Vec` | -| 6 | Configuration space | `vec![2; num_vars]` | -| 7 | Feasibility check | Convert config to Boolean assignment; each clause must contain both truth values among its literal occurrences | -| 8 | Objective function | `bool` | -| 9 | Best known exact algorithm | brute-force, issue gives `2^num_vars`; for `declare_variants!` use the repo’s accepted getter name (`2^num_variables` if `num_vars` is rejected at compile time) | -| 10 | Solving strategy | existing `BruteForce` solver | -| 11 | Category | `src/models/formula/` | -| 12 | Expected outcome | issue example assignment `[0, 0, 0, 1, 1]` is satisfying; complement `[1, 1, 1, 0, 0]` is also satisfying; total satisfying assignments = `10` | - -## Associated Rule Check - -- Existing cross-reference: GitHub issue `#382` `[Rule] NOT-ALL-EQUAL 3SAT to SET SPLITTING` -- Planned follow-ons in the issue body: `Satisfiability -> NAESatisfiability`, `NAESatisfiability -> MaxCut` -- Result: safe to proceed; this model is not an orphan. - -## Design Notes - -- Reuse [`src/models/formula/sat.rs`](/Users/jinguomini/rcode/problem-reductions/.worktrees/issue-143/src/models/formula/sat.rs) for the struct/registry/test pattern, but do not reuse `CNFClause::is_satisfied()` for model semantics. -- Add model-local helpers such as `count_nae_satisfied`, `is_nae_satisfying`, and a literal-evaluation helper that works on literal occurrences, not deduplicated variables. -- Enforce the issue schema invariant that each clause has at least two literals in the constructor. Empty formulas remain valid; empty or unit clauses inside a formula should be rejected at construction time. -- No new CLI flags should be necessary: existing `--num-vars` and `--clauses` are enough. -- CLI alias resolution is registry-backed in the current codebase, so prefer defining aliases in `ProblemSchemaEntry` over adding manual alias tables unless implementation proves otherwise. - -## Batch Plan - -- **Batch 1:** model implementation, registration, CLI create support, example-db, and Rust tests -- **Batch 2:** paper entry, paper-example alignment, final verification - -## Batch 1 - -### Task 1: Add failing model tests first - -**Files:** -- Create: `src/unit_tests/models/formula/nae_satisfiability.rs` - -**Step 1: Write the failing tests** - -Add tests that lock down the issue semantics before implementation: -- `test_nae_satisfiability_creation` -- `test_nae_clause_requires_true_and_false_literals` -- `test_nae_satisfying_example_from_issue` -- `test_nae_complement_symmetry_for_issue_example` -- `test_nae_solver_counts_ten_solutions_for_issue_example` -- `test_nae_empty_formula_is_trivially_satisfying` -- `test_nae_constructor_rejects_short_clauses` -- `test_nae_get_clause_and_num_literals` -- `test_nae_serialization_round_trip` - -Use the exact issue example with 5 variables and 5 clauses. The solver-count test should assert that `BruteForce::find_all_satisfying()` returns `10` satisfying assignments and contains both the issue assignment and its complement. - -**Step 2: Run the targeted test file and confirm it fails** - -Run: -```bash -cargo test nae_satisfiability --lib -``` - -Expected: compile failure because the model module does not exist yet. - -### Task 2: Implement the new model - -**Files:** -- Create: `src/models/formula/nae_satisfiability.rs` -- Modify: `src/models/formula/mod.rs` -- Modify: `src/models/mod.rs` -- Modify: `src/lib.rs` - -**Step 1: Implement the model file** - -Mirror the structure of `sat.rs`: -- `inventory::submit!` with `ProblemSchemaEntry` -- `#[derive(Debug, Clone, Serialize, Deserialize)]` -- fields `num_vars`, `clauses` -- getters `num_vars()`, `num_clauses()`, `num_literals()`, `clauses()`, `get_clause()` -- `Problem` impl with `Metric = bool`, `dims()`, `evaluate()`, `variant()` -- `impl SatisfactionProblem` -- `declare_variants!` entry for the default variant -- `#[cfg(feature = "example-db")]` canonical example spec -- `#[cfg(test)]` path link to the new test file - -Add model-local helpers: -- `config_to_assignment(config: &[usize]) -> Vec` -- `literal_value(lit: i32, assignment: &[bool]) -> bool` -- `clause_is_nae_satisfied(clause: &CNFClause, assignment: &[bool]) -> bool` -- `is_nae_satisfying(&self, assignment: &[bool]) -> bool` -- `count_nae_satisfied(&self, assignment: &[bool]) -> usize` - -`clause_is_nae_satisfied` should evaluate every literal occurrence, then return `true` iff at least one evaluated literal is `true` and at least one is `false`. - -**Step 2: Register the model** - -Update module exports: -- `src/models/formula/mod.rs`: add module declaration, public re-export, and include its example specs in the formula example chain -- `src/models/mod.rs`: add `NAESatisfiability` to the formula re-export block -- `src/lib.rs`: add `NAESatisfiability` to the public formula exports - -**Step 3: Run the new targeted tests** - -Run: -```bash -cargo test nae_satisfiability --lib -``` - -Expected: the new test file passes or exposes only the remaining registration/example-db gaps. - -### Task 3: Wire CLI creation and example-db - -**Files:** -- Modify: `problemreductions-cli/src/commands/create.rs` -- Modify: `src/models/formula/mod.rs` - -**Step 1: Add CLI create support** - -In `problemreductions-cli/src/commands/create.rs`: -- add an `example_for("NAESatisfiability")` usage string beside the SAT entries -- add a `create()` match arm for `"NAESatisfiability"` reusing the existing clause parser and `--num-vars` -- import the new model if the file needs it - -Do not add new flags unless the existing parser proves insufficient. - -**Step 2: Confirm example-db discovery** - -Ensure the new model file exposes `canonical_model_example_specs()` and that `src/models/formula/mod.rs` includes it in the aggregated example spec list. `src/example_db/model_builders.rs` should then pick it up automatically through the existing formula chain, so no direct edit is expected there. - -**Step 3: Run CLI/example-focused tests** - -Run: -```bash -cargo test nae_satisfiability --lib -cargo test create --package problemreductions-cli -``` - -Expected: the new model can be constructed by the CLI path and the model tests still pass. - -### Task 4: Full Rust verification for Batch 1 - -**Files:** -- No new files; verification only - -**Step 1: Run focused formatting/build checks** - -Run: -```bash -cargo fmt --all -cargo test nae_satisfiability --lib -cargo test --package problemreductions-cli create -``` - -**Step 2: Commit Batch 1** - -Run: -```bash -git add src/models/formula/nae_satisfiability.rs src/models/formula/mod.rs src/models/mod.rs src/lib.rs src/unit_tests/models/formula/nae_satisfiability.rs problemreductions-cli/src/commands/create.rs -git commit -m "Add NAESatisfiability model" -``` - -## Batch 2 - -### Task 5: Add the paper entry and align the worked example - -**Files:** -- Modify: `docs/paper/reductions.typ` - -**Step 1: Add display name** - -Insert a display-name entry for `NAESatisfiability` near the other formula problems. - -**Step 2: Add `problem-def("NAESatisfiability")`** - -Use the SAT and K-SAT entries as the reference pattern. The body should include: -- a short explanation of NAE-SAT and complement symmetry -- the brute-force complexity statement with citation already present in `references.bib` -- the exact 5-variable issue example -- a sentence showing why `[0,0,0,1,1]` satisfies every clause -- a note that `[1,1,1,0,0]` is also satisfying by complement symmetry - -Prefer to load the canonical example from example-db rather than duplicating raw data. - -### Task 6: Add/finish the paper-example test and run paper verification - -**Files:** -- Modify: `src/unit_tests/models/formula/nae_satisfiability.rs` -- Modify: `docs/paper/reductions.typ` - -**Step 1: Ensure there is a dedicated paper-example test** - -Add `test_nae_satisfiability_paper_example` that: -- constructs the exact issue/paper instance -- asserts the issue solution evaluates to `true` -- asserts the complement evaluates to `true` -- asserts the satisfying-solution count is `10` - -**Step 2: Build the paper** - -Run: -```bash -make paper -``` - -Expected: Typst compiles without errors and the new problem definition is included. - -### Task 7: Final verification - -**Files:** -- No new files; verification only - -**Step 1: Run project verification** - -Run: -```bash -make test -make clippy -``` - -If either command surfaces unrelated pre-existing failures, capture them explicitly before proceeding. - -**Step 2: Commit Batch 2** - -Run: -```bash -git add docs/paper/reductions.typ src/unit_tests/models/formula/nae_satisfiability.rs -git commit -m "Document NAESatisfiability" -``` - -## Handoff Notes for Execution - -- Keep the implementation close to `Satisfiability`; avoid premature abstractions shared between SAT and NAE-SAT in this PR. -- Treat the issue’s 5-variable example as the source of truth for the canonical example, test data, and paper write-up. -- Before final push, verify the plan file itself is deleted from the branch as required by `issue-to-pr`.