Skip to content

Commit 142d3c2

Browse files
GiggleLiuclaude
andauthored
docs: improve example instances implementation plan (#41)
* docs: update title for example instances improvement plan Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * feat(docs): interactive reduction diagram with Cytoscape.js (#34) Add an interactive Cytoscape.js-based reduction graph page to the mdBook documentation. The page loads reduction_graph.json, filters to base problem nodes, deduplicates edges, and renders an explorable directed graph with category-colored nodes and two-click shortest-path highlighting. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use Petersen graph for MIS reductions Replace trivial P4 path graph (4 vertices, 3 edges, MIS=2) with the Petersen graph (10 vertices, 15 edges, 3-regular, MIS=4) in all four MIS reduction examples: QUBO, ILP, MinimumVertexCover, MaximumSetPacking. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use Petersen graph for MVC reductions Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use Petersen graph for Matching and DomSet reductions Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use Petersen graph for Coloring and MaxCut reductions Replace trivial K3/triangle instances with more interesting graphs: - kcoloring_to_ilp: Petersen graph (10v, 15e) with ILPSolver - kcoloring_to_qubo: house graph (5v, 6e) to keep BruteForce feasible - maxcut_to_spinglass: Petersen graph (10v, 15e) with unit weights Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use octahedron for MaximumClique reduction Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use 6-set instances for SetPacking and SetCovering Replace trivial 3-set instances with richer 6-set instances over 8 elements in SetPacking (QUBO and ILP) and SetCovering (ILP) examples. The new instances have interesting overlap structure and produce max packing size 2 and min cover size 3. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use 5-variable SAT instances for SAT reductions Replace trivial 2-3 variable SAT formulas with richer 5-variable instances across 4 SAT reduction examples: - sat_to_mis: 5-var, 7-clause 3-SAT (21 vertices, fast BruteForce) - sat_to_coloring: 5-var, 3 unit clauses (13 vertices; OR-gadgets make multi-literal clauses infeasible for BruteForce on 3-coloring) - sat_to_mds: 5-var, 7-clause 3-SAT (22 vertices, fast BruteForce) - sat_to_ksat: 5-var, 6-clause mixed sizes (1,2,3,3,4,5 literals) to demonstrate both padding and splitting transformations Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use 5-variable 3-SAT instance for kSAT-to-QUBO Generalize the KSatisfiability-to-QUBO reduction to support K=3 using Rosenberg quadratization (one auxiliary variable per 3-literal clause). Update the example from a trivial 2-SAT/3-variable instance to a 3-SAT instance with 5 variables and 7 clauses, producing a 12-variable QUBO (5 original + 7 auxiliary). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use Petersen topology for SpinGlass/QUBO/MaxCut Replace trivial 3-spin/3-variable instances with 10-variable Petersen graph instances for SpinGlass-QUBO and SpinGlass-MaxCut reductions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use 6-variable knapsack for ILP-to-QUBO Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use full adder circuit for CircuitSAT-to-SpinGlass Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * examples: use factoring 35=5×7 for Factoring reductions Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * fix: address review feedback - Remove interactive reduction graph page (docs/src/reductions/graph.md) - Remove Reductions section from SUMMARY.md - Rename ReductionK3SatToQUBO to Reduction3SATToQUBO - Document 3-SAT→QUBO Rosenberg quadratization in reductions.typ - Update PR description to reflect code changes Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
1 parent 0ea5572 commit 142d3c2

35 files changed

Lines changed: 854 additions & 383 deletions

docs/paper/reductions.typ

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -522,9 +522,9 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
522522
]
523523

524524
#reduction-rule("KSatisfiability", "QUBO")[
525-
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.
525+
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))$.
526526
][
527-
_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$:
527+
*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$:
528528

529529
#table(
530530
columns: (auto, auto, auto, auto),
@@ -538,6 +538,12 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
538538
)
539539

540540
Summing over all clauses, $f(bold(x)) = sum_j "penalty"_j (bold(x))$ counts falsified clauses. Minimizers of $f$ maximize satisfied clauses.
541+
542+
*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$:
543+
$ H = a dot y_3 + M (y_1 y_2 - 2 y_1 a - 2 y_2 a + 3a) $
544+
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.
545+
546+
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]$.
541547
]
542548

543549
#reduction-rule("ILP", "QUBO")[

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
# Improve Example Instances — Implementation Plan
1+
# Improve Example Instances — Implementation Plan (v2)
22

33
> **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task.
44

examples/reduction_circuitsat_to_spinglass.rs

Lines changed: 35 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,11 @@
66
//! of gadget Hamiltonians; ground states correspond to satisfying assignments.
77
//!
88
//! ## This Example
9-
//! - Instance: Simple AND gate circuit (c = x AND y)
10-
//! - Source: CircuitSAT with 2 inputs
9+
//! - Instance: 1-bit full adder circuit (a, b, cin -> sum, cout)
10+
//! - sum = a XOR b XOR cin (via intermediate t = a XOR b)
11+
//! - cout = (a AND b) OR (cin AND t)
12+
//! - 5 gates (2 XOR, 2 AND, 1 OR), ~8 variables
13+
//! - Source: CircuitSAT with 3 inputs
1114
//! - Target: SpinGlass
1215
//!
1316
//! ## Output
@@ -19,18 +22,40 @@ use problemreductions::prelude::*;
1922
use problemreductions::topology::{Graph, SimpleGraph};
2023

2124
fn main() {
22-
// 1. Create CircuitSAT instance: c = x AND y
23-
// This is a simple circuit with one AND gate.
25+
// 1. Create CircuitSAT instance: 1-bit full adder
26+
// sum = a XOR b XOR cin, cout = (a AND b) OR (cin AND (a XOR b))
27+
// Decomposed into 5 gates with intermediate variables t, ab, cin_t.
2428
let circuit = Circuit::new(vec![
29+
// Intermediate: t = a XOR b
2530
Assignment::new(
26-
vec!["c".to_string()],
27-
BooleanExpr::and(vec![BooleanExpr::var("x"), BooleanExpr::var("y")]),
31+
vec!["t".to_string()],
32+
BooleanExpr::xor(vec![BooleanExpr::var("a"), BooleanExpr::var("b")]),
33+
),
34+
// sum = t XOR cin
35+
Assignment::new(
36+
vec!["sum".to_string()],
37+
BooleanExpr::xor(vec![BooleanExpr::var("t"), BooleanExpr::var("cin")]),
38+
),
39+
// ab = a AND b
40+
Assignment::new(
41+
vec!["ab".to_string()],
42+
BooleanExpr::and(vec![BooleanExpr::var("a"), BooleanExpr::var("b")]),
43+
),
44+
// cin_t = cin AND t
45+
Assignment::new(
46+
vec!["cin_t".to_string()],
47+
BooleanExpr::and(vec![BooleanExpr::var("cin"), BooleanExpr::var("t")]),
48+
),
49+
// cout = ab OR cin_t
50+
Assignment::new(
51+
vec!["cout".to_string()],
52+
BooleanExpr::or(vec![BooleanExpr::var("ab"), BooleanExpr::var("cin_t")]),
2853
),
2954
]);
3055
let circuit_sat = CircuitSAT::<i32>::new(circuit);
3156

3257
println!("=== Circuit-SAT to Spin Glass Reduction ===\n");
33-
println!("Source circuit: c = x AND y");
58+
println!("Source circuit: 1-bit full adder (a, b, cin -> sum, cout)");
3459
println!(
3560
" {} variables: {:?}",
3661
circuit_sat.num_variables(),
@@ -51,9 +76,9 @@ fn main() {
5176
sg.num_spins(),
5277
sg.graph().num_edges()
5378
);
54-
println!(" Each logic gate becomes a spin glass gadget.");
55-
println!(" AND gadget: 3 spins with J=[1,-2,-2], h=[-1,-1,2]");
56-
println!(" Ground states encode valid truth table entries.");
79+
println!(" Each logic gate (AND, OR, XOR) becomes a spin glass gadget.");
80+
println!(" Gadget ground states encode valid truth table entries.");
81+
println!(" Full adder uses 5 gadgets for its 5 gate decomposition.");
5782

5883
// 3. Solve the target SpinGlass problem
5984
let solver = BruteForce::new();

examples/reduction_factoring_to_circuitsat.rs

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,12 @@
55
//! iff N can be factored within the given bit bounds.
66
//!
77
//! ## This Example
8-
//! - Instance: Factor 6 = 2 * 3 (m=2 bits, n=2 bits)
8+
//! - Instance: Factor 35 = 5 × 7 (m=3 bits, n=3 bits)
99
//! - Reference: Based on ProblemReductions.jl factoring example
10-
//! - Source: Factoring(2, 2, 6)
10+
//! - Source: Factoring(3, 3, 35)
1111
//! - Target: CircuitSAT
1212
//!
13-
//! We solve the source Factoring problem directly with BruteForce (only 4 binary
13+
//! We solve the source Factoring problem directly with BruteForce (only 6 binary
1414
//! variables), then verify the reduction produces a valid CircuitSAT encoding by
1515
//! simulating the circuit forward from a known factorization to build a complete
1616
//! satisfying assignment.
@@ -40,9 +40,9 @@ fn simulate_circuit(
4040
}
4141

4242
fn main() {
43-
// 1. Create Factoring instance: factor 6 with 2-bit factors
44-
// Possible: 2*3=6 or 3*2=6
45-
let factoring = Factoring::new(2, 2, 6);
43+
// 1. Create Factoring instance: factor 35 with 3-bit factors
44+
// Possible: 5*7=35 or 7*5=35
45+
let factoring = Factoring::new(3, 3, 35);
4646

4747
println!("=== Factoring to Circuit-SAT Reduction ===\n");
4848
println!(
@@ -58,7 +58,7 @@ fn main() {
5858
factoring.n()
5959
);
6060

61-
// 2. Solve the source Factoring problem directly (only 4 binary variables)
61+
// 2. Solve the source Factoring problem directly (only 6 binary variables)
6262
let solver = BruteForce::new();
6363
let factoring_solutions = solver.find_best(&factoring);
6464
println!("\nFactoring solutions found: {}", factoring_solutions.len());
@@ -93,7 +93,7 @@ fn main() {
9393
a, b, a * b, factoring_sol
9494
);
9595

96-
// Set input variables: p1, p2 for first factor, q1, q2 for second factor
96+
// Set input variables: p1..p3 for first factor, q1..q3 for second factor
9797
let mut input_values: HashMap<String, bool> = HashMap::new();
9898
for (i, &bit) in factoring_sol.iter().enumerate().take(factoring.m()) {
9999
input_values.insert(format!("p{}", i + 1), bit == 1);
@@ -161,7 +161,7 @@ fn main() {
161161
});
162162
}
163163

164-
println!("\nReduction verified successfully: {} = {} * {}", factoring.target(), a, b);
164+
println!("\nReduction verified successfully: 35 = 5 * 7");
165165

166166
// 6. Export JSON
167167
let overhead = lookup_overhead("Factoring", "CircuitSAT")

examples/reduction_factoring_to_ilp.rs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,9 @@
1010
//! Objective: feasibility (minimize 0).
1111
//!
1212
//! ## This Example
13-
//! - Instance: Factor 15 = 3 * 5 (m=4 bits, n=4 bits)
13+
//! - Instance: Factor 35 = 5 × 7 (m=3 bits, n=3 bits)
1414
//! - NOTE: Uses ILPSolver (not BruteForce) since the ILP has many variables
15-
//! - Target ILP: 4+4+16+8 = 32 variables
15+
//! - Target ILP: ~21 variables (factor bits + product bits + carries)
1616
//!
1717
//! ## Output
1818
//! Exports `docs/paper/examples/factoring_to_ilp.json` for use in paper code blocks.
@@ -22,8 +22,8 @@ use problemreductions::prelude::*;
2222
use problemreductions::solvers::ILPSolver;
2323

2424
fn main() {
25-
// 1. Create Factoring instance: find p (4-bit) x q (4-bit) = 15
26-
let problem = Factoring::new(4, 4, 15);
25+
// 1. Create Factoring instance: find p (3-bit) x q (3-bit) = 35
26+
let problem = Factoring::new(3, 3, 35);
2727

2828
// 2. Reduce to ILP
2929
let reduction = ReduceTo::<ILP>::reduce_to(&problem);
@@ -36,18 +36,18 @@ fn main() {
3636

3737
// 4. Solve ILP using ILPSolver (too many variables for BruteForce)
3838
let solver = ILPSolver::new();
39-
let ilp_solution = solver.solve(ilp).expect("ILP should be feasible for 15 = 3 * 5");
39+
let ilp_solution = solver.solve(ilp).expect("ILP should be feasible for 35 = 5 * 7");
4040
println!("\n=== Solution ===");
41-
println!("ILP solution found (first 8 vars): {:?}", &ilp_solution[..8]);
41+
println!("ILP solution found (first 6 vars): {:?}", &ilp_solution[..6]);
4242

4343
// 5. Extract factoring solution
4444
let extracted = reduction.extract_solution(&ilp_solution);
4545
println!("Source Factoring solution: {:?}", extracted);
4646

47-
// 6. Verify: read factors and confirm p * q = 15
47+
// 6. Verify: read factors and confirm p * q = 35
4848
let (p, q) = problem.read_factors(&extracted);
4949
println!("Factors: {} x {} = {}", p, q, p * q);
50-
assert_eq!(p * q, 15);
50+
assert_eq!(p * q, 35);
5151
println!("\nReduction verified successfully");
5252

5353
// 7. Collect solutions and export JSON

examples/reduction_ilp_to_qubo.rs

Lines changed: 61 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -17,12 +17,14 @@
1717
//! solutions with better objective values.
1818
//!
1919
//! ## This Example
20-
//! - Instance: 3 binary projects with values [1, 2, 3]
21-
//! - Constraint 1: x0 + x1 <= 1 (projects 0 and 1 share a team)
22-
//! - Constraint 2: x1 + x2 <= 1 (projects 1 and 2 share equipment)
23-
//! - Objective: maximize 1*x0 + 2*x1 + 3*x2
24-
//! - Expected: Select projects {0, 2} for total value 4 (x0 and x2 don't
25-
//! share resources)
20+
//! - Instance: 6-variable binary knapsack problem
21+
//! - Items with weights [3, 2, 5, 4, 2, 3] and values [10, 7, 12, 8, 6, 9]
22+
//! - Constraint 1: 3x0 + 2x1 + 5x2 + 4x3 + 2x4 + 3x5 <= 10 (weight capacity)
23+
//! - Constraint 2: x0 + x1 + x2 <= 2 (category A limit)
24+
//! - Constraint 3: x3 + x4 + x5 <= 2 (category B limit)
25+
//! - Objective: maximize 10x0 + 7x1 + 12x2 + 8x3 + 6x4 + 9x5
26+
//! - Expected: Select items that maximize total value while satisfying all
27+
//! weight and category constraints
2628
//!
2729
//! ## Outputs
2830
//! - `docs/paper/examples/ilp_to_qubo.json` — reduction structure
@@ -39,35 +41,51 @@ use problemreductions::prelude::*;
3941
fn main() {
4042
println!("=== ILP (Binary) -> QUBO Reduction ===\n");
4143

42-
// 3 projects with values 1, 2, 3
43-
// Constraint 1: x0 + x1 <= 1 (shared team)
44-
// Constraint 2: x1 + x2 <= 1 (shared equipment)
44+
// 6-variable binary knapsack problem
45+
// Items with weights [3, 2, 5, 4, 2, 3] and values [10, 7, 12, 8, 6, 9]
46+
// Constraint 1: knapsack weight capacity <= 10
47+
// Constraint 2: category A items (x0, x1, x2) limited to 2
48+
// Constraint 3: category B items (x3, x4, x5) limited to 2
4549
let ilp = ILP::binary(
46-
3,
50+
6,
4751
vec![
48-
LinearConstraint::le(vec![(0, 1.0), (1, 1.0)], 1.0),
49-
LinearConstraint::le(vec![(1, 1.0), (2, 1.0)], 1.0),
52+
// Knapsack weight constraint: 3x0 + 2x1 + 5x2 + 4x3 + 2x4 + 3x5 <= 10
53+
LinearConstraint::le(
54+
vec![(0, 3.0), (1, 2.0), (2, 5.0), (3, 4.0), (4, 2.0), (5, 3.0)],
55+
10.0,
56+
),
57+
// Category A limit: x0 + x1 + x2 <= 2
58+
LinearConstraint::le(vec![(0, 1.0), (1, 1.0), (2, 1.0)], 2.0),
59+
// Category B limit: x3 + x4 + x5 <= 2
60+
LinearConstraint::le(vec![(3, 1.0), (4, 1.0), (5, 1.0)], 2.0),
5061
],
51-
vec![(0, 1.0), (1, 2.0), (2, 3.0)],
62+
vec![(0, 10.0), (1, 7.0), (2, 12.0), (3, 8.0), (4, 6.0), (5, 9.0)],
5263
ObjectiveSense::Maximize,
5364
);
5465

55-
let project_names = ["Alpha", "Beta", "Gamma"];
66+
let item_names = ["Item0", "Item1", "Item2", "Item3", "Item4", "Item5"];
67+
let weights = [3, 2, 5, 4, 2, 3];
68+
let values = [10, 7, 12, 8, 6, 9];
5669

5770
// Reduce to QUBO
5871
let reduction = ReduceTo::<QUBO>::reduce_to(&ilp);
5972
let qubo = reduction.target_problem();
6073

61-
println!("Source: ILP (binary) with 3 variables, 2 constraints");
62-
println!(" Objective: maximize 1*x0 + 2*x1 + 3*x2");
63-
println!(" Constraint 1: x0 + x1 <= 1 (shared team)");
64-
println!(" Constraint 2: x1 + x2 <= 1 (shared equipment)");
74+
println!("Source: ILP (binary) with 6 variables, 3 constraints");
75+
println!(" Objective: maximize 10x0 + 7x1 + 12x2 + 8x3 + 6x4 + 9x5");
76+
println!(" Constraint 1: 3x0 + 2x1 + 5x2 + 4x3 + 2x4 + 3x5 <= 10 (weight capacity)");
77+
println!(" Constraint 2: x0 + x1 + x2 <= 2 (category A limit)");
78+
println!(" Constraint 3: x3 + x4 + x5 <= 2 (category B limit)");
6579
println!("Target: QUBO with {} variables", qubo.num_variables());
66-
println!("Q matrix ({}x{}):", qubo.matrix().len(), qubo.matrix().len());
67-
for row in qubo.matrix() {
68-
let formatted: Vec<String> = row.iter().map(|v| format!("{:7.1}", v)).collect();
69-
println!(" [{}]", formatted.join(", "));
70-
}
80+
println!(
81+
" (6 original + {} slack variables for inequality constraints)",
82+
qubo.num_variables() - 6
83+
);
84+
println!(
85+
"Q matrix size: {}x{}",
86+
qubo.matrix().len(),
87+
qubo.matrix().len()
88+
);
7189

7290
// Solve QUBO with brute force
7391
let solver = BruteForce::new();
@@ -82,17 +100,31 @@ fn main() {
82100
.iter()
83101
.enumerate()
84102
.filter(|(_, &x)| x == 1)
85-
.map(|(i, _)| project_names[i].to_string())
103+
.map(|(i, _)| item_names[i].to_string())
86104
.collect();
87-
let value = ilp.solution_size(&extracted).size;
105+
let total_weight: i32 = extracted
106+
.iter()
107+
.enumerate()
108+
.filter(|(_, &x)| x == 1)
109+
.map(|(i, _)| weights[i])
110+
.sum();
111+
let total_value: i32 = extracted
112+
.iter()
113+
.enumerate()
114+
.filter(|(_, &x)| x == 1)
115+
.map(|(i, _)| values[i])
116+
.sum();
88117
println!(
89-
" Selected projects: {:?} (total value: {:.0})",
90-
selected, value
118+
" Selected items: {:?} (total weight: {}, total value: {})",
119+
selected, total_weight, total_value
91120
);
92121

93122
// Closed-loop verification: check solution is valid in original problem
94123
let sol_size = ilp.solution_size(&extracted);
95-
assert!(sol_size.is_valid, "Solution must be valid in source problem");
124+
assert!(
125+
sol_size.is_valid,
126+
"Solution must be valid in source problem"
127+
);
96128

97129
solutions.push(SolutionPair {
98130
source_config: extracted,
@@ -103,8 +135,7 @@ fn main() {
103135
println!("\nVerification passed: all solutions are feasible and optimal");
104136

105137
// Export JSON
106-
let overhead = lookup_overhead("ILP", "QUBO")
107-
.expect("ILP -> QUBO overhead not found");
138+
let overhead = lookup_overhead("ILP", "QUBO").expect("ILP -> QUBO overhead not found");
108139

109140
let data = ReductionData {
110141
source: ProblemSide {

0 commit comments

Comments
 (0)