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) 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/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(); diff --git a/src/unit_tests/rules/setsplitting_naesatisfiability.rs b/src/unit_tests/rules/setsplitting_naesatisfiability.rs new file mode 100644 index 000000000..312202464 --- /dev/null +++ b/src/unit_tests/rules/setsplitting_naesatisfiability.rs @@ -0,0 +1,143 @@ +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_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(); + 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]); +}