Fix #126: Add KSatisfiability to SubsetSum reduction

docs/paper/reductions.typ

@@ -52,6 +52,7 @@
   "BicliqueCover": [Biclique Cover],
   "BinPacking": [Bin Packing],
   "ClosestVectorProblem": [Closest Vector Problem],
+  "SubsetSum": [Subset Sum],
 )
 
 // Definition label: "def:<ProblemName>" — 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$).
 ][

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<i64>",
+        "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)",

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"
     }
   ]
-}
+}

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::<K3>::new(3, clauses);
+    println!("Source: KSatisfiability<K3> 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::<SubsetSum>::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::<K3>::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::<K3>::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()
+}

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::<ClosestVectorProblem<i32>>(data),
         },
         "Knapsack" => deser_opt::<Knapsack>(data),
+        "SubsetSum" => deser_sat::<SubsetSum>(data),
         _ => bail!("{}", crate::problem_name::unknown_problem_error(&canonical)),
     }
 }
@@ -305,6 +306,7 @@ pub fn serialize_any_problem(
             _ => try_ser::<ClosestVectorProblem<i32>>(any),
         },
         "Knapsack" => try_ser::<Knapsack>(any),
+        "SubsetSum" => try_ser::<SubsetSum>(any),
         _ => bail!("{}", crate::problem_name::unknown_problem_error(&canonical)),
     }
 }

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
     }
 }

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

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;