From fcff546cc30f3752f4aad8a21b1f688cba301a25 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 13:46:11 +0800 Subject: [PATCH 1/6] Add plan for #1100: SetSplitting to NAESatisfiability --- ...08-02-setsplitting-to-naesatisfiability.md | 57 +++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100644 docs/plans/2026-08-02-setsplitting-to-naesatisfiability.md diff --git a/docs/plans/2026-08-02-setsplitting-to-naesatisfiability.md b/docs/plans/2026-08-02-setsplitting-to-naesatisfiability.md new file mode 100644 index 000000000..697eaa5ce --- /dev/null +++ b/docs/plans/2026-08-02-setsplitting-to-naesatisfiability.md @@ -0,0 +1,57 @@ +# SetSplitting to NAESatisfiability implementation plan + +Issue: #1100 `[Rule] SetSplitting to NAESatisfiability` + +The implementation follows the repository `add-rule` workflow. Both models use +`Or`, so the reduction is witness-capable through `ReduceTo`. +The construction encodes element `u` as positive, one-indexed literal `u + 1`, +deduplicates each source subset while preserving first-occurrence order, and +emits `(x_u, x_u)` when a subset contains only repetitions of one element. + +## Batch 1: verify and implement the rule + +1. Run the `verify-reduction` workflow before writing Rust: + - prove that a source subset is split exactly when its positive-literal NAE + clause contains both truth values; + - cover the all-repeated subset with the unsatisfiable repeated-literal + clause; + - verify direct witness extraction and the overhead bounds + `num_vars = universe_size`, `num_clauses = num_subsets`, and + `num_literals <= (universe_size + 1) * num_subsets`; + - run independent constructor and adversary checks with at least 5,000 + checks each and cross-compare their target construction. +2. Add `src/rules/setsplitting_naesatisfiability.rs` with a direct + `ReductionResult`, identity witness extraction, deterministic first-seen + deduplication, `CNFClause` construction, and the required overhead metadata. +3. Register the module in `src/rules/mod.rs` without introducing any dispatch + layer or compatibility path. +4. Add focused tests in + `src/unit_tests/rules/setsplitting_naesatisfiability.rs`: + - closed-loop feasibility and witness extraction for the issue example; + - exact target structure and overhead bounds; + - repeated members and the all-repeated infeasible case; + - empty family, unused universe elements, and clauses of arity two through + greater than three; + - canonical example-db output. +5. Add the issue's four-element example to the rule's + `canonical_rule_example_specs()` implementation and ensure the existing + example-db collector discovers it. + +## Batch 2: paper documentation and generated fixtures + +1. With fresh context after Batch 1, add a self-contained + `reduction-rule("SetSplitting", "NAESatisfiability", ...)` entry to + `docs/paper/reductions.typ`, following the existing reverse rule and the + KColoring-to-QUBO tutorial structure. +2. Describe the construction, both correctness directions, identity solution + extraction, duplicate canonicalization, and the all-repeated NO case. +3. Build the worked example from the canonical example-db fixture and begin its + `extra:` block with the `pred-commands()` create/reduce/solve/evaluate flow. +4. Regenerate the reduction graph, schemas, and example-db fixtures, then run + `make paper`. + +## Final verification + +Run formatting, tests, and clippy (`make fmt-check`, `make test`, and +`make clippy`). Confirm that tracked changes are limited to the rule, +registration, tests, canonical fixture/export updates, and paper entry. From 80bb46ca6eed4f6ce75f3ea3ce8b606c87bbefb0 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 13:57:33 +0800 Subject: [PATCH 2/6] Implement SetSplitting to NAESatisfiability reduction --- src/rules/mod.rs | 2 + src/rules/setsplitting_naesatisfiability.rs | 89 +++++++++++++ .../rules/setsplitting_naesatisfiability.rs | 121 ++++++++++++++++++ 3 files changed, 212 insertions(+) create mode 100644 src/rules/setsplitting_naesatisfiability.rs create mode 100644 src/unit_tests/rules/setsplitting_naesatisfiability.rs diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 95eb5f477..aedda4356 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -138,6 +138,7 @@ pub(crate) mod satisfiability_maximum2satisfiability; pub(crate) mod satisfiability_naesatisfiability; pub(crate) mod satisfiability_nontautology; pub(crate) mod setsplitting_betweenness; +pub(crate) mod setsplitting_naesatisfiability; mod spinglass_casts; pub(crate) mod spinglass_maxcut; pub(crate) mod spinglass_qubo; @@ -557,6 +558,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 = "universe_size", + num_clauses = "num_subsets", + num_literals = "(universe_size + 1) * num_subsets", + } +)] +impl ReduceTo for SetSplitting { + type Result = ReductionSetSplittingToNAESatisfiability; + + fn reduce_to(&self) -> Self::Result { + let clauses = self + .subsets() + .iter() + .map(|subset| { + let mut seen = HashSet::new(); + let mut literals: Vec<_> = subset + .iter() + .copied() + .filter(|element| seen.insert(*element)) + .map(|element| (element + 1) as i32) + .collect(); + + if literals.len() == 1 { + literals.push(literals[0]); + } + + CNFClause::new(literals) + }) + .collect(); + + ReductionSetSplittingToNAESatisfiability { + target: NAESatisfiability::new(self.universe_size(), clauses), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "setsplitting_to_naesatisfiability", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, NAESatisfiability>( + SetSplitting::new(4, vec![vec![0, 1], vec![1, 2, 3], vec![0, 2, 3]]), + SolutionPair { + source_config: vec![0, 1, 0, 1], + target_config: vec![0, 1, 0, 1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/setsplitting_naesatisfiability.rs"] +mod tests; diff --git a/src/unit_tests/rules/setsplitting_naesatisfiability.rs b/src/unit_tests/rules/setsplitting_naesatisfiability.rs new file mode 100644 index 000000000..436325a6c --- /dev/null +++ b/src/unit_tests/rules/setsplitting_naesatisfiability.rs @@ -0,0 +1,121 @@ +use crate::models::formula::NAESatisfiability; +use crate::models::set::SetSplitting; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::rules::{ReduceTo, ReductionResult}; +use crate::solvers::BruteForce; + +fn issue_example() -> SetSplitting { + SetSplitting::new(4, vec![vec![0, 1], vec![1, 2, 3], vec![0, 2, 3]]) +} + +#[test] +fn test_setsplitting_to_naesatisfiability_closed_loop() { + let source = issue_example(); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "SetSplitting -> NAE-SAT", + ); + assert_eq!(reduction.extract_solution(&[0, 1, 0, 1]), vec![0, 1, 0, 1]); +} + +#[test] +fn test_setsplitting_to_naesatisfiability_structure_and_overhead() { + let source = issue_example(); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 4); + assert_eq!(target.num_clauses(), 3); + assert_eq!(target.num_literals(), 8); + assert_eq!( + target + .clauses() + .iter() + .map(|clause| clause.literals.clone()) + .collect::>(), + vec![vec![1, 2], vec![2, 3, 4], vec![1, 3, 4]], + ); + + let entry = inventory::iter::() + .find(|entry| { + entry.source_name == "SetSplitting" && entry.target_name == "NAESatisfiability" + }) + .expect("SetSplitting -> NAESatisfiability 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(15)); + assert!(target.num_literals() <= overhead.get("num_literals").unwrap()); +} + +#[test] +fn test_setsplitting_to_naesatisfiability_deduplicates_in_first_occurrence_order() { + let source = SetSplitting::new(4, vec![vec![2, 0, 2, 1, 0]]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!( + reduction.target_problem().clauses()[0].literals, + vec![3, 1, 2] + ); +} + +#[test] +fn test_setsplitting_to_naesatisfiability_all_repeated_subset_is_infeasible() { + let source = SetSplitting::new(1, vec![vec![0, 0]]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_eq!(reduction.target_problem().clauses()[0].literals, vec![1, 1]); + assert!(BruteForce::new().find_witness(&source).is_none()); + assert!(BruteForce::new() + .find_witness(reduction.target_problem()) + .is_none()); +} + +#[test] +fn test_setsplitting_to_naesatisfiability_empty_family_and_unused_element() { + let empty_source = SetSplitting::new(3, vec![]); + let empty_reduction = ReduceTo::::reduce_to(&empty_source); + assert_eq!(empty_reduction.target_problem().num_vars(), 3); + assert!(empty_reduction.target_problem().clauses().is_empty()); + + let source = SetSplitting::new(5, vec![vec![0, 1], vec![0, 1, 2], vec![0, 1, 2, 3, 1]]); + let reduction = ReduceTo::::reduce_to(&source); + assert_eq!(reduction.target_problem().num_vars(), 5); + assert_eq!( + reduction + .target_problem() + .clauses() + .iter() + .map(|clause| clause.literals.clone()) + .collect::>(), + vec![vec![1, 2], vec![1, 2, 3], vec![1, 2, 3, 4]], + ); +} + +#[cfg(feature = "example-db")] +#[test] +fn test_setsplitting_to_naesatisfiability_canonical_example_spec() { + let specs = crate::rules::setsplitting_naesatisfiability::canonical_rule_example_specs(); + assert_eq!(specs.len(), 1); + + let example = (specs[0].build)(); + assert_eq!(example.source.problem, "SetSplitting"); + assert_eq!(example.target.problem, "NAESatisfiability"); + assert_eq!(example.source.instance["universe_size"], 4); + assert_eq!( + example.target.instance["clauses"], + serde_json::json!([ + { "literals": [1, 2] }, + { "literals": [2, 3, 4] }, + { "literals": [1, 3, 4] }, + ]), + ); + + let pair = &example.solutions[0]; + assert_eq!(pair.source_config, vec![0, 1, 0, 1]); + assert_eq!(pair.target_config, vec![0, 1, 0, 1]); +} From 98414dfa7d34bae7ee10230987363301c69f2de1 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:01:22 +0800 Subject: [PATCH 3/6] Document SetSplitting to NAESatisfiability reduction --- docs/paper/reductions.typ | 43 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 88cd07556..360f136f7 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -18775,6 +18775,49 @@ The following table shows concrete variable overhead for example instances, take _Solution extraction._ Set $alpha(x_(i+1)) = chi(2i)$ for $i = 0, dots, n-1$. ] +// 8a. SetSplitting → NAESatisfiability +#let ss_nae = load-example("SetSplitting", "NAESatisfiability") +#let ss_nae_sol = ss_nae.solutions.at(0) +#reduction-rule("SetSplitting", "NAESatisfiability", + example: true, + example-caption: [$|U| = #ss_nae.source.instance.universe_size$, $#ss_nae.source.instance.subsets.len()$ subsets, and $#ss_nae.target.instance.clauses.len()$ NAE clauses], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(ss_nae.source) + " -o set-splitting.json", + "pred reduce set-splitting.json --to " + target-spec(ss_nae) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate set-splitting.json --config " + ss_nae_sol.source_config.map(str).join(","), + ) + + #{ + let source = ss_nae.source.instance + let target = ss_nae.target.instance + let colors = ss_nae_sol.source_config + [ + *Step 1 -- Start from the set family.* The universe is $U = {0, dots, #(source.universe_size - 1)}$, with subsets $S_1 = {#source.subsets.at(0).map(str).join(", ")}$, $S_2 = {#source.subsets.at(1).map(str).join(", ")}$, and $S_3 = {#source.subsets.at(2).map(str).join(", ")}$. The fixture's splitting is $(#colors.map(str).join(", "))$. + + *Step 2 -- Turn elements into variables and subsets into clauses.* The target has $#target.num_vars$ variables, one for each universe element. In signed one-indexed storage, the three canonicalized subsets become the positive-literal clauses $(#target.clauses.at(0).literals.map(str).join(", "))$, $(#target.clauses.at(1).literals.map(str).join(", "))$, and $(#target.clauses.at(2).literals.map(str).join(", "))$. Thus this fixture has $#target.clauses.len()$ clauses and $#target.clauses.map(c => c.literals.len()).sum()$ literal occurrences. + + *Step 3 -- Verify the NAE assignment.* Under the source colors, the three subsets have truth patterns $(#source.subsets.at(0).map(u => colors.at(u)).map(str).join(", "))$, $(#source.subsets.at(1).map(u => colors.at(u)).map(str).join(", "))$, and $(#source.subsets.at(2).map(u => colors.at(u)).map(str).join(", "))$. Every pattern contains both 0 and 1, so the identical target assignment $(#ss_nae_sol.target_config.map(str).join(", "))$ NAE-satisfies every clause. Extracting it unchanged recovers the source splitting $(#colors.map(str).join(", "))$ #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical witness. Because construction and extraction leave the configuration vector unchanged, every valid splitting corresponds to exactly one satisfying target assignment and conversely. + ] + } + ], +)[ + This $O(n + sum_(j=1)^m |S_j|)$ reduction @garey1979 @schaefer1978 identifies a two-way split with a Boolean assignment. It creates one variable for each of the $n$ universe elements and one positive-literal NAE clause for each of the $m$ source subset vectors. The target has exactly $n$ variables and $m$ clauses; its literal count is at most $(n + 1)m$. +][ + _Construction._ Let the Set Splitting instance have universe $U = {0, dots, n - 1}$ and subset vectors $S_1, dots, S_m$. Introduce a Boolean variable $x_u$ for each $u in U$, with its truth value denoting the side assigned to $u$. For each $S_j$, scan its entries from left to right and retain only the first occurrence of each distinct element, obtaining the canonical sequence $D_j$. If $|D_j| >= 2$, emit the NAE clause $C_j = (x_u : u in D_j)$, using only positive literals. If $D_j = (u)$, emit $C_j = (x_u, x_u)$. The implementation stores positive literal $x_u$ as the signed one-indexed integer $u + 1$. + + Duplicate removal preserves the first-seen order for deterministic output and does not affect which colors occur in a subset. The exact literal count is $sum_j max(2, |D_j|)$, bounded by $(n + 1)m$; the variable and clause counts are exactly $n$ and $m$. + + _Correctness._ ($arrow.r.double$) Let $chi: U -> {0, 1}$ split every source subset, and assign $x_u = chi(u)$. Removing duplicates does not remove either color from a split subset, so every $D_j$ contains elements of both colors and $C_j$ has both truth values. Hence every target clause satisfies NAE. ($arrow.l.double$) Let $bold(x)$ NAE-satisfy every target clause and color element $u$ by $chi(u) = x_u$. A repeated-literal clause $(x_u, x_u)$ can never satisfy NAE, so no all-repeated source subset can occur in a satisfiable target instance. Every other clause contains both truth values; therefore its canonical sequence $D_j$, and hence the original subset vector $S_j$, contains elements on both sides of the split. Thus $chi$ splits every source subset. + + An all-repeated vector such as $(u, u, dots, u)$ is therefore preserved as a NO constraint: canonicalization finds only $u$, and the emitted $(x_u, x_u)$ is false under both possible values of $x_u$. + + _Solution extraction._ Return the target assignment unchanged: the source color of universe element $u$ is $x_u$. +] + // 6b. NAESatisfiability → PartitionIntoPerfectMatchings (#845) #let nae_ppm = load-example("NAESatisfiability", "PartitionIntoPerfectMatchings") #let nae_ppm_sol = nae_ppm.solutions.at(0) From 649e055f1739300fa02f5235c56461314441c970 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:08:53 +0800 Subject: [PATCH 4/6] Update dominated-rule expectation for new path --- src/unit_tests/rules/analysis.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/unit_tests/rules/analysis.rs b/src/unit_tests/rules/analysis.rs index 6088d9d38..721549244 100644 --- a/src/unit_tests/rules/analysis.rs +++ b/src/unit_tests/rules/analysis.rs @@ -322,6 +322,8 @@ fn test_find_dominated_rules_returns_known_set() { "PartitionIntoPathsOfLength2 {graph: \"SimpleGraph\"}", "ILP {variable: \"bool\"}", ), + // SetSplitting → NAE-SAT → ILP is better than direct SetSplitting → ILP + ("SetSplitting", "ILP {variable: \"bool\"}"), ] .into_iter() .collect(); From f59e9a9cdaea0d8ac9733180b43ed7b84669e28c Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:09:01 +0800 Subject: [PATCH 5/6] chore: remove plan file after implementation --- ...08-02-setsplitting-to-naesatisfiability.md | 57 ------------------- 1 file changed, 57 deletions(-) delete mode 100644 docs/plans/2026-08-02-setsplitting-to-naesatisfiability.md diff --git a/docs/plans/2026-08-02-setsplitting-to-naesatisfiability.md b/docs/plans/2026-08-02-setsplitting-to-naesatisfiability.md deleted file mode 100644 index 697eaa5ce..000000000 --- a/docs/plans/2026-08-02-setsplitting-to-naesatisfiability.md +++ /dev/null @@ -1,57 +0,0 @@ -# SetSplitting to NAESatisfiability implementation plan - -Issue: #1100 `[Rule] SetSplitting to NAESatisfiability` - -The implementation follows the repository `add-rule` workflow. Both models use -`Or`, so the reduction is witness-capable through `ReduceTo`. -The construction encodes element `u` as positive, one-indexed literal `u + 1`, -deduplicates each source subset while preserving first-occurrence order, and -emits `(x_u, x_u)` when a subset contains only repetitions of one element. - -## Batch 1: verify and implement the rule - -1. Run the `verify-reduction` workflow before writing Rust: - - prove that a source subset is split exactly when its positive-literal NAE - clause contains both truth values; - - cover the all-repeated subset with the unsatisfiable repeated-literal - clause; - - verify direct witness extraction and the overhead bounds - `num_vars = universe_size`, `num_clauses = num_subsets`, and - `num_literals <= (universe_size + 1) * num_subsets`; - - run independent constructor and adversary checks with at least 5,000 - checks each and cross-compare their target construction. -2. Add `src/rules/setsplitting_naesatisfiability.rs` with a direct - `ReductionResult`, identity witness extraction, deterministic first-seen - deduplication, `CNFClause` construction, and the required overhead metadata. -3. Register the module in `src/rules/mod.rs` without introducing any dispatch - layer or compatibility path. -4. Add focused tests in - `src/unit_tests/rules/setsplitting_naesatisfiability.rs`: - - closed-loop feasibility and witness extraction for the issue example; - - exact target structure and overhead bounds; - - repeated members and the all-repeated infeasible case; - - empty family, unused universe elements, and clauses of arity two through - greater than three; - - canonical example-db output. -5. Add the issue's four-element example to the rule's - `canonical_rule_example_specs()` implementation and ensure the existing - example-db collector discovers it. - -## Batch 2: paper documentation and generated fixtures - -1. With fresh context after Batch 1, add a self-contained - `reduction-rule("SetSplitting", "NAESatisfiability", ...)` entry to - `docs/paper/reductions.typ`, following the existing reverse rule and the - KColoring-to-QUBO tutorial structure. -2. Describe the construction, both correctness directions, identity solution - extraction, duplicate canonicalization, and the all-repeated NO case. -3. Build the worked example from the canonical example-db fixture and begin its - `extra:` block with the `pred-commands()` create/reduce/solve/evaluate flow. -4. Regenerate the reduction graph, schemas, and example-db fixtures, then run - `make paper`. - -## Final verification - -Run formatting, tests, and clippy (`make fmt-check`, `make test`, and -`make clippy`). Confirm that tracked changes are limited to the rule, -registration, tests, canonical fixture/export updates, and paper entry. From 45d01c335d5fb39a5db734a3be45623d32726ec0 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:54:51 +0800 Subject: [PATCH 6/6] fix: address PR #1109 review comments - add a five-element satisfiable closed-loop test - add a non-degenerate infeasible odd-cycle test --- .../rules/setsplitting_naesatisfiability.rs | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/unit_tests/rules/setsplitting_naesatisfiability.rs b/src/unit_tests/rules/setsplitting_naesatisfiability.rs index 436325a6c..312202464 100644 --- a/src/unit_tests/rules/setsplitting_naesatisfiability.rs +++ b/src/unit_tests/rules/setsplitting_naesatisfiability.rs @@ -21,6 +21,28 @@ fn test_setsplitting_to_naesatisfiability_closed_loop() { assert_eq!(reduction.extract_solution(&[0, 1, 0, 1]), vec![0, 1, 0, 1]); } +#[test] +fn test_setsplitting_to_naesatisfiability_five_element_closed_loop() { + let source = SetSplitting::new(5, vec![vec![0, 1], vec![1, 2, 3], vec![0, 2, 3, 4]]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "five-element SetSplitting -> NAE-SAT", + ); +} + +#[test] +fn test_setsplitting_to_naesatisfiability_odd_cycle_is_infeasible() { + let source = SetSplitting::new(3, vec![vec![0, 1], vec![1, 2], vec![0, 2]]); + let reduction = ReduceTo::::reduce_to(&source); + let solver = BruteForce::new(); + + assert!(solver.find_witness(&source).is_none()); + assert!(solver.find_witness(reduction.target_problem()).is_none()); +} + #[test] fn test_setsplitting_to_naesatisfiability_structure_and_overhead() { let source = issue_example();