diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 915878827..67730248d 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -52,6 +52,7 @@ "BicliqueCover": [Biclique Cover], "BinPacking": [Bin Packing], "ClosestVectorProblem": [Closest Vector Problem], + "SubsetSum": [Subset Sum], ) // Definition label: "def:" — each definition block must have a matching label @@ -895,6 +896,14 @@ Biclique Cover is equivalent to factoring the biadjacency matrix $M$ of the bipa *Example.* Let $n = 4$ items with weights $(2, 3, 4, 5)$, values $(3, 4, 5, 7)$, and capacity $C = 7$. Selecting $S = {1, 2}$ (items with weights 3 and 4) gives total weight $3 + 4 = 7 lt.eq C$ and total value $4 + 5 = 9$. Selecting $S = {0, 3}$ (weights 2 and 5) gives weight $2 + 5 = 7 lt.eq C$ and value $3 + 7 = 10$, which is optimal. ] +#problem-def("SubsetSum")[ + Given a finite set $A = {a_0, dots, a_(n-1)}$ with sizes $s(a_i) in ZZ^+$ and a target $B in ZZ^+$, determine whether there exists a subset $A' subset.eq A$ such that $sum_(a in A') s(a) = B$. +][ + One of Karp's 21 NP-complete problems @karp1972. Subset Sum is the special case of Knapsack where $v_i = w_i$ for all items and we seek an exact sum rather than an inequality. Though NP-complete, it is only _weakly_ NP-hard: a dynamic-programming algorithm runs in $O(n B)$ pseudo-polynomial time. The best known exact algorithm is the $O^*(2^(n slash 2))$ meet-in-the-middle approach of Horowitz and Sahni @horowitz1974. + + *Example.* Let $A = {3, 7, 1, 8, 2, 4}$ ($n = 6$) and target $B = 11$. Selecting $A' = {3, 8}$ gives sum $3 + 8 = 11 = B$. Another solution: $A' = {7, 4}$ with sum $7 + 4 = 11 = B$. +] + // Completeness check: warn about problem types in JSON but missing from paper #{ let json-models = { @@ -1125,6 +1134,33 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ Discard auxiliary variables: return $bold(x)[0..n]$. ] +#let ksat_ss = load-example("ksatisfiability_to_subsetsum") +#let ksat_ss_r = load-results("ksatisfiability_to_subsetsum") +#let ksat_ss_sol = ksat_ss_r.solutions.at(0) +#reduction-rule("KSatisfiability", "SubsetSum", + example: true, + example-caption: [3-SAT with 3 variables and 2 clauses], + extra: [ + Source: $n = #ksat_ss.source.instance.num_vars$ variables, $m = #ksat_ss.source.instance.num_clauses$ clauses \ + Target: #ksat_ss.target.instance.num_elements elements, target $= #ksat_ss.target.instance.target$ \ + Source config: #ksat_ss_sol.source_config #h(1em) Target config: #ksat_ss_sol.target_config + ], +)[ + Classical Karp reduction @karp1972 using base-10 digit encoding. Each integer has $(n + m)$ digits, where the first $n$ positions correspond to variables and the last $m$ to clauses. For variable $x_i$, two integers $y_i, z_i$ encode positive and negative literal occurrences. For clause $C_j$, slack integers $g_j, h_j$ pad the clause digit to exactly 4. Since each clause has at most 3 literals and slacks add at most 2, no digit exceeds 5, so no carries occur. +][ + _Construction._ Given a 3-CNF formula $phi$ with $n$ variables and $m$ clauses, create $2n + 2m$ integers in $(n+m)$-digit base-10 representation: + + (i) _Variable integers_ ($2n$): For each $x_i$, create $y_i$ with $d_i = 1$ and $d_(n+j) = 1$ if $x_i in C_j$, and $z_i$ with $d_i = 1$ and $d_(n+j) = 1$ if $overline(x_i) in C_j$. + + (ii) _Slack integers_ ($2m$): For each clause $C_j$, create $g_j$ with $d_(n+j) = 1$ and $h_j$ with $d_(n+j) = 2$. + + (iii) _Target_ $T$: $d_i = 1$ for $i in [1, n]$ and $d_(n+j) = 4$ for $j in [1, m]$. + + _Correctness._ ($arrow.r.double$) If assignment $alpha$ satisfies $phi$, select $y_i$ when $x_i = top$ and $z_i$ when $x_i = bot$. Variable digits sum to exactly 1 (one of $y_i, z_i$ per variable). Each satisfied clause has 1--3 true literals contributing 1--3 to its digit; slacks $g_j, h_j$ with values 1, 2 can pad any value in ${1, 2, 3}$ to 4. ($arrow.l.double$) Variable digits force exactly one of $y_i, z_i$ per variable, defining a truth assignment. Clause digits reach 4 only if the literal contribution is $>= 1$, meaning each clause is satisfied. + + _Solution extraction._ For each $i$: if $y_i$ is selected ($x_(2i) = 1$), set $x_i = 1$; if $z_i$ is selected ($x_(2i+1) = 1$), set $x_i = 0$. +] + #reduction-rule("ILP", "QUBO")[ A binary ILP optimizes a linear objective over binary variables subject to linear constraints. The penalty method converts each equality constraint $bold(a)_k^top bold(x) = b_k$ into the quadratic penalty $(bold(a)_k^top bold(x) - b_k)^2$, which is zero if and only if the constraint is satisfied. Inequality constraints are first converted to equalities using binary slack variables with powers-of-two coefficients. The resulting unconstrained quadratic over binary variables is a QUBO whose matrix $Q$ combines the negated objective (as diagonal terms) with the expanded constraint penalties (as a Gram matrix $A^top A$). ][ diff --git a/docs/src/reductions/problem_schemas.json b/docs/src/reductions/problem_schemas.json index 50d327e9b..ea93e5f67 100644 --- a/docs/src/reductions/problem_schemas.json +++ b/docs/src/reductions/problem_schemas.json @@ -397,6 +397,22 @@ } ] }, + { + "name": "SubsetSum", + "description": "Find a subset of integers that sums to exactly a target value", + "fields": [ + { + "name": "sizes", + "type_name": "Vec", + "description": "Integer sizes s(a) for each element" + }, + { + "name": "target", + "type_name": "i64", + "description": "Target sum B" + } + ] + }, { "name": "TravelingSalesman", "description": "Find minimum weight Hamiltonian cycle in a graph (Traveling Salesman Problem)", diff --git a/docs/src/reductions/reduction_graph.json b/docs/src/reductions/reduction_graph.json index e189c002a..dcef7eae0 100644 --- a/docs/src/reductions/reduction_graph.json +++ b/docs/src/reductions/reduction_graph.json @@ -1,14 +1,3 @@ -{ - "nodes": [ - { - "name": "BMF", - "variant": {}, - "category": "algebraic", - "doc_path": "models/algebraic/struct.BMF.html", - "complexity": "2^(rows * rank + r -Exported to: docs/src/reductions/reduction_graph.json - -JSON content: { "nodes": [ { @@ -386,6 +375,13 @@ JSON content: "doc_path": "models/graph/struct.SpinGlass.html", "complexity": "2^num_spins" }, + { + "name": "SubsetSum", + "variant": {}, + "category": "misc", + "doc_path": "models/misc/struct.SubsetSum.html", + "complexity": "2^(num_elements / 2)" + }, { "name": "TravelingSalesman", "variant": { @@ -577,6 +573,17 @@ JSON content: ], "doc_path": "rules/ksatisfiability_qubo/index.html" }, + { + "source": 16, + "target": 41, + "overhead": [ + { + "field": "num_elements", + "formula": "2 * num_vars + 2 * num_clauses" + } + ], + "doc_path": "rules/ksatisfiability_subsetsum/index.html" + }, { "source": 17, "target": 38, @@ -1140,7 +1147,7 @@ JSON content: "doc_path": "rules/spinglass_casts/index.html" }, { - "source": 41, + "source": 42, "target": 8, "overhead": [ { @@ -1155,4 +1162,4 @@ JSON content: "doc_path": "rules/travelingsalesman_ilp/index.html" } ] -} +} \ No newline at end of file diff --git a/examples/reduction_ksatisfiability_to_subsetsum.rs b/examples/reduction_ksatisfiability_to_subsetsum.rs new file mode 100644 index 000000000..92634e35a --- /dev/null +++ b/examples/reduction_ksatisfiability_to_subsetsum.rs @@ -0,0 +1,131 @@ +// # K-Satisfiability (3-SAT) to SubsetSum Reduction (Karp 1972) +// +// ## Mathematical Relationship +// The classical Karp reduction encodes a 3-CNF formula as a SubsetSum instance +// using base-10 digit positions. Each integer has (n + m) digits where n is the +// number of variables and m is the number of clauses. Variable digits ensure +// exactly one truth value per variable; clause digits count satisfied literals, +// padded to 4 by slack integers. +// +// No carries occur because the maximum digit sum is at most 3 + 2 = 5 < 10. +// +// ## This Example +// - Instance: 3-SAT formula (x₁ ∨ x₂ ∨ x₃) ∧ (¬x₁ ∨ ¬x₂ ∨ x₃) +// - n = 3 variables, m = 2 clauses +// - SubsetSum: 10 integers (2n + 2m) with 5-digit (n + m) encoding +// - Target: T = 11144 +// +// ## Outputs +// - `docs/paper/examples/ksatisfiability_to_subsetsum.json` — reduction structure +// - `docs/paper/examples/ksatisfiability_to_subsetsum.result.json` — solutions +// +// ## Usage +// ```bash +// cargo run --example reduction_ksatisfiability_to_subsetsum +// ``` + +use problemreductions::export::*; +use problemreductions::prelude::*; +use problemreductions::variant::K3; + +pub fn run() { + println!("=== K-Satisfiability (3-SAT) -> SubsetSum Reduction ===\n"); + + // 3-SAT: (x₁ ∨ x₂ ∨ x₃) ∧ (¬x₁ ∨ ¬x₂ ∨ x₃) + let clauses = vec![ + CNFClause::new(vec![1, 2, 3]), // x₁ ∨ x₂ ∨ x₃ + CNFClause::new(vec![-1, -2, 3]), // ¬x₁ ∨ ¬x₂ ∨ x₃ + ]; + + let ksat = KSatisfiability::::new(3, clauses); + println!("Source: KSatisfiability with 3 variables, 2 clauses"); + println!(" C1: x1 OR x2 OR x3"); + println!(" C2: NOT x1 OR NOT x2 OR x3"); + + // Reduce to SubsetSum + let reduction = ReduceTo::::reduce_to(&ksat); + let subsetsum = reduction.target_problem(); + + println!( + "\nTarget: SubsetSum with {} elements, target = {}", + subsetsum.num_elements(), + subsetsum.target() + ); + println!("Elements: {:?}", subsetsum.sizes()); + + // Solve SubsetSum with brute force + let solver = BruteForce::new(); + let ss_solutions = solver.find_all_satisfying(subsetsum); + + println!("\nSatisfying solutions:"); + let mut solutions = Vec::new(); + for sol in &ss_solutions { + let extracted = reduction.extract_solution(sol); + let assignment: Vec<&str> = extracted + .iter() + .map(|&x| if x == 1 { "T" } else { "F" }) + .collect(); + let satisfied = ksat.evaluate(&extracted); + println!( + " x = [{}] -> formula {}", + assignment.join(", "), + if satisfied { + "SATISFIED" + } else { + "NOT SATISFIED" + } + ); + assert!(satisfied, "Extracted solution must satisfy the formula"); + + solutions.push(SolutionPair { + source_config: extracted, + target_config: sol.clone(), + }); + } + + println!( + "\nVerification passed: all {} SubsetSum solutions map to satisfying assignments", + ss_solutions.len() + ); + + // Export JSON + let source_variant = variant_to_map(KSatisfiability::::variant()); + let target_variant = variant_to_map(SubsetSum::variant()); + let overhead = lookup_overhead( + "KSatisfiability", + &source_variant, + "SubsetSum", + &target_variant, + ) + .expect("KSatisfiability -> SubsetSum overhead not found"); + + let data = ReductionData { + source: ProblemSide { + problem: KSatisfiability::::NAME.to_string(), + variant: source_variant, + instance: serde_json::json!({ + "num_vars": ksat.num_vars(), + "num_clauses": ksat.clauses().len(), + "k": 3, + }), + }, + target: ProblemSide { + problem: SubsetSum::NAME.to_string(), + variant: target_variant, + instance: serde_json::json!({ + "num_elements": subsetsum.num_elements(), + "sizes": subsetsum.sizes(), + "target": subsetsum.target(), + }), + }, + overhead: overhead_to_json(&overhead), + }; + + let results = ResultData { solutions }; + let name = "ksatisfiability_to_subsetsum"; + write_example(name, &data, &results); +} + +fn main() { + run() +} diff --git a/problemreductions-cli/src/dispatch.rs b/problemreductions-cli/src/dispatch.rs index 7a8498421..72bc23997 100644 --- a/problemreductions-cli/src/dispatch.rs +++ b/problemreductions-cli/src/dispatch.rs @@ -1,6 +1,6 @@ use anyhow::{bail, Context, Result}; use problemreductions::models::algebraic::{ClosestVectorProblem, ILP}; -use problemreductions::models::misc::{BinPacking, Knapsack}; +use problemreductions::models::misc::{BinPacking, Knapsack, SubsetSum}; use problemreductions::prelude::*; use problemreductions::rules::{MinimizeSteps, ReductionGraph}; use problemreductions::solvers::{BruteForce, ILPSolver, Solver}; @@ -245,6 +245,7 @@ pub fn load_problem( _ => deser_opt::>(data), }, "Knapsack" => deser_opt::(data), + "SubsetSum" => deser_sat::(data), _ => bail!("{}", crate::problem_name::unknown_problem_error(&canonical)), } } @@ -305,6 +306,7 @@ pub fn serialize_any_problem( _ => try_ser::>(any), }, "Knapsack" => try_ser::(any), + "SubsetSum" => try_ser::(any), _ => bail!("{}", crate::problem_name::unknown_problem_error(&canonical)), } } diff --git a/problemreductions-cli/src/problem_name.rs b/problemreductions-cli/src/problem_name.rs index acd9b4b59..cbee6c98d 100644 --- a/problemreductions-cli/src/problem_name.rs +++ b/problemreductions-cli/src/problem_name.rs @@ -52,6 +52,7 @@ pub fn resolve_alias(input: &str) -> String { "binpacking" => "BinPacking".to_string(), "cvp" | "closestvectorproblem" => "ClosestVectorProblem".to_string(), "knapsack" => "Knapsack".to_string(), + "subsetsum" => "SubsetSum".to_string(), _ => input.to_string(), // pass-through for exact names } } diff --git a/src/lib.rs b/src/lib.rs index b0d99699a..34e61c557 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -45,7 +45,7 @@ pub mod prelude { KColoring, MaxCut, MaximalIS, MaximumClique, MaximumIndependentSet, MaximumMatching, MinimumDominatingSet, MinimumVertexCover, TravelingSalesman, }; - pub use crate::models::misc::{BinPacking, Factoring, Knapsack, PaintShop}; + pub use crate::models::misc::{BinPacking, Factoring, Knapsack, PaintShop, SubsetSum}; pub use crate::models::set::{MaximumSetPacking, MinimumSetCovering}; // Core traits diff --git a/src/models/misc/mod.rs b/src/models/misc/mod.rs index cdb66e969..36ebe905b 100644 --- a/src/models/misc/mod.rs +++ b/src/models/misc/mod.rs @@ -5,13 +5,16 @@ //! - [`Factoring`]: Integer factorization //! - [`Knapsack`]: 0-1 Knapsack (maximize value subject to weight capacity) //! - [`PaintShop`]: Minimize color switches in paint shop scheduling +//! - [`SubsetSum`]: Find a subset summing to exactly a target value mod bin_packing; pub(crate) mod factoring; mod knapsack; pub(crate) mod paintshop; +mod subset_sum; pub use bin_packing::BinPacking; pub use factoring::Factoring; pub use knapsack::Knapsack; pub use paintshop::PaintShop; +pub use subset_sum::SubsetSum; diff --git a/src/models/misc/subset_sum.rs b/src/models/misc/subset_sum.rs new file mode 100644 index 000000000..ecb520a9c --- /dev/null +++ b/src/models/misc/subset_sum.rs @@ -0,0 +1,109 @@ +//! Subset Sum problem implementation. +//! +//! Given a set of integers and a target value, the problem asks whether any +//! subset sums to exactly the target. One of Karp's original 21 NP-complete +//! problems (1972). + +use crate::registry::{FieldInfo, ProblemSchemaEntry}; +use crate::traits::{Problem, SatisfactionProblem}; +use serde::{Deserialize, Serialize}; + +inventory::submit! { + ProblemSchemaEntry { + name: "SubsetSum", + module_path: module_path!(), + description: "Find a subset of integers that sums to exactly a target value", + fields: &[ + FieldInfo { name: "sizes", type_name: "Vec", description: "Integer sizes s(a) for each element" }, + FieldInfo { name: "target", type_name: "i64", description: "Target sum B" }, + ], + } +} + +/// The Subset Sum problem. +/// +/// Given a set of `n` integers and a target `B`, determine whether there exists +/// a subset whose elements sum to exactly `B`. +/// +/// # Representation +/// +/// Each element has a binary variable: `x_i = 1` if element `i` is selected, +/// `0` otherwise. The problem is satisfiable iff `∑_{i: x_i=1} sizes[i] == target`. +/// +/// # Example +/// +/// ``` +/// use problemreductions::models::misc::SubsetSum; +/// use problemreductions::{Problem, Solver, BruteForce}; +/// +/// let problem = SubsetSum::new(vec![3, 7, 1, 8, 2, 4], 11); +/// let solver = BruteForce::new(); +/// let solution = solver.find_satisfying(&problem); +/// assert!(solution.is_some()); +/// ``` +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct SubsetSum { + sizes: Vec, + target: i64, +} + +impl SubsetSum { + /// Create a new SubsetSum instance. + pub fn new(sizes: Vec, target: i64) -> Self { + Self { sizes, target } + } + + /// Returns the element sizes. + pub fn sizes(&self) -> &[i64] { + &self.sizes + } + + /// Returns the target sum. + pub fn target(&self) -> i64 { + self.target + } + + /// Returns the number of elements. + pub fn num_elements(&self) -> usize { + self.sizes.len() + } +} + +impl Problem for SubsetSum { + const NAME: &'static str = "SubsetSum"; + type Metric = bool; + + fn variant() -> Vec<(&'static str, &'static str)> { + crate::variant_params![] + } + + fn dims(&self) -> Vec { + vec![2; self.num_elements()] + } + + fn evaluate(&self, config: &[usize]) -> bool { + if config.len() != self.num_elements() { + return false; + } + if config.iter().any(|&v| v >= 2) { + return false; + } + let total: i64 = config + .iter() + .enumerate() + .filter(|(_, &x)| x == 1) + .map(|(i, _)| self.sizes[i]) + .sum(); + total == self.target + } +} + +impl SatisfactionProblem for SubsetSum {} + +crate::declare_variants! { + SubsetSum => "2^(num_elements / 2)", +} + +#[cfg(test)] +#[path = "../../unit_tests/models/misc/subset_sum.rs"] +mod tests; diff --git a/src/models/mod.rs b/src/models/mod.rs index 96b4b79d1..fb89aba4b 100644 --- a/src/models/mod.rs +++ b/src/models/mod.rs @@ -15,5 +15,5 @@ pub use graph::{ BicliqueCover, KColoring, MaxCut, MaximalIS, MaximumClique, MaximumIndependentSet, MaximumMatching, MinimumDominatingSet, MinimumVertexCover, SpinGlass, TravelingSalesman, }; -pub use misc::{BinPacking, Factoring, Knapsack, PaintShop}; +pub use misc::{BinPacking, Factoring, Knapsack, PaintShop, SubsetSum}; pub use set::{MaximumSetPacking, MinimumSetCovering}; diff --git a/src/rules/ksatisfiability_subsetsum.rs b/src/rules/ksatisfiability_subsetsum.rs new file mode 100644 index 000000000..1bd3d7352 --- /dev/null +++ b/src/rules/ksatisfiability_subsetsum.rs @@ -0,0 +1,140 @@ +//! Reduction from KSatisfiability (3-SAT) to SubsetSum. +//! +//! Classical Karp reduction using base-10 digit encoding. Each integer has +//! (n + m) digits, where n is the number of variables and m is the number +//! of clauses. Variable digits ensure exactly one of y_i/z_i per variable; +//! clause digits count satisfied literals, padded to 4 by slack integers. +//! +//! No carries occur because the maximum digit sum is at most 3 + 2 = 5 < 10. +//! +//! Reference: Karp 1972; Sipser Theorem 7.56; CLRS §34.5.5 + +use crate::models::formula::KSatisfiability; +use crate::models::misc::SubsetSum; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::variant::K3; + +/// Result of reducing KSatisfiability to SubsetSum. +#[derive(Debug, Clone)] +pub struct Reduction3SATToSubsetSum { + target: SubsetSum, + source_num_vars: usize, +} + +impl ReductionResult for Reduction3SATToSubsetSum { + type Source = KSatisfiability; + type Target = SubsetSum; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + // Variable integers are the first 2n elements in 0-based indexing: + // for variable i (0 <= i < n), y_i is stored at index 2*i and z_i at index 2*i + 1. + // If y_i is selected (target_solution[2*i] == 1), set x_i = 1; otherwise x_i = 0. + (0..self.source_num_vars) + .map(|i| { + let y_selected = target_solution[2 * i] == 1; + if y_selected { + 1 + } else { + 0 + } + }) + .collect() + } +} + +/// Build a base-10 integer from a digit array (most significant first). +/// +/// digits[0] is the most significant digit, digits[num_digits-1] is the least. +fn digits_to_integer(digits: &[i64]) -> i64 { + let mut value: i64 = 0; + for &d in digits { + value = value * 10 + d; + } + value +} + +#[reduction( + overhead = { num_elements = "2 * num_vars + 2 * num_clauses" } +)] +impl ReduceTo for KSatisfiability { + type Result = Reduction3SATToSubsetSum; + + fn reduce_to(&self) -> Self::Result { + let n = self.num_vars(); + let m = self.num_clauses(); + let num_digits = n + m; + assert!( + num_digits <= 18, + "3-SAT to SubsetSum reduction requires n + m <= 18 for i64 encoding \ + (got n={n}, m={m}, n+m={num_digits})" + ); + + let mut sizes = Vec::with_capacity(2 * n + 2 * m); + + // Step 1: Variable integers (2n integers) + for i in 0..n { + // y_i: d_i = 1, d_{n+j} = 1 if x_{i+1} appears positive in C_j + let mut y_digits = vec![0i64; num_digits]; + y_digits[i] = 1; + for (j, clause) in self.clauses().iter().enumerate() { + for &lit in &clause.literals { + let var_idx = (lit.unsigned_abs() as usize) - 1; + if var_idx == i && lit > 0 { + y_digits[n + j] = 1; + } + } + } + sizes.push(digits_to_integer(&y_digits)); + + // z_i: d_i = 1, d_{n+j} = 1 if ¬x_{i+1} appears in C_j + let mut z_digits = vec![0i64; num_digits]; + z_digits[i] = 1; + for (j, clause) in self.clauses().iter().enumerate() { + for &lit in &clause.literals { + let var_idx = (lit.unsigned_abs() as usize) - 1; + if var_idx == i && lit < 0 { + z_digits[n + j] = 1; + } + } + } + sizes.push(digits_to_integer(&z_digits)); + } + + // Step 2: Slack integers (2m integers) + for j in 0..m { + // g_j: d_{n+j} = 1 + let mut g_digits = vec![0i64; num_digits]; + g_digits[n + j] = 1; + sizes.push(digits_to_integer(&g_digits)); + + // h_j: d_{n+j} = 2 + let mut h_digits = vec![0i64; num_digits]; + h_digits[n + j] = 2; + sizes.push(digits_to_integer(&h_digits)); + } + + // Step 3: Target + let mut target_digits = vec![0i64; num_digits]; + for d in target_digits.iter_mut().take(n) { + *d = 1; + } + for d in target_digits.iter_mut().skip(n).take(m) { + *d = 4; + } + let target = digits_to_integer(&target_digits); + + Reduction3SATToSubsetSum { + target: SubsetSum::new(sizes, target), + source_num_vars: n, + } + } +} + +#[cfg(test)] +#[path = "../unit_tests/rules/ksatisfiability_subsetsum.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 80bdb735b..c37af7e0a 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -13,6 +13,7 @@ mod graph; mod kcoloring_casts; mod ksatisfiability_casts; mod ksatisfiability_qubo; +mod ksatisfiability_subsetsum; mod maximumindependentset_casts; mod maximumindependentset_gridgraph; mod maximumindependentset_maximumsetpacking; diff --git a/src/unit_tests/models/misc/subset_sum.rs b/src/unit_tests/models/misc/subset_sum.rs new file mode 100644 index 000000000..5fa113c6b --- /dev/null +++ b/src/unit_tests/models/misc/subset_sum.rs @@ -0,0 +1,107 @@ +use super::*; +use crate::solvers::{BruteForce, Solver}; +use crate::traits::Problem; + +#[test] +fn test_subsetsum_basic() { + let problem = SubsetSum::new(vec![3, 7, 1, 8, 2, 4], 11); + assert_eq!(problem.num_elements(), 6); + assert_eq!(problem.sizes(), &[3, 7, 1, 8, 2, 4]); + assert_eq!(problem.target(), 11); + assert_eq!(problem.dims(), vec![2; 6]); + assert_eq!(::NAME, "SubsetSum"); + assert_eq!(::variant(), vec![]); +} + +#[test] +fn test_subsetsum_evaluate_satisfying() { + let problem = SubsetSum::new(vec![3, 7, 1, 8, 2, 4], 11); + // {3, 8} = 11 + assert!(problem.evaluate(&[1, 0, 0, 1, 0, 0])); + // {7, 4} = 11 + assert!(problem.evaluate(&[0, 1, 0, 0, 0, 1])); +} + +#[test] +fn test_subsetsum_evaluate_unsatisfying() { + let problem = SubsetSum::new(vec![3, 7, 1, 8, 2, 4], 11); + // {3, 7} = 10 ≠ 11 + assert!(!problem.evaluate(&[1, 1, 0, 0, 0, 0])); + // empty = 0 ≠ 11 + assert!(!problem.evaluate(&[0, 0, 0, 0, 0, 0])); +} + +#[test] +fn test_subsetsum_evaluate_wrong_config_length() { + let problem = SubsetSum::new(vec![3, 7, 1], 10); + assert!(!problem.evaluate(&[1, 0])); + assert!(!problem.evaluate(&[1, 0, 0, 0])); +} + +#[test] +fn test_subsetsum_evaluate_invalid_variable_value() { + let problem = SubsetSum::new(vec![3, 7], 10); + assert!(!problem.evaluate(&[2, 0])); +} + +#[test] +fn test_subsetsum_empty_instance() { + // Empty set, target 0: empty subset satisfies + let problem = SubsetSum::new(vec![], 0); + assert_eq!(problem.num_elements(), 0); + assert_eq!(problem.dims(), Vec::::new()); + assert!(problem.evaluate(&[])); +} + +#[test] +fn test_subsetsum_empty_instance_nonzero_target() { + // Empty set, target 5: impossible + let problem = SubsetSum::new(vec![], 5); + assert!(!problem.evaluate(&[])); +} + +#[test] +fn test_subsetsum_brute_force() { + let problem = SubsetSum::new(vec![3, 7, 1, 8, 2, 4], 11); + let solver = BruteForce::new(); + let solution = solver + .find_satisfying(&problem) + .expect("should find a solution"); + assert!(problem.evaluate(&solution)); +} + +#[test] +fn test_subsetsum_brute_force_all() { + let problem = SubsetSum::new(vec![3, 7, 1, 8, 2, 4], 11); + let solver = BruteForce::new(); + let solutions = solver.find_all_satisfying(&problem); + assert!(!solutions.is_empty()); + for sol in &solutions { + assert!(problem.evaluate(sol)); + } +} + +#[test] +fn test_subsetsum_unsatisfiable() { + // Target 100 is unreachable + let problem = SubsetSum::new(vec![1, 2, 3], 100); + let solver = BruteForce::new(); + let solution = solver.find_satisfying(&problem); + assert!(solution.is_none()); +} + +#[test] +fn test_subsetsum_serialization() { + let problem = SubsetSum::new(vec![3, 7, 1, 8, 2, 4], 11); + let json = serde_json::to_value(&problem).unwrap(); + let restored: SubsetSum = serde_json::from_value(json).unwrap(); + assert_eq!(restored.sizes(), problem.sizes()); + assert_eq!(restored.target(), problem.target()); +} + +#[test] +fn test_subsetsum_single_element() { + let problem = SubsetSum::new(vec![5], 5); + assert!(problem.evaluate(&[1])); + assert!(!problem.evaluate(&[0])); +} diff --git a/src/unit_tests/rules/ksatisfiability_subsetsum.rs b/src/unit_tests/rules/ksatisfiability_subsetsum.rs new file mode 100644 index 000000000..42f1fceaa --- /dev/null +++ b/src/unit_tests/rules/ksatisfiability_subsetsum.rs @@ -0,0 +1,161 @@ +use super::*; +use crate::models::formula::CNFClause; +use crate::solvers::{BruteForce, Solver}; +use crate::traits::Problem; +use crate::variant::K3; + +#[test] +fn test_ksatisfiability_to_subsetsum_closed_loop() { + // Issue example: (x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2 ∨ x3), n=3, m=2 + let ksat = KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), // x1 ∨ x2 ∨ x3 + CNFClause::new(vec![-1, -2, 3]), // ¬x1 ∨ ¬x2 ∨ x3 + ], + ); + let reduction = ReduceTo::::reduce_to(&ksat); + let target = reduction.target_problem(); + + // Verify structure: 2*3 + 2*2 = 10 elements + assert_eq!(target.num_elements(), 10); + + // Verify target value: 11144 + assert_eq!(target.target(), 11144); + + let solver = BruteForce::new(); + let solutions = solver.find_all_satisfying(target); + assert!(!solutions.is_empty()); + + // Every SubsetSum solution must map back to a satisfying 3-SAT assignment + for sol in &solutions { + let extracted = reduction.extract_solution(sol); + assert_eq!(extracted.len(), 3); + assert!(ksat.evaluate(&extracted)); + } +} + +#[test] +fn test_ksatisfiability_to_subsetsum_unsatisfiable() { + // Unsatisfiable: (x1) ∧ (¬x1) ∧ (x1) — but 3-SAT needs 3 literals per clause. + // Use: (x1 ∨ x1 ∨ x1) ∧ (¬x1 ∨ ¬x1 ∨ ¬x1) ∧ (x1 ∨ x1 ∨ x1) + // x1=T satisfies C1,C3 but not C2. x1=F satisfies C2 but not C1,C3. + let ksat = KSatisfiability::::new( + 1, + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -1]), + CNFClause::new(vec![1, 1, 1]), + ], + ); + let reduction = ReduceTo::::reduce_to(&ksat); + let target = reduction.target_problem(); + + let solver = BruteForce::new(); + let solution = solver.find_satisfying(target); + assert!(solution.is_none()); +} + +#[test] +fn test_ksatisfiability_to_subsetsum_single_clause() { + // Single clause: (x1 ∨ x2 ∨ x3) — 7 out of 8 assignments satisfy it + let ksat = KSatisfiability::::new(3, vec![CNFClause::new(vec![1, 2, 3])]); + let reduction = ReduceTo::::reduce_to(&ksat); + let target = reduction.target_problem(); + + // 2*3 + 2*1 = 8 elements + assert_eq!(target.num_elements(), 8); + + let solver = BruteForce::new(); + let solutions = solver.find_all_satisfying(target); + + // Each SubsetSum solution maps to a satisfying assignment + let mut sat_assignments = std::collections::HashSet::new(); + for sol in &solutions { + let extracted = reduction.extract_solution(sol); + assert!(ksat.evaluate(&extracted)); + sat_assignments.insert(extracted); + } + // Should find exactly 7 distinct satisfying assignments + assert_eq!(sat_assignments.len(), 7); +} + +#[test] +fn test_ksatisfiability_to_subsetsum_structure() { + // Verify sizes match the issue's example table + let ksat = KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), // x1 ∨ x2 ∨ x3 + CNFClause::new(vec![-1, -2, 3]), // ¬x1 ∨ ¬x2 ∨ x3 + ], + ); + let reduction = ReduceTo::::reduce_to(&ksat); + let target = reduction.target_problem(); + let sizes = target.sizes(); + + // From the issue: + // y1=10010, z1=10001, y2=01010, z2=01001, y3=00111, z3=00100 + // g1=00010, h1=00020, g2=00001, h2=00002 + assert_eq!(sizes[0], 10010); // y1 + assert_eq!(sizes[1], 10001); // z1 + assert_eq!(sizes[2], 1010); // y2 (leading zero dropped) + assert_eq!(sizes[3], 1001); // z2 + assert_eq!(sizes[4], 111); // y3 + assert_eq!(sizes[5], 100); // z3 + assert_eq!(sizes[6], 10); // g1 + assert_eq!(sizes[7], 20); // h1 + assert_eq!(sizes[8], 1); // g2 + assert_eq!(sizes[9], 2); // h2 +} + +#[test] +fn test_ksatisfiability_to_subsetsum_all_negated() { + // All negated: (¬x1 ∨ ¬x2 ∨ ¬x3) — 7 satisfying assignments + let ksat = KSatisfiability::::new(3, vec![CNFClause::new(vec![-1, -2, -3])]); + let reduction = ReduceTo::::reduce_to(&ksat); + let target = reduction.target_problem(); + + let solver = BruteForce::new(); + let solutions = solver.find_all_satisfying(target); + + let mut sat_assignments = std::collections::HashSet::new(); + for sol in &solutions { + let extracted = reduction.extract_solution(sol); + assert!(ksat.evaluate(&extracted)); + sat_assignments.insert(extracted); + } + assert_eq!(sat_assignments.len(), 7); +} + +#[test] +fn test_ksatisfiability_to_subsetsum_extract_solution_example() { + // Verify the specific example from the issue: + // x1=T, x2=T, x3=T → select y1, y2, y3 + slack to reach target 11144 + let ksat = KSatisfiability::::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, -2, 3]), + ], + ); + let reduction = ReduceTo::::reduce_to(&ksat); + let target = reduction.target_problem(); + + // Construct the known subset for x1=T, x2=T, x3=T: + // y1=10010, y2=01010, y3=00111 → variable digits sum: 111, clause digits: 31 + // Need clause digits = 44, so slack: C1 needs +1 (g1=10), C2 needs +3 (g2=1, h2=2) + // Total: 10010 + 01010 + 00111 + 00010 + 00001 + 00002 = 11144 + let specific_config = vec![ + 1, 0, // y1 selected, z1 not + 1, 0, // y2 selected, z2 not + 1, 0, // y3 selected, z3 not + 1, 0, // g1 selected, h1 not + 1, 1, // g2 selected, h2 selected + ]; + assert!(target.evaluate(&specific_config)); + + let extracted = reduction.extract_solution(&specific_config); + assert_eq!(extracted, vec![1, 1, 1]); // x1=T, x2=T, x3=T + assert!(ksat.evaluate(&extracted)); +} diff --git a/tests/suites/examples.rs b/tests/suites/examples.rs index 3c9ad8033..784cf3432 100644 --- a/tests/suites/examples.rs +++ b/tests/suites/examples.rs @@ -20,6 +20,7 @@ example_test!(reduction_ilp_to_qubo); example_test!(reduction_kcoloring_to_ilp); example_test!(reduction_kcoloring_to_qubo); example_test!(reduction_ksatisfiability_to_qubo); +example_test!(reduction_ksatisfiability_to_subsetsum); example_test!(reduction_ksatisfiability_to_satisfiability); example_test!(reduction_maxcut_to_spinglass); example_test!(reduction_maximumclique_to_ilp); @@ -83,6 +84,10 @@ example_fn!( test_ksatisfiability_to_qubo, reduction_ksatisfiability_to_qubo ); +example_fn!( + test_ksatisfiability_to_subsetsum, + reduction_ksatisfiability_to_subsetsum +); example_fn!( test_ksatisfiability_to_satisfiability, reduction_ksatisfiability_to_satisfiability