docs: improve example instances implementation plan

docs/paper/reductions.typ

@@ -501,9 +501,9 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
 ]
 
 #reduction-rule("KSatisfiability", "QUBO")[
-  Given a Max-2-SAT instance with $m$ clauses over $n$ variables, construct upper-triangular $Q in RR^(n times n)$ where each clause $(ell_i or ell_j)$ contributes a penalty gadget encoding its unique falsifying assignment.
+  Given a Max-$k$-SAT instance with $m$ clauses over $n$ variables, construct a QUBO that counts unsatisfied clauses. For $k = 2$, $Q in RR^(n times n)$ directly encodes quadratic penalties. For $k = 3$, Rosenberg quadratization introduces $m$ auxiliary variables, giving $Q in RR^((n+m) times (n+m))$.
 ][
-  _Construction._ Applying the penalty method (@sec:penalty-method), each 2-literal clause has exactly one falsifying assignment (both literals false). The penalty for that assignment is a quadratic function of $x_i, x_j$:
+  *Case $k = 2$.* Applying the penalty method (@sec:penalty-method), each 2-literal clause has exactly one falsifying assignment (both literals false). The penalty for that assignment is a quadratic function of $x_i, x_j$:
 
   #table(
     columns: (auto, auto, auto, auto),
@@ -517,6 +517,12 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   )
 
   Summing over all clauses, $f(bold(x)) = sum_j "penalty"_j (bold(x))$ counts falsified clauses. Minimizers of $f$ maximize satisfied clauses.
+
+  *Case $k = 3$ (Rosenberg quadratization).* For each clause $(ell_1 or ell_2 or ell_3)$, define complement variables $y_i = overline(ell_i)$ (so $y_i = x_i$ if the literal is negated, $y_i = 1 - x_i$ if positive). The clause is violated when $y_1 y_2 y_3 = 1$. This cubic penalty is reduced to quadratic form by introducing an auxiliary variable $a$ and the substitution $a = y_1 y_2$, enforced via a Rosenberg penalty with weight $M$:
+  $ H = a dot y_3 + M (y_1 y_2 - 2 y_1 a - 2 y_2 a + 3a) $
+  where $M = 2$ suffices. For any binary assignment, if $a = y_1 y_2$ the penalty term vanishes and $H = y_1 y_2 y_3$ counts the clause violation. If $a != y_1 y_2$, the penalty $M(dots.c) >= 1$ makes this suboptimal.
+
+  Each clause adds one auxiliary variable (indices $n, n+1, ..., n+m-1$), so the total QUBO has $n + m$ variables. Solution extraction discards auxiliary variables: return $bold(x)[0..n]$.
 ]
 
 #reduction-rule("ILP", "QUBO")[

docs/plans/2026-02-10-improve-example-instances-impl.md

@@ -1,4 +1,4 @@
-# Improve Example Instances — Implementation Plan
+# Improve Example Instances — Implementation Plan (v2)
 
 > **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task.
 

examples/reduction_circuitsat_to_spinglass.rs

@@ -6,8 +6,11 @@
 //! of gadget Hamiltonians; ground states correspond to satisfying assignments.
 //!
 //! ## This Example
-//! - Instance: Simple AND gate circuit (c = x AND y)
-//! - Source: CircuitSAT with 2 inputs
+//! - Instance: 1-bit full adder circuit (a, b, cin -> sum, cout)
+//!   - sum = a XOR b XOR cin (via intermediate t = a XOR b)
+//!   - cout = (a AND b) OR (cin AND t)
+//!   - 5 gates (2 XOR, 2 AND, 1 OR), ~8 variables
+//! - Source: CircuitSAT with 3 inputs
 //! - Target: SpinGlass
 //!
 //! ## Output
@@ -19,18 +22,40 @@ use problemreductions::prelude::*;
 use problemreductions::topology::{Graph, SimpleGraph};
 
 fn main() {
-    // 1. Create CircuitSAT instance: c = x AND y
-    //    This is a simple circuit with one AND gate.
+    // 1. Create CircuitSAT instance: 1-bit full adder
+    //    sum = a XOR b XOR cin, cout = (a AND b) OR (cin AND (a XOR b))
+    //    Decomposed into 5 gates with intermediate variables t, ab, cin_t.
     let circuit = Circuit::new(vec![
+        // Intermediate: t = a XOR b
         Assignment::new(
-            vec!["c".to_string()],
-            BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
+            vec!["t".to_string()],
+            BooleanExpr::xor(vec![BooleanExpr::var("a"), BooleanExpr::var("b")]),
+        ),
+        // sum = t XOR cin
+        Assignment::new(
+            vec!["sum".to_string()],
+            BooleanExpr::xor(vec![BooleanExpr::var("t"), BooleanExpr::var("cin")]),
+        ),
+        // ab = a AND b
+        Assignment::new(
+            vec!["ab".to_string()],
+            BooleanExpr::and(vec![BooleanExpr::var("a"), BooleanExpr::var("b")]),
+        ),
+        // cin_t = cin AND t
+        Assignment::new(
+            vec!["cin_t".to_string()],
+            BooleanExpr::and(vec![BooleanExpr::var("cin"), BooleanExpr::var("t")]),
+        ),
+        // cout = ab OR cin_t
+        Assignment::new(
+            vec!["cout".to_string()],
+            BooleanExpr::or(vec![BooleanExpr::var("ab"), BooleanExpr::var("cin_t")]),
         ),
     ]);
     let circuit_sat = CircuitSAT::<i32>::new(circuit);
 
     println!("=== Circuit-SAT to Spin Glass Reduction ===\n");
-    println!("Source circuit: c = x AND y");
+    println!("Source circuit: 1-bit full adder (a, b, cin -> sum, cout)");
     println!(
         "  {} variables: {:?}",
         circuit_sat.num_variables(),
@@ -51,9 +76,9 @@ fn main() {
         sg.num_spins(),
         sg.graph().num_edges()
     );
-    println!("  Each logic gate becomes a spin glass gadget.");
-    println!("  AND gadget: 3 spins with J=[1,-2,-2], h=[-1,-1,2]");
-    println!("  Ground states encode valid truth table entries.");
+    println!("  Each logic gate (AND, OR, XOR) becomes a spin glass gadget.");
+    println!("  Gadget ground states encode valid truth table entries.");
+    println!("  Full adder uses 5 gadgets for its 5 gate decomposition.");
 
     // 3. Solve the target SpinGlass problem
     let solver = BruteForce::new();

examples/reduction_factoring_to_circuitsat.rs

@@ -5,12 +5,12 @@
 //! iff N can be factored within the given bit bounds.
 //!
 //! ## This Example
-//! - Instance: Factor 6 = 2 * 3 (m=2 bits, n=2 bits)
+//! - Instance: Factor 35 = 5 × 7 (m=3 bits, n=3 bits)
 //! - Reference: Based on ProblemReductions.jl factoring example
-//! - Source: Factoring(2, 2, 6)
+//! - Source: Factoring(3, 3, 35)
 //! - Target: CircuitSAT
 //!
-//! We solve the source Factoring problem directly with BruteForce (only 4 binary
+//! We solve the source Factoring problem directly with BruteForce (only 6 binary
 //! variables), then verify the reduction produces a valid CircuitSAT encoding by
 //! simulating the circuit forward from a known factorization to build a complete
 //! satisfying assignment.
@@ -40,9 +40,9 @@ fn simulate_circuit(
 }
 
 fn main() {
-    // 1. Create Factoring instance: factor 6 with 2-bit factors
-    //    Possible: 2*3=6 or 3*2=6
-    let factoring = Factoring::new(2, 2, 6);
+    // 1. Create Factoring instance: factor 35 with 3-bit factors
+    //    Possible: 5*7=35 or 7*5=35
+    let factoring = Factoring::new(3, 3, 35);
 
     println!("=== Factoring to Circuit-SAT Reduction ===\n");
     println!(
@@ -58,7 +58,7 @@ fn main() {
         factoring.n()
     );
 
-    // 2. Solve the source Factoring problem directly (only 4 binary variables)
+    // 2. Solve the source Factoring problem directly (only 6 binary variables)
     let solver = BruteForce::new();
     let factoring_solutions = solver.find_best(&factoring);
     println!("\nFactoring solutions found: {}", factoring_solutions.len());
@@ -93,7 +93,7 @@ fn main() {
         a, b, a * b, factoring_sol
     );
 
-    // Set input variables: p1, p2 for first factor, q1, q2 for second factor
+    // Set input variables: p1..p3 for first factor, q1..q3 for second factor
     let mut input_values: HashMap<String, bool> = HashMap::new();
     for (i, &bit) in factoring_sol.iter().enumerate().take(factoring.m()) {
         input_values.insert(format!("p{}", i + 1), bit == 1);
@@ -161,7 +161,7 @@ fn main() {
         });
     }
 
-    println!("\nReduction verified successfully: {} = {} * {}", factoring.target(), a, b);
+    println!("\nReduction verified successfully: 35 = 5 * 7");
 
     // 6. Export JSON
     let overhead = lookup_overhead("Factoring", "CircuitSAT")

examples/reduction_factoring_to_ilp.rs

@@ -10,9 +10,9 @@
 //! Objective: feasibility (minimize 0).
 //!
 //! ## This Example
-//! - Instance: Factor 15 = 3 * 5 (m=4 bits, n=4 bits)
+//! - Instance: Factor 35 = 5 × 7 (m=3 bits, n=3 bits)
 //! - NOTE: Uses ILPSolver (not BruteForce) since the ILP has many variables
-//! - Target ILP: 4+4+16+8 = 32 variables
+//! - Target ILP: ~21 variables (factor bits + product bits + carries)
 //!
 //! ## Output
 //! Exports `docs/paper/examples/factoring_to_ilp.json` for use in paper code blocks.
@@ -22,8 +22,8 @@ use problemreductions::prelude::*;
 use problemreductions::solvers::ILPSolver;
 
 fn main() {
-    // 1. Create Factoring instance: find p (4-bit) x q (4-bit) = 15
-    let problem = Factoring::new(4, 4, 15);
+    // 1. Create Factoring instance: find p (3-bit) x q (3-bit) = 35
+    let problem = Factoring::new(3, 3, 35);
 
     // 2. Reduce to ILP
     let reduction = ReduceTo::<ILP>::reduce_to(&problem);
@@ -36,18 +36,18 @@ fn main() {
 
     // 4. Solve ILP using ILPSolver (too many variables for BruteForce)
     let solver = ILPSolver::new();
-    let ilp_solution = solver.solve(ilp).expect("ILP should be feasible for 15 = 3 * 5");
+    let ilp_solution = solver.solve(ilp).expect("ILP should be feasible for 35 = 5 * 7");
     println!("\n=== Solution ===");
-    println!("ILP solution found (first 8 vars): {:?}", &ilp_solution[..8]);
+    println!("ILP solution found (first 6 vars): {:?}", &ilp_solution[..6]);
 
     // 5. Extract factoring solution
     let extracted = reduction.extract_solution(&ilp_solution);
     println!("Source Factoring solution: {:?}", extracted);
 
-    // 6. Verify: read factors and confirm p * q = 15
+    // 6. Verify: read factors and confirm p * q = 35
     let (p, q) = problem.read_factors(&extracted);
     println!("Factors: {} x {} = {}", p, q, p * q);
-    assert_eq!(p * q, 15);
+    assert_eq!(p * q, 35);
     println!("\nReduction verified successfully");
 
     // 7. Collect solutions and export JSON

examples/reduction_ilp_to_qubo.rs

@@ -17,12 +17,14 @@
 //! solutions with better objective values.
 //!
 //! ## This Example
-//! - Instance: 3 binary projects with values [1, 2, 3]
-//!   - Constraint 1: x0 + x1 <= 1 (projects 0 and 1 share a team)
-//!   - Constraint 2: x1 + x2 <= 1 (projects 1 and 2 share equipment)
-//!   - Objective: maximize 1*x0 + 2*x1 + 3*x2
-//! - Expected: Select projects {0, 2} for total value 4 (x0 and x2 don't
-//!   share resources)
+//! - Instance: 6-variable binary knapsack problem
+//!   - Items with weights [3, 2, 5, 4, 2, 3] and values [10, 7, 12, 8, 6, 9]
+//!   - Constraint 1: 3x0 + 2x1 + 5x2 + 4x3 + 2x4 + 3x5 <= 10 (weight capacity)
+//!   - Constraint 2: x0 + x1 + x2 <= 2 (category A limit)
+//!   - Constraint 3: x3 + x4 + x5 <= 2 (category B limit)
+//!   - Objective: maximize 10x0 + 7x1 + 12x2 + 8x3 + 6x4 + 9x5
+//! - Expected: Select items that maximize total value while satisfying all
+//!   weight and category constraints
 //!
 //! ## Outputs
 //! - `docs/paper/examples/ilp_to_qubo.json` — reduction structure
@@ -39,35 +41,51 @@ use problemreductions::prelude::*;
 fn main() {
     println!("=== ILP (Binary) -> QUBO Reduction ===\n");
 
-    // 3 projects with values 1, 2, 3
-    // Constraint 1: x0 + x1 <= 1 (shared team)
-    // Constraint 2: x1 + x2 <= 1 (shared equipment)
+    // 6-variable binary knapsack problem
+    // Items with weights [3, 2, 5, 4, 2, 3] and values [10, 7, 12, 8, 6, 9]
+    // Constraint 1: knapsack weight capacity <= 10
+    // Constraint 2: category A items (x0, x1, x2) limited to 2
+    // Constraint 3: category B items (x3, x4, x5) limited to 2
     let ilp = ILP::binary(
-        3,
+        6,
         vec![
-            LinearConstraint::le(vec![(0, 1.0), (1, 1.0)], 1.0),
-            LinearConstraint::le(vec![(1, 1.0), (2, 1.0)], 1.0),
+            // Knapsack weight constraint: 3x0 + 2x1 + 5x2 + 4x3 + 2x4 + 3x5 <= 10
+            LinearConstraint::le(
+                vec![(0, 3.0), (1, 2.0), (2, 5.0), (3, 4.0), (4, 2.0), (5, 3.0)],
+                10.0,
+            ),
+            // Category A limit: x0 + x1 + x2 <= 2
+            LinearConstraint::le(vec![(0, 1.0), (1, 1.0), (2, 1.0)], 2.0),
+            // Category B limit: x3 + x4 + x5 <= 2
+            LinearConstraint::le(vec![(3, 1.0), (4, 1.0), (5, 1.0)], 2.0),
         ],
-        vec![(0, 1.0), (1, 2.0), (2, 3.0)],
+        vec![(0, 10.0), (1, 7.0), (2, 12.0), (3, 8.0), (4, 6.0), (5, 9.0)],
         ObjectiveSense::Maximize,
     );
 
-    let project_names = ["Alpha", "Beta", "Gamma"];
+    let item_names = ["Item0", "Item1", "Item2", "Item3", "Item4", "Item5"];
+    let weights = [3, 2, 5, 4, 2, 3];
+    let values = [10, 7, 12, 8, 6, 9];
 
     // Reduce to QUBO
     let reduction = ReduceTo::<QUBO>::reduce_to(&ilp);
     let qubo = reduction.target_problem();
 
-    println!("Source: ILP (binary) with 3 variables, 2 constraints");
-    println!("  Objective: maximize 1*x0 + 2*x1 + 3*x2");
-    println!("  Constraint 1: x0 + x1 <= 1 (shared team)");
-    println!("  Constraint 2: x1 + x2 <= 1 (shared equipment)");
+    println!("Source: ILP (binary) with 6 variables, 3 constraints");
+    println!("  Objective: maximize 10x0 + 7x1 + 12x2 + 8x3 + 6x4 + 9x5");
+    println!("  Constraint 1: 3x0 + 2x1 + 5x2 + 4x3 + 2x4 + 3x5 <= 10 (weight capacity)");
+    println!("  Constraint 2: x0 + x1 + x2 <= 2 (category A limit)");
+    println!("  Constraint 3: x3 + x4 + x5 <= 2 (category B limit)");
     println!("Target: QUBO with {} variables", qubo.num_variables());
-    println!("Q matrix ({}x{}):", qubo.matrix().len(), qubo.matrix().len());
-    for row in qubo.matrix() {
-        let formatted: Vec<String> = row.iter().map(|v| format!("{:7.1}", v)).collect();
-        println!("  [{}]", formatted.join(", "));
-    }
+    println!(
+        "  (6 original + {} slack variables for inequality constraints)",
+        qubo.num_variables() - 6
+    );
+    println!(
+        "Q matrix size: {}x{}",
+        qubo.matrix().len(),
+        qubo.matrix().len()
+    );
 
     // Solve QUBO with brute force
     let solver = BruteForce::new();
@@ -82,17 +100,31 @@ fn main() {
             .iter()
             .enumerate()
             .filter(|(_, &x)| x == 1)
-            .map(|(i, _)| project_names[i].to_string())
+            .map(|(i, _)| item_names[i].to_string())
             .collect();
-        let value = ilp.solution_size(&extracted).size;
+        let total_weight: i32 = extracted
+            .iter()
+            .enumerate()
+            .filter(|(_, &x)| x == 1)
+            .map(|(i, _)| weights[i])
+            .sum();
+        let total_value: i32 = extracted
+            .iter()
+            .enumerate()
+            .filter(|(_, &x)| x == 1)
+            .map(|(i, _)| values[i])
+            .sum();
         println!(
-            "  Selected projects: {:?} (total value: {:.0})",
-            selected, value
+            "  Selected items: {:?} (total weight: {}, total value: {})",
+            selected, total_weight, total_value
         );
 
         // Closed-loop verification: check solution is valid in original problem
         let sol_size = ilp.solution_size(&extracted);
-        assert!(sol_size.is_valid, "Solution must be valid in source problem");
+        assert!(
+            sol_size.is_valid,
+            "Solution must be valid in source problem"
+        );
 
         solutions.push(SolutionPair {
             source_config: extracted,
@@ -103,8 +135,7 @@ fn main() {
     println!("\nVerification passed: all solutions are feasible and optimal");
 
     // Export JSON
-    let overhead = lookup_overhead("ILP", "QUBO")
-        .expect("ILP -> QUBO overhead not found");
+    let overhead = lookup_overhead("ILP", "QUBO").expect("ILP -> QUBO overhead not found");
 
     let data = ReductionData {
         source: ProblemSide {