diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 8e0462b7a..448a554b8 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -19402,6 +19402,110 @@ The following table shows concrete target-variable counts for example instances, _Solution extraction._ The X3C configuration equals the Subset Product configuration: select subset $j$ iff $x_j = 1$. ] +// OneInThreeSatisfiability → SubsetProduct (#1201) +#let oit_sp = load-example("OneInThreeSatisfiability", "SubsetProduct") +#let oit_sp_sol = oit_sp.solutions.at(0) +#reduction-rule("OneInThreeSatisfiability", "SubsetProduct", + example: true, + example-caption: [$n = #oit_sp.source.instance.num_vars$ variables, $m = #oit_sp.source.instance.clauses.len()$ clauses], + extra: [ + #pred-commands( + "pred create --example " + rule-spec(oit_sp) + " -o oit.json", + "pred reduce oit.json --via route.json -o bundle.json", + "pred solve bundle.json", + "pred evaluate oit.json --config " + cli-config(oit_sp_sol.source_config), + ) + + #{ + let n = oit_sp.source.instance.num_vars + let clauses = oit_sp.source.instance.clauses.map(c => c.literals) + let m = clauses.len() + let sizes = oit_sp.target.instance.sizes.map(int) + let big-b = int(oit_sp.target.instance.target) + // First k primes by trial division. + let first-primes(k) = { + let ps = () + let c = 2 + while ps.len() < k { + if ps.all(p => calc.rem(c, p) != 0) { ps.push(c) } + c += 1 + } + ps + } + let primes = first-primes(n + m) + let lit(l) = if l > 0 [$x_#l$] else [$not x_#(-l)$] + // Items of the construction for any clause list: index 2i is false, 2i + 1 true. + let build(n, clauses) = { + let ps = first-primes(n + clauses.len()) + let items = () + for i in range(n) { + for t in range(2) { + let v = ps.at(i) + for (j, cl) in clauses.enumerate() { + for l in cl { + if l == (i + 1) * (if t == 1 { 1 } else { -1 }) { v = v * ps.at(n + j) } + } + } + items.push(v) + } + } + (items, ps.fold(1, (a, b) => a * b)) + } + // Prime factorization of an item, as a product. + let factored(v) = { + let fs = () + let rest = v + for p in primes { + while calc.rem(rest, p) == 0 { + fs.push(p) + rest = calc.quo(rest, p) + } + } + fs.map(str).join($dot$) + } + let (items, b) = build(n, clauses) + assert(items == sizes) + assert(b == big-b) + let chosen = oit_sp_sol.target_config.enumerate().filter(((i, x)) => x).map(((i, x)) => i) + let product = chosen.map(i => sizes.at(i)).fold(1, (a, b) => a * b) + assert(product == big-b) + let true-pos = range(n).map(i => 2 * i + 1) + assert(oit_sp_sol.source_config == true-pos.map(i => oit_sp_sol.target_config.at(i))) + [ + *Step 1 -- Source instance.* The fixture has $n = #n$ variables and the clauses #clauses.enumerate().map(((j, c)) => [$C_#(j + 1) = (#c.map(lit).join($, $))$]).join([, ]). Exactly one literal occurrence must be true in every clause. + + *Step 2 -- Assign primes.* Variables get the primes $(p_1, dots, p_#n) = (#primes.slice(0, n).map(str).join(", "))$ and clauses $(q_1, dots, q_#m) = (#primes.slice(n).map(str).join(", "))$. Each variable $x_i$ contributes a false item $p_i dot product_j q_j^(nu^-_(j i))$ and a true item $p_i dot product_j q_j^(nu^+_(j i))$. + + *Step 3 -- Form the items.* The item list in index order is $(#sizes.map(str).join(", "))$, that is #sizes.map(v => [$#v = #factored(v)$]).join([, ]). The target is $B = #big-b = #factored(big-b)$. + + *Step 4 -- Verify the witness.* The selection $(#fmt-values(oit_sp_sol.target_config))$ picks items #chosen.map(i => str(sizes.at(i))).join([, ]), whose product is #chosen.map(i => str(sizes.at(i))).join($dot$)$= #product = B$. Every $p_i$ occurs once, and the exponent of each $q_j$ counts the true occurrences of clause $C_j$, which is one. Reading the true-item positions $#true-pos.map(str).join(", ")$ gives the assignment $(#fmt-values(oit_sp_sol.source_config))$ #sym.checkmark. + + *NO example.* Take three variables and the clauses $(x_1, x_2, x_3)$ and $(not x_1, not x_2, not x_3)$. If $t$ variables are true, the first clause has $t$ true occurrences and the second has $3 - t$, and $t = 1$ together with $3 - t = 1$ is impossible, so the formula has no solution. #{ + let no-clauses = ((1, 2, 3), (-1, -2, -3)) + let (no-items, no-b) = build(3, no-clauses) + let no-primes = first-primes(5) + // No selection of the six items multiplies to B. + for mask in range(64) { + let prod = range(6).filter(i => calc.rem(calc.quo(mask, calc.pow(2, i)), 2) == 1).map(i => no-items.at(i)).fold(1, (a, b) => a * b) + assert(prod != no-b) + } + [The construction gives the items $(#no-items.map(str).join(", "))$ and $B = #no-b$, with variable primes $(#no-primes.slice(0, 3).map(str).join(", "))$ and clause primes $(q_1, q_2) = (#no-primes.slice(3).map(str).join(", "))$. A product equal to $B$ takes exactly one item of each variable, and then the exponents of $q_1$ and $q_2$ are $t$ and $3 - t$, which cannot both be one. All $2^6 = 64$ selections have a product different from $#no-b$, so the target is infeasible too #sym.checkmark.] + } + + *Multiplicity:* The fixture stores one canonical witness. + ] + } + ], +)[ + This reduction is derived directly from unique factorization, in the style of the prime-product reduction from ExactCoverBy3Sets. It assigns $n + m$ primes, creates $2n$ items, and sets the target to the product of all assigned primes; the target has exactly $2n$ items, and its values need $O((n + m) log(n + m + 2))$ bits. +][ + _Construction._ Let the formula have variables $x_1, dots, x_n$ and clauses $C_1, dots, C_m$, each a triple of signed literal occurrences (repeats and both signs of a variable allowed). Let $p_1, dots, p_n, q_1, dots, q_m$ be the first $n + m$ primes, in order. For variable $x_i$ and clause $C_j$ let $nu^-_(j i)$ and $nu^+_(j i)$ count the occurrences of $not x_i$ and $x_i$ in $C_j$. Create two items per variable, in the order false, true: $a_(i,0) = p_i product_j q_j^(nu^-_(j i))$ and $a_(i,1) = p_i product_j q_j^(nu^+_(j i))$. Set $B = product_i p_i dot product_j q_j$. Equal-valued items remain distinct indices. + + _Correctness._ Take a selection $S$ and write $e_i$ for the number of selected items among $a_(i,0), a_(i,1)$. The only items divisible by $p_i$ are these two, so $p_i$ has exponent $e_i$ in the product. ($arrow.r.double$) If an assignment $alpha$ makes exactly one occurrence true in every clause, select $a_(i,1)$ when $alpha(x_i)$ holds and $a_(i,0)$ otherwise. Each $p_i$ occurs once. The exponent of $q_j$ is the number of occurrences of $C_j$ made true by $alpha$, because an occurrence of $x_i$ is true exactly when the true item is chosen and an occurrence of $not x_i$ exactly when the false item is chosen. That number is one, so the product is $B$. ($arrow.l.double$) Suppose the product is $B$. The exponent of $p_i$ in $B$ is one, so exactly one item of each pair is selected, which defines an assignment $alpha$ with $alpha(x_i)$ true iff $a_(i,1)$ is selected. The exponent of $q_j$ is again the number of true occurrences in $C_j$ under $alpha$ and must equal one, so $alpha$ satisfies every clause. The argument counts occurrences, so repeated literals (exponent up to three) and a variable of both signs in one clause are covered; an unused variable contributes only its private prime, and the empty formula gives no items and $B = 1$. + + _Solution extraction._ Validate that the target selection multiplies to $B$, then return source bit $i$ as the selection bit of the true item, position $2i + 1$ counting from zero. No integer is factored. +] + // ExactCoverBy3Sets → BoundedDiameterSpanningTree (#913) #let x3c_bdst = load-example("ExactCoverBy3Sets", "BoundedDiameterSpanningTree") #let x3c_bdst_sol = x3c_bdst.solutions.at(0) diff --git a/src/models/misc/subset_product.rs b/src/models/misc/subset_product.rs index 4b8a44086..b57083f3d 100644 --- a/src/models/misc/subset_product.rs +++ b/src/models/misc/subset_product.rs @@ -97,7 +97,10 @@ impl SubsetProduct { Self::try_new(sizes, target).unwrap_or_else(|error| panic!("{error}")) } - fn try_new(sizes: Vec, target: T) -> Result + pub(crate) fn try_new( + sizes: Vec, + target: T, + ) -> Result where S: ToBigUint, T: ToBigUint, diff --git a/src/rules/exactcoverby3sets_subsetproduct.rs b/src/rules/exactcoverby3sets_subsetproduct.rs index b184b5942..389d253ce 100644 --- a/src/rules/exactcoverby3sets_subsetproduct.rs +++ b/src/rules/exactcoverby3sets_subsetproduct.rs @@ -41,7 +41,7 @@ impl ReductionResult for ReductionX3CToSubsetProduct { } } -fn product_biguint(values: I) -> BigUint +pub(crate) fn product_biguint(values: I) -> BigUint where I: IntoIterator, { @@ -50,7 +50,7 @@ where }) } -fn assigned_primes(universe_size: usize) -> Vec { +pub(crate) fn assigned_primes(universe_size: usize) -> Vec { match universe_size { 0 => Vec::new(), 1 => vec![2], diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 7606f4923..077b342a0 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -275,6 +275,7 @@ pub(crate) mod multiprocessorscheduling_ilp; pub(crate) mod naesatisfiability_ilp; pub(crate) mod numericalmatchingwithtargetsums_ilp; pub(crate) mod oneinthreesatisfiability_ilp; +pub(crate) mod oneinthreesatisfiability_subsetproduct; pub(crate) mod openshopscheduling_ilp; pub(crate) mod optimallineararrangement_ilp; pub(crate) mod optimumcommunicationspanningtree_ilp; @@ -384,6 +385,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec> for OneInThreeSatisfiability { vec![], ObjectiveSense::Minimize, ) - .map_err(Self::target_construction)?; + .map_err(>>::target_construction)?; Ok(Self::Result { target }) } } diff --git a/src/rules/oneinthreesatisfiability_subsetproduct.rs b/src/rules/oneinthreesatisfiability_subsetproduct.rs new file mode 100644 index 000000000..de175a915 --- /dev/null +++ b/src/rules/oneinthreesatisfiability_subsetproduct.rs @@ -0,0 +1,124 @@ +//! Reduction from OneInThreeSatisfiability to SubsetProduct. +//! +//! Variable `i` receives a private prime `p_i` and clause `j` a prime `q_j`. +//! Each variable has a false item and a true item, both divisible by `p_i`; +//! the exponent of `q_j` in an item counts the literal occurrences of clause +//! `j` that the item makes true. The target is the product of all primes, so by +//! unique factorization a matching subset picks one item per variable and makes +//! exactly one occurrence true in every clause. + +use crate::models::formula::OneInThreeSatisfiability; +use crate::models::misc::SubsetProduct; +use crate::reduction; +use crate::rules::ReductionError; +use crate::rules::exactcoverby3sets_subsetproduct::{assigned_primes, product_biguint}; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use num_bigint::BigUint; + +/// Result of reducing OneInThreeSatisfiability to SubsetProduct. +#[derive(Debug, Clone)] +pub struct ReductionOneInThreeSatisfiabilityToSubsetProduct { + target: SubsetProduct, +} + +impl ReductionResult for ReductionOneInThreeSatisfiabilityToSubsetProduct { + type Source = OneInThreeSatisfiability; + type Target = SubsetProduct; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution( + &self, + target_solution: &::Solution, + ) -> crate::rules::ExtractionResult<::Solution> { + crate::rules::traits::validate_target_witness( + self.target_problem(), + target_solution, + |value| value.0, + "target witness does not multiply to the target", + )?; + // Item `2i + 1` is the true item of variable `i`. + Ok(target_solution.iter().skip(1).step_by(2).copied().collect()) + } +} + +/// Two items per variable, with the overflow reported as a reduction error. +fn item_count(num_vars: usize) -> Result { + num_vars.checked_mul(2).ok_or_else(|| { + ReductionError::integer_overflow::( + "doubling the number of variables", + ) + }) +} + +#[crate::aggregate_reduction(identity)] +impl crate::rules::AggregateReductionResult for ReductionOneInThreeSatisfiabilityToSubsetProduct {} + +#[reduction( + transform = exact { + num_elements = "2 * num_vars", + })] +impl ReduceTo for OneInThreeSatisfiability { + type Result = ReductionOneInThreeSatisfiabilityToSubsetProduct; + + fn reduce_to(&self) -> Result { + let num_vars = self.num_vars(); + // `num_vars + num_clauses` cannot overflow once the item count fits: the + // clauses are stored in memory, so there are at most `isize::MAX` of them. + let num_items = item_count(num_vars)?; + let primes = assigned_primes(num_vars + self.num_clauses()); + let (variable_primes, clause_primes) = primes.split_at(num_vars); + + // Items 2i (false) and 2i + 1 (true), each starting at the private prime p_i. + let mut sizes: Vec = Vec::with_capacity(num_items); + for &prime in variable_primes { + sizes.push(BigUint::from(prime)); + sizes.push(BigUint::from(prime)); + } + + // Each literal occurrence multiplies q_j into the item that makes it true. + for (clause, &clause_prime) in self.clauses().iter().zip(clause_primes) { + for (variable, &literal) in clause.variables().into_iter().zip(&clause.literals) { + let item = 2 * variable + usize::from(literal > 0); + sizes[item] *= clause_prime; + } + } + + let target = product_biguint(primes.iter().copied()); + let target = SubsetProduct::try_new(sizes, target) + .map_err(>::target_construction)?; + Ok(ReductionOneInThreeSatisfiabilityToSubsetProduct { target }) + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + use crate::models::formula::CNFClause; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "oneinthreesatisfiability_to_subsetproduct", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, SubsetProduct>( + OneInThreeSatisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, -2, 3]), + CNFClause::new(vec![1, -2, -3]), + ], + ), + SolutionPair { + source_config: serde_json::json!(vec![false, true, false]), + target_config: serde_json::json!(vec![true, false, false, true, true, false]), + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/oneinthreesatisfiability_subsetproduct.rs"] +mod tests; diff --git a/src/unit_tests/rules/oneinthreesatisfiability_subsetproduct.rs b/src/unit_tests/rules/oneinthreesatisfiability_subsetproduct.rs new file mode 100644 index 000000000..2523abdb9 --- /dev/null +++ b/src/unit_tests/rules/oneinthreesatisfiability_subsetproduct.rs @@ -0,0 +1,268 @@ +use super::*; +use crate::models::formula::CNFClause; +use crate::rules::ReductionError; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::traits::Problem; +use crate::types::Or; +use num_bigint::BigUint; + +fn source(num_vars: usize, clauses: &[[i64; 3]]) -> OneInThreeSatisfiability { + OneInThreeSatisfiability::new( + num_vars, + clauses + .iter() + .map(|clause| CNFClause::new(clause.to_vec())) + .collect(), + ) +} + +fn reduce(source: &OneInThreeSatisfiability) -> ReductionOneInThreeSatisfiabilityToSubsetProduct { + ReduceTo::::reduce_to(source).expect("reduction should succeed") +} + +fn sizes_of(target: &SubsetProduct) -> Vec { + target + .sizes() + .iter() + .map(|size| u64::try_from(size).unwrap()) + .collect() +} + +fn assignments(num_vars: usize) -> impl Iterator> { + (0..1usize << num_vars).map(move |mask| (0..num_vars).map(|i| mask >> i & 1 == 1).collect()) +} + +/// Checks the whole target-witness set against the source assignments. +fn assert_equivalent(source: &OneInThreeSatisfiability) { + let reduction = reduce(source); + let target = reduction.target_problem(); + assert_eq!(target.num_elements(), 2 * source.num_vars()); + let mut witnesses = 0usize; + for selection in assignments(target.num_elements()) { + let target_value = target.evaluate(&selection).unwrap().0; + if target_value { + witnesses += 1; + let extracted = reduction.extract_solution(&selection).unwrap(); + assert!(source.evaluate(&extracted).unwrap().0); + for (i, &value) in extracted.iter().enumerate() { + assert_ne!(selection[2 * i], selection[2 * i + 1]); + assert_eq!(selection[2 * i + 1], value); + } + } else { + assert!(reduction.extract_solution(&selection).is_err()); + } + } + let satisfying = assignments(source.num_vars()) + .filter(|assignment| source.evaluate(assignment).unwrap().0) + .count(); + assert_eq!(witnesses, satisfying); +} + +#[test] +fn test_oneinthreesatisfiability_to_subsetproduct_yes_example() { + let source = source(3, &[[1, 2, 3], [-1, -2, 3], [1, -2, -3]]); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(sizes_of(target), vec![22, 182, 429, 21, 65, 385]); + assert_eq!(target.target(), &BigUint::from(30030u64)); + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "OneInThreeSatisfiability -> SubsetProduct closed loop", + ); + + let witness = vec![true, false, false, true, true, false]; + assert!(target.evaluate(&witness).unwrap().0); + assert_eq!( + reduction.extract_solution(&witness).unwrap(), + vec![false, true, false] + ); + // It is the only witness. + let count = assignments(6) + .filter(|selection| target.evaluate(selection).unwrap().0) + .count(); + assert_eq!(count, 1); +} + +#[test] +fn test_oneinthreesatisfiability_to_subsetproduct_no_example() { + let source = source(3, &[[1, 2, 3], [-1, -2, -3]]); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(sizes_of(target), vec![22, 14, 33, 21, 55, 35]); + assert_eq!(target.target(), &BigUint::from(2310u64)); + assert!(assignments(3).all(|a| !source.evaluate(&a).unwrap().0)); + assert!(assignments(6).all(|s| !target.evaluate(&s).unwrap().0)); + assert_equivalent(&source); +} + +#[test] +fn test_oneinthreesatisfiability_to_subsetproduct_all_single_clauses() { + // Every ordered clause over three variables: repeats and both signs included. + let literals = [-3i64, -2, -1, 1, 2, 3]; + for a in literals { + for b in literals { + for c in literals { + assert_equivalent(&source(3, &[[a, b, c]])); + } + } + } +} + +#[test] +fn test_oneinthreesatisfiability_to_subsetproduct_all_clause_pairs() { + let literals = [-2i64, -1, 1, 2]; + let mut clauses: Vec<[i64; 3]> = Vec::new(); + for a in literals { + for b in literals { + for c in literals { + clauses.push([a, b, c]); + } + } + } + for first in &clauses { + for second in &clauses { + assert_equivalent(&source(2, &[*first, *second])); + } + } +} + +#[test] +fn test_oneinthreesatisfiability_to_subsetproduct_five_variables() { + assert_equivalent(&source( + 5, + &[[1, 2, 3], [-3, 4, 5], [1, -4, -5], [2, -2, 5]], + )); + assert_equivalent(&source(5, &[[1, 1, 2], [3, 4, 5], [-1, -2, 5]])); +} + +#[test] +fn test_oneinthreesatisfiability_to_subsetproduct_special_cases() { + // Repeated literal: exponent 3 on the true item, 0 on the false item. + let triple = reduce(&source(1, &[[1, 1, 1]])); + assert_eq!(sizes_of(triple.target_problem()), vec![2, 2 * 27]); + assert_equivalent(&source(1, &[[1, 1, 1]])); + assert_equivalent(&source(1, &[[-1, -1, -1]])); + let double = reduce(&source(2, &[[1, 1, 2]])); + assert_eq!(sizes_of(double.target_problem()), vec![2, 2 * 25, 3, 3 * 5]); + + // Both signs of one variable in one clause: equal-valued items stay two indices. + let both = reduce(&source(2, &[[1, -1, 2]])); + assert_eq!(sizes_of(both.target_problem()), vec![10, 10, 3, 15]); + assert_equivalent(&source(2, &[[1, -1, 2]])); + + // Unused variables and no clauses: two equal items per variable, 2^n witnesses. + let unused = reduce(&source(3, &[])); + assert_eq!(sizes_of(unused.target_problem()), vec![2, 2, 3, 3, 5, 5]); + assert_eq!(unused.target_problem().target(), &BigUint::from(30u64)); + assert_equivalent(&source(3, &[])); + assert_equivalent(&source(4, &[[1, 2, 2]])); + + // Empty instance: no items, target 1, the empty selection is the witness. + let empty = reduce(&source(0, &[])); + assert_eq!(empty.target_problem().num_elements(), 0); + assert_eq!(empty.target_problem().target(), &BigUint::from(1u64)); + assert_eq!(empty.extract_solution(&vec![]).unwrap(), Vec::::new()); + assert_equivalent(&source(0, &[])); +} + +#[test] +fn test_oneinthreesatisfiability_to_subsetproduct_uses_first_primes_exactly() { + // 6 variables and 6 clauses: the first twelve primes, each with exponent one in the target. + let clauses: Vec<[i64; 3]> = (1..=6).map(|j| [j, -((j % 6) + 1), 1]).collect(); + let reduction = reduce(&source(6, &clauses)); + let primes: u64 = 2 * 3 * 5 * 7 * 11 * 13 * 17 * 19 * 23 * 29 * 31 * 37; + assert_eq!(reduction.target_problem().target(), &BigUint::from(primes)); +} + +#[test] +fn test_oneinthreesatisfiability_to_subsetproduct_large_numbers_exceed_u64() { + // 20 variables, 30 clauses (target B has 50 prime factors, far beyond 64 bits), planted assignment: in every clause the first literal is true + // under it and the other two are false, so it is satisfying by construction. + let planted: Vec = (0..20).map(|i| i % 3 != 0).collect(); + let signed = |variable: usize, want_true: bool| { + let literal = variable as i64 + 1; + if planted[variable] == want_true { + literal + } else { + -literal + } + }; + let clauses: Vec<[i64; 3]> = (0..30) + .map(|j| { + let (a, b, c) = (j % 20, (j + 7) % 20, (j + 13) % 20); + [signed(a, true), signed(b, false), signed(c, false)] + }) + .collect(); + let source = source(20, &clauses); + // The three variables of a clause are distinct, so the planted assignment satisfies it. + assert!(source.evaluate(&planted).unwrap().0); + + let reduction = reduce(&source); + let target = reduction.target_problem(); + assert_eq!(target.num_elements(), 40); + assert!(target.target().bits() > 64); + + let selection: Vec = planted.iter().flat_map(|&v| [!v, v]).collect(); + assert!(target.evaluate(&selection).unwrap().0); + assert_eq!(reduction.extract_solution(&selection).unwrap(), planted); + // Flipping one variable breaks the product. + let mut flipped = selection.clone(); + flipped.swap(0, 1); + assert!(!target.evaluate(&flipped).unwrap().0); + assert!(reduction.extract_solution(&flipped).is_err()); + // Products are exact: selecting every item overshoots the target. + assert!(!target.evaluate(&vec![true; 40]).unwrap().0); +} + +#[test] +fn test_oneinthreesatisfiability_to_subsetproduct_extract_rejects_invalid_witnesses() { + let source = source(3, &[[1, 2, 3], [-1, -2, 3], [1, -2, -3]]); + let reduction = reduce(&source); + // A non-solution of the right length. + assert!(reduction.extract_solution(&vec![false; 6]).is_err()); + // Both items of a pair selected. + assert!( + reduction + .extract_solution(&vec![true, true, false, true, true, false]) + .is_err() + ); + // Wrong lengths. + assert!(reduction.extract_solution(&vec![]).is_err()); + assert!(reduction.extract_solution(&vec![true; 5]).is_err()); + assert!(reduction.extract_solution(&vec![true; 7]).is_err()); +} + +#[test] +fn test_oneinthreesatisfiability_to_subsetproduct_identity_value_mapping() { + let yes = source(3, &[[1, 2, 3], [-1, -2, 3], [1, -2, -3]]); + let no = source(3, &[[1, 2, 3], [-1, -2, -3]]); + for (source, feasible) in [(yes, true), (no, false)] { + let reduction = reduce(&source); + let target_feasible = crate::solvers::BruteForce::new() + .solve(reduction.target_problem()) + .unwrap() + .is_some(); + let source_value = + crate::rules::AggregateReductionResult::extract_value(&reduction, Or(target_feasible)); + assert_eq!(source_value, Or(feasible)); + } +} + +#[test] +fn test_oneinthreesatisfiability_to_subsetproduct_item_count_boundary() { + // The source model caps variables at i64::MAX, so the doubling can only fail on narrower + // targets; the helper is checked at the boundary on both sides. + assert_eq!(item_count(0).unwrap(), 0); + assert_eq!(item_count(7).unwrap(), 14); + assert_eq!(item_count(usize::MAX / 2).unwrap(), usize::MAX - 1); + let error = item_count(usize::MAX / 2 + 1).unwrap_err(); + assert!(matches!(error, ReductionError::IntegerOverflow { .. })); + assert!(error.to_string().contains("doubling")); + assert!(matches!( + item_count(usize::MAX), + Err(ReductionError::IntegerOverflow { .. }) + )); +}