From 0e9c68d0c148ccd0a7492626b5c15abf76478c26 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 13:54:24 +0800 Subject: [PATCH 1/3] Add plan for #1101: NAESatisfiability to Satisfiability --- ...-02-naesatisfiability-to-satisfiability.md | 60 +++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 docs/plans/2026-08-02-naesatisfiability-to-satisfiability.md diff --git a/docs/plans/2026-08-02-naesatisfiability-to-satisfiability.md b/docs/plans/2026-08-02-naesatisfiability-to-satisfiability.md new file mode 100644 index 000000000..e61f21692 --- /dev/null +++ b/docs/plans/2026-08-02-naesatisfiability-to-satisfiability.md @@ -0,0 +1,60 @@ +# NAESatisfiability to Satisfiability Reduction + +Implement issue #1101 as a witness-preserving reduction from arbitrary-width +`NAESatisfiability` to `Satisfiability`. The construction retains every source +variable and replaces each NAE clause `C` by the two SAT clauses `C` and its +literalwise complement. Target witnesses therefore map back by identity. + +## Batch 1: Verify and implement the rule + +Follow `.agents/skills/add-rule/SKILL.md` Steps 0-5 and 7, including the default +`.agents/skills/verify-reduction/SKILL.md` procedure before writing Rust code. + +1. Confirm the `Or -> Or` type pairing in + `src/models/formula/nae_satisfiability.rs` and `src/models/formula/sat.rs`. +2. Verify the construction mathematically with ephemeral artifacts: + - Write a self-contained Typst proof covering arbitrary clause width, + repeated literals and variables, tautological clauses, and the empty + conjunction. + - Independently exercise the clause-doubling constructor, identity solution + extraction, exact overhead (`num_vars`, `2 * num_clauses`, + `2 * num_literals`), target validity, and both directions on at least 5,000 + checks, including exhaustive assignments through five variables. + - Use a three-variable feasible example and a three-variable infeasible + example, then cross-compare an independent adversary implementation. +3. Add `src/rules/naesatisfiability_satisfiability.rs` with one + `#[reduction]` registration, a direct target construction, and identity + extraction. Do not add adapters or alternate implementations. +4. Register the module in `src/rules/mod.rs`. +5. Add focused tests in + `src/unit_tests/rules/naesatisfiability_satisfiability.rs` for: + - the issue's three-clause closed-loop witness; + - an infeasible repeated-literal formula; + - exact doubled clauses and all three overhead metrics; + - empty conjunction, arbitrary width, repeated literals, tautological + clauses, and identity extraction; + - direct reduction-graph registration and canonical example integrity. +6. Add the issue's three-variable instance as the canonical example in the + rule's `canonical_rule_example_specs()` registration, following the current + module-local example-db pattern. +7. Run focused Rust tests and regenerate graph/schema exports and example + fixtures needed by the paper. Keep only tracked artifacts required by the + rule. + +## Batch 2: Document the verified rule + +With fresh context, follow `.agents/skills/add-rule/SKILL.md` Step 6. + +1. Add the Gurumukhani-Paturi-Saks-Talebanfard STACS 2025 reference to + `docs/paper/references.bib` if it is not already present; retain Schaefer's + classical citation where useful. +2. Add the `NAESatisfiability -> Satisfiability` theorem, proof, extraction, + and tutorial example to `docs/paper/reductions.typ`. Derive the command block + and concrete values from the canonical example fixture. +3. State the two-clause construction and prove both directions independently: + the original clause supplies a true literal, while its complement supplies + a false literal. +4. Run `make paper`, then run the full required `make test clippy` verification. + Confirm formatting, a clean tracked worktree, and that the temporary plan is + removed before the final push. + From 453d7d04203f104bd1478834826c888ecd4c490b Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:23:44 +0800 Subject: [PATCH 2/3] Implement #1101: NAESatisfiability to Satisfiability --- docs/paper/reductions.typ | 53 +++++++ docs/paper/references.bib | 12 +- src/rules/mod.rs | 2 + src/rules/naesatisfiability_satisfiability.rs | 84 +++++++++++ .../rules/naesatisfiability_satisfiability.rs | 133 ++++++++++++++++++ 5 files changed, 283 insertions(+), 1 deletion(-) create mode 100644 src/rules/naesatisfiability_satisfiability.rs create mode 100644 src/unit_tests/rules/naesatisfiability_satisfiability.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 88cd07556..f0f15f00b 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -13066,6 +13066,59 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ If the sentinel $s = 0$, return the first $n$ variables. If $s = 1$, return the complement of the first $n$ variables. ] +#let nae_sat = load-example("NAESatisfiability", "Satisfiability") +#let nae_sat_sol = nae_sat.solutions.at(0) +#reduction-rule("NAESatisfiability", "Satisfiability", + example: true, + example-caption: [$n = #nae_sat.source.instance.num_vars$ variables, $m = #sat-num-clauses(nae_sat.source.instance)$ NAE clauses, and $#sat-num-clauses(nae_sat.target.instance)$ SAT clauses], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(nae_sat.source) + " -o naesat.json", + "pred reduce naesat.json --to " + target-spec(nae_sat) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate naesat.json --config " + nae_sat_sol.source_config.map(str).join(","), + ) + + #{ + let fmt-lit(l) = if l > 0 { $x_#l$ } else { $overline(x)_#calc.abs(l)$ } + let fmt-clause(c) = $paren.l #c.literals.map(fmt-lit).join($or$) paren.r$ + let lit-value(l, config) = if l > 0 { config.at(l - 1) } else { 1 - config.at(-l - 1) } + let truth-pattern(c, config) = c.literals.map(l => lit-value(l, config)) + let clause-value(c, config) = if truth-pattern(c, config).any(v => v == 1) { 1 } else { 0 } + [ + *Step 1 -- Read the NAE instance.* The fixture has $#nae_sat.source.instance.num_vars$ variables and $#sat-num-clauses(nae_sat.source.instance)$ clauses: + $#nae_sat.source.instance.clauses.enumerate().map(((j, c)) => $C_#(j + 1) = #fmt-clause(c)$).join($comma quad$)$. + + *Step 2 -- Double the clauses.* For each $C_j$, emit $C_j$ followed by its literalwise complement $overline(C_j)$. The target therefore retains $#nae_sat.target.instance.num_vars$ variables and contains $#sat-num-clauses(nae_sat.target.instance)$ clauses: + $#nae_sat.target.instance.clauses.enumerate().map(((j, c)) => $D_#(j + 1) = #fmt-clause(c)$).join($comma quad$)$. + The source has $#nae_sat.source.instance.clauses.map(c => c.literals.len()).sum()$ literal occurrences, while the target has $#nae_sat.target.instance.clauses.map(c => c.literals.len()).sum()$. + + *Step 3 -- Verify the canonical witness.* For $(#range(nae_sat.source.instance.num_vars).map(i => $x_#(i + 1)$).join(", ")) = (#nae_sat_sol.source_config.map(str).join(", "))$, the source clauses have literal-value patterns + $#nae_sat.source.instance.clauses.enumerate().map(((j, c)) => $C_#(j + 1): #truth-pattern(c, nae_sat_sol.source_config).map(str).join(",")$).join([; ])$. + Every pattern contains both $0$ and $1$, so every NAE clause is satisfied. Under the identical target configuration $(#nae_sat_sol.target_config.map(str).join(", "))$, the target clauses evaluate to $(#nae_sat.target.instance.clauses.map(c => str(clause-value(c, nae_sat_sol.target_config))).join(", "))$ #sym.checkmark. + + *Step 4 -- Extract the source witness.* Identity extraction returns $(#nae_sat_sol.target_config.map(str).join(", "))$, exactly the stored source configuration $(#nae_sat_sol.source_config.map(str).join(", "))$. + + *Multiplicity:* The fixture stores one canonical witness. Since the reduction introduces no variables and preserves every assignment pointwise, each NAE witness corresponds to exactly one SAT witness and conversely; this conclusion follows from the construction, not from the number of stored fixture solutions. + ] + } + ], +)[ + Let $L = sum_(j=1)^m |C_j|$ be the number of literal occurrences. This $O(L)$ negation-closure construction @Gurumukhani2025, also implicit in the classical ternary NAE relation @schaefer1978, keeps all $n$ variables and replaces every NAE clause $C_j$ by two SAT clauses, $C_j$ and its literalwise complement $overline(C_j)$. The target has $n$ variables, $2m$ clauses, and $2L$ literal occurrences. +][ + _Construction._ Let $Phi = and.big_(j=1)^m "NAE"(C_j)$ be an NAE-CNF formula on variables $x_1, dots, x_n$, where $C_j = (ell_(j,1), dots, ell_(j,r_j))$ and each $ell_(j,k)$ is a literal. For a literal $ell$, let $overline(ell)$ denote its Boolean complement, and define $overline(C_j) = (overline(ell_(j,1)) or dots or overline(ell_(j,r_j)))$. Construct the ordinary CNF formula + $ + Psi = and.big_(j=1)^m (C_j and overline(C_j)), + $ + interpreting $C_j$ itself as the disjunction $(ell_(j,1) or dots or ell_(j,r_j))$. No variables are added or reordered. The construction copies and complements each literal once, so it takes $O(L)$ time. When $m = 0$, both source and target are the empty conjunction. + + _Correctness._ ($arrow.r.double$) Suppose an assignment satisfies $Phi$. In each $C_j$, the NAE condition supplies a true literal $ell_(j,p)$ and a false literal $ell_(j,q)$. The true literal satisfies the target clause $C_j$, while $overline(ell_(j,q))$ is true and satisfies $overline(C_j)$. Hence every pair $C_j and overline(C_j)$ is satisfied, so the assignment satisfies $Psi$. + + ($arrow.l.double$) Conversely, suppose an assignment satisfies $Psi$. For every $j$, satisfaction of $C_j$ supplies at least one true source literal. Satisfaction of $overline(C_j)$ supplies a true complemented literal $overline(ell_(j,q))$, so the corresponding source literal $ell_(j,q)$ is false. Thus $C_j$ contains both truth values and satisfies NAE. Therefore the same assignment satisfies $Phi$. + + _Solution extraction._ Return the target Boolean configuration unchanged. Because the target uses exactly the source variables in the same order, this identity map is valid for every satisfying assignment, including the unique empty configuration when $n = 0$. +] + #let cs_sat = load-example("CircuitSAT", "Satisfiability") #let cs_sat_sol = cs_sat.solutions.at(0) #reduction-rule("CircuitSAT", "Satisfiability", diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 186f70de2..7740fb8cb 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -1580,6 +1580,17 @@ @book{papadimitriou-steiglitz1982 year = {1982} } +@inproceedings{Gurumukhani2025, + author = {Mohit Gurumukhani and Ramamohan Paturi and Michael Saks and Navid Talebanfard}, + title = {Local Enumeration: The Not-All-Equal Case}, + booktitle = {42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + volume = {327}, + pages = {42:1--42:19}, + year = {2025}, + doi = {10.4230/LIPIcs.STACS.2025.42} +} + @article{schaefer1978, author = {Thomas J. Schaefer}, title = {The Complexity of Satisfiability Problems}, @@ -2142,4 +2153,3 @@ @article{berlekampMcElieceTilborg1978 year = {1978}, doi = {10.1109/TIT.1978.1055873} } - diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 95eb5f477..497abe110 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -109,6 +109,7 @@ pub(crate) mod minimumvertexcover_minimumsetcovering; pub(crate) mod minimumvertexcover_minimumweightandorgraph; pub(crate) mod naesatisfiability_maxcut; pub(crate) mod naesatisfiability_partitionintoperfectmatchings; +pub(crate) mod naesatisfiability_satisfiability; pub(crate) mod naesatisfiability_setsplitting; pub(crate) mod numerical3dimensionalmatching_numericalmatchingwithtargetsums; pub(crate) mod optimallineararrangement_consecutiveonesmatrixaugmentation; @@ -517,6 +518,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[reduction(overhead = { + num_vars = "num_vars", + num_clauses = "2 * num_clauses", + num_literals = "2 * num_literals", +})] +impl ReduceTo for NAESatisfiability { + type Result = ReductionNAESATToSAT; + + fn reduce_to(&self) -> Self::Result { + let clauses = self + .clauses() + .iter() + .flat_map(|clause| { + [ + clause.clone(), + CNFClause::new(clause.literals.iter().map(|literal| -literal).collect()), + ] + }) + .collect(); + + ReductionNAESATToSAT { + target: Satisfiability::new(self.num_vars(), clauses), + } + } +} + +#[cfg(any(test, feature = "example-db"))] +fn canonical_source() -> NAESatisfiability { + NAESatisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, 2]), + CNFClause::new(vec![1, -2, -3]), + ], + ) +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "naesatisfiability_to_satisfiability", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>( + canonical_source(), + SolutionPair { + source_config: vec![0, 0, 1], + target_config: vec![0, 0, 1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/naesatisfiability_satisfiability.rs"] +mod tests; diff --git a/src/unit_tests/rules/naesatisfiability_satisfiability.rs b/src/unit_tests/rules/naesatisfiability_satisfiability.rs new file mode 100644 index 000000000..190b1cd30 --- /dev/null +++ b/src/unit_tests/rules/naesatisfiability_satisfiability.rs @@ -0,0 +1,133 @@ +#[cfg(feature = "example-db")] +use super::canonical_rule_example_specs; +use super::*; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::{ReduceTo, ReductionGraph, ReductionResult}; +use crate::solvers::BruteForce; +use crate::traits::Problem; + +#[test] +fn test_naesatisfiability_to_satisfiability_closed_loop() { + let source = canonical_source(); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "NAESatisfiability -> Satisfiability closed loop", + ); + assert_eq!(reduction.extract_solution(&[0, 0, 1]), vec![0, 0, 1]); + assert!(source.evaluate(&[0, 0, 1]).0); + assert!(reduction.target_problem().evaluate(&[0, 0, 1]).0); +} + +#[test] +fn test_naesatisfiability_to_satisfiability_repeated_literal_infeasible() { + let source = NAESatisfiability::new(1, vec![CNFClause::new(vec![1, 1])]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!(BruteForce::new().find_witness(&source), None); + assert_eq!( + BruteForce::new().find_witness(reduction.target_problem()), + None + ); +} + +#[test] +fn test_naesatisfiability_to_satisfiability_structure_and_overhead() { + let source = NAESatisfiability::new( + 4, + vec![ + CNFClause::new(vec![1, -2]), + CNFClause::new(vec![2, 3, -4, 1]), + CNFClause::new(vec![-1, -1, 4]), + ], + ); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), source.num_vars()); + assert_eq!(target.num_clauses(), 2 * source.num_clauses()); + assert_eq!(target.num_literals(), 2 * source.num_literals()); + assert_eq!( + target.clauses(), + &[ + CNFClause::new(vec![1, -2]), + CNFClause::new(vec![-1, 2]), + CNFClause::new(vec![2, 3, -4, 1]), + CNFClause::new(vec![-2, -3, 4, -1]), + CNFClause::new(vec![-1, -1, 4]), + CNFClause::new(vec![1, 1, -4]), + ] + ); + + let entry = inventory::iter::() + .find(|entry| { + entry.source_name == "NAESatisfiability" && entry.target_name == "Satisfiability" + }) + .expect("NAESatisfiability -> Satisfiability reduction should be registered"); + let overhead = (entry.overhead_eval_fn)(&source as &dyn std::any::Any); + assert_eq!(overhead.get("num_vars"), Some(target.num_vars())); + assert_eq!(overhead.get("num_clauses"), Some(target.num_clauses())); + assert_eq!(overhead.get("num_literals"), Some(target.num_literals())); +} + +#[test] +fn test_naesatisfiability_to_satisfiability_edge_case_semantics() { + let formulas = [ + NAESatisfiability::new(0, vec![]), + NAESatisfiability::new(5, vec![CNFClause::new(vec![1, 2, -3, 4, -5])]), + NAESatisfiability::new(2, vec![CNFClause::new(vec![1, 1, -2])]), + NAESatisfiability::new(2, vec![CNFClause::new(vec![1, -1, 2])]), + ]; + + for source in formulas { + let reduction = ReduceTo::::reduce_to(&source); + for mask in 0..(1usize << source.num_vars()) { + let config = (0..source.num_vars()) + .map(|bit| (mask >> bit) & 1) + .collect::>(); + assert_eq!( + source.evaluate(&config), + reduction.target_problem().evaluate(&config), + "evaluation differs for config {config:?}", + ); + assert_eq!(reduction.extract_solution(&config), config); + } + } +} + +#[test] +fn test_reduction_graph_registers_naesatisfiability_to_satisfiability() { + assert!( + ReductionGraph::new().has_direct_reduction_by_name("NAESatisfiability", "Satisfiability") + ); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_naesatisfiability_to_satisfiability_canonical_example_spec() { + let example = (canonical_rule_example_specs() + .into_iter() + .find(|spec| spec.id == "naesatisfiability_to_satisfiability") + .expect("missing canonical NAESatisfiability -> Satisfiability example spec") + .build)(); + + assert_eq!(example.source.problem, "NAESatisfiability"); + assert_eq!(example.target.problem, "Satisfiability"); + assert_eq!(example.source.instance["num_vars"], serde_json::json!(3)); + assert_eq!( + example.target.instance["clauses"].as_array().unwrap().len(), + 6 + ); + assert_eq!(example.solutions.len(), 1); + assert_eq!(example.solutions[0].source_config, vec![0, 0, 1]); + assert_eq!(example.solutions[0].target_config, vec![0, 0, 1]); + + let source: NAESatisfiability = serde_json::from_value(example.source.instance.clone()) + .expect("source example deserializes"); + let target: Satisfiability = serde_json::from_value(example.target.instance.clone()) + .expect("target example deserializes"); + assert!(source.evaluate(&example.solutions[0].source_config).0); + assert!(target.evaluate(&example.solutions[0].target_config).0); +} From 9612967e50299d288fdb4563312e2e542da9d06a Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:23:48 +0800 Subject: [PATCH 3/3] chore: remove plan file after implementation --- ...-02-naesatisfiability-to-satisfiability.md | 60 ------------------- 1 file changed, 60 deletions(-) delete mode 100644 docs/plans/2026-08-02-naesatisfiability-to-satisfiability.md diff --git a/docs/plans/2026-08-02-naesatisfiability-to-satisfiability.md b/docs/plans/2026-08-02-naesatisfiability-to-satisfiability.md deleted file mode 100644 index e61f21692..000000000 --- a/docs/plans/2026-08-02-naesatisfiability-to-satisfiability.md +++ /dev/null @@ -1,60 +0,0 @@ -# NAESatisfiability to Satisfiability Reduction - -Implement issue #1101 as a witness-preserving reduction from arbitrary-width -`NAESatisfiability` to `Satisfiability`. The construction retains every source -variable and replaces each NAE clause `C` by the two SAT clauses `C` and its -literalwise complement. Target witnesses therefore map back by identity. - -## Batch 1: Verify and implement the rule - -Follow `.agents/skills/add-rule/SKILL.md` Steps 0-5 and 7, including the default -`.agents/skills/verify-reduction/SKILL.md` procedure before writing Rust code. - -1. Confirm the `Or -> Or` type pairing in - `src/models/formula/nae_satisfiability.rs` and `src/models/formula/sat.rs`. -2. Verify the construction mathematically with ephemeral artifacts: - - Write a self-contained Typst proof covering arbitrary clause width, - repeated literals and variables, tautological clauses, and the empty - conjunction. - - Independently exercise the clause-doubling constructor, identity solution - extraction, exact overhead (`num_vars`, `2 * num_clauses`, - `2 * num_literals`), target validity, and both directions on at least 5,000 - checks, including exhaustive assignments through five variables. - - Use a three-variable feasible example and a three-variable infeasible - example, then cross-compare an independent adversary implementation. -3. Add `src/rules/naesatisfiability_satisfiability.rs` with one - `#[reduction]` registration, a direct target construction, and identity - extraction. Do not add adapters or alternate implementations. -4. Register the module in `src/rules/mod.rs`. -5. Add focused tests in - `src/unit_tests/rules/naesatisfiability_satisfiability.rs` for: - - the issue's three-clause closed-loop witness; - - an infeasible repeated-literal formula; - - exact doubled clauses and all three overhead metrics; - - empty conjunction, arbitrary width, repeated literals, tautological - clauses, and identity extraction; - - direct reduction-graph registration and canonical example integrity. -6. Add the issue's three-variable instance as the canonical example in the - rule's `canonical_rule_example_specs()` registration, following the current - module-local example-db pattern. -7. Run focused Rust tests and regenerate graph/schema exports and example - fixtures needed by the paper. Keep only tracked artifacts required by the - rule. - -## Batch 2: Document the verified rule - -With fresh context, follow `.agents/skills/add-rule/SKILL.md` Step 6. - -1. Add the Gurumukhani-Paturi-Saks-Talebanfard STACS 2025 reference to - `docs/paper/references.bib` if it is not already present; retain Schaefer's - classical citation where useful. -2. Add the `NAESatisfiability -> Satisfiability` theorem, proof, extraction, - and tutorial example to `docs/paper/reductions.typ`. Derive the command block - and concrete values from the canonical example fixture. -3. State the two-clause construction and prove both directions independently: - the original clause supplies a true literal, while its complement supplies - a false literal. -4. Run `make paper`, then run the full required `make test clippy` verification. - Confirm formatting, a clean tracked worktree, and that the temporary plan is - removed before the final push. -