Skip to content
124 changes: 67 additions & 57 deletions docs/paper/reduction_graph.json
Original file line number Diff line number Diff line change
@@ -1,8 +1,13 @@
{
"nodes": [
{
"id": "MaxCut",
"label": "MaxCut",
"id": "CircuitSAT",
"label": "CircuitSAT",
"category": "satisfiability"
},
{
"id": "Coloring",
"label": "Coloring",
"category": "graph"
},
{
Expand All @@ -11,13 +16,13 @@
"category": "graph"
},
{
"id": "SpinGlass",
"label": "SpinGlass",
"category": "optimization"
"id": "Factoring",
"label": "Factoring",
"category": "specialized"
},
{
"id": "QUBO",
"label": "QUBO",
"id": "ILP",
"label": "ILP",
"category": "optimization"
},
{
Expand All @@ -26,49 +31,49 @@
"category": "graph"
},
{
"id": "SetPacking",
"label": "SetPacking",
"category": "set"
},
{
"id": "Satisfiability",
"label": "Satisfiability",
"id": "KSatisfiability",
"label": "KSatisfiability",
"category": "satisfiability"
},
{
"id": "Coloring",
"label": "Coloring",
"id": "Matching",
"label": "Matching",
"category": "graph"
},
{
"id": "VertexCovering",
"label": "VertexCovering",
"id": "MaxCut",
"label": "MaxCut",
"category": "graph"
},
{
"id": "KSatisfiability",
"label": "KSatisfiability",
"category": "satisfiability"
"id": "QUBO",
"label": "QUBO",
"category": "optimization"
},
{
"id": "CircuitSAT",
"label": "CircuitSAT",
"id": "Satisfiability",
"label": "Satisfiability",
"category": "satisfiability"
},
{
"id": "Factoring",
"label": "Factoring",
"category": "specialized"
"id": "SetCovering",
"label": "SetCovering",
"category": "set"
},
{
"id": "Matching",
"label": "Matching",
"category": "graph"
"id": "SetPacking",
"label": "SetPacking",
"category": "set"
},
{
"id": "SetCovering",
"label": "SetCovering",
"category": "set"
"id": "SpinGlass",
"label": "SpinGlass",
"category": "optimization"
},
{
"id": "VertexCovering",
"label": "VertexCovering",
"category": "graph"
}
],
"edges": [
Expand All @@ -78,38 +83,33 @@
"bidirectional": false
},
{
"source": "Matching",
"target": "SetPacking",
"source": "Factoring",
"target": "CircuitSAT",
"bidirectional": false
},
{
"source": "Satisfiability",
"target": "KSatisfiability",
"bidirectional": true
},
{
"source": "Factoring",
"target": "CircuitSAT",
"target": "ILP",
"bidirectional": false
},
{
"source": "IndependentSet",
"target": "SetPacking",
"source": "KSatisfiability",
"target": "Satisfiability",
"bidirectional": true
},
{
"source": "SpinGlass",
"target": "QUBO",
"bidirectional": true
"source": "Matching",
"target": "SetPacking",
"bidirectional": false
},
{
"source": "MaxCut",
"target": "SpinGlass",
"bidirectional": true
"source": "Satisfiability",
"target": "Coloring",
"bidirectional": false
},
{
"source": "VertexCovering",
"target": "SetCovering",
"source": "Satisfiability",
"target": "DominatingSet",
"bidirectional": false
},
{
Expand All @@ -118,18 +118,28 @@
"bidirectional": false
},
{
"source": "Satisfiability",
"target": "Coloring",
"bidirectional": false
"source": "SetPacking",
"target": "IndependentSet",
"bidirectional": true
},
{
"source": "SpinGlass",
"target": "MaxCut",
"bidirectional": true
},
{
"source": "IndependentSet",
"target": "VertexCovering",
"source": "SpinGlass",
"target": "QUBO",
"bidirectional": true
},
{
"source": "Satisfiability",
"target": "DominatingSet",
"source": "VertexCovering",
"target": "IndependentSet",
"bidirectional": true
},
{
"source": "VertexCovering",
"target": "SetCovering",
"bidirectional": false
}
]
Expand Down
49 changes: 49 additions & 0 deletions docs/paper/reductions.typ
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@
"VertexCovering": (-0.5, 2),
"Matching": (-2, 2),
"SpinGlass": (2.5, 2),
"ILP": (3.5, 1),
// Row 3: Leaf nodes
"SetPacking": (-1.5, 3),
"SetCovering": (0.5, 3),
Expand Down Expand Up @@ -330,6 +331,53 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
_Solution extraction._ Without ancilla: identity. With ancilla: if $sigma_a = 1$, flip all spins before removing ancilla.
]

#theorem[
*(Factoring $arrow.r$ ILP)* Integer factorization reduces to binary ILP using McCormick linearization with $O(m n)$ variables and constraints.
]

#proof[
_Construction._ For target $N$ with $m$-bit factor $p$ and $n$-bit factor $q$:

_Variables:_ Binary $p_i, q_j in {0,1}$ for factor bits; binary $z_(i j) in {0,1}$ for products $p_i dot q_j$; integer $c_k >= 0$ for carries at each bit position.

_Product linearization (McCormick):_ For each $z_(i j) = p_i dot q_j$:
$ z_(i j) <= p_i, quad z_(i j) <= q_j, quad z_(i j) >= p_i + q_j - 1 $

_Bit-position equations:_ For each bit position $k$:
$ sum_(i+j=k) z_(i j) + c_(k-1) = N_k + 2 c_k $
where $N_k$ is the $k$-th bit of $N$ and $c_(-1) = 0$.

_No overflow:_ $c_(m+n-1) = 0$.

_Correctness._ The McCormick constraints enforce $z_(i j) = p_i dot q_j$ for binary variables. The bit equations encode $p times q = N$ via carry propagation, matching array multiplier semantics.

_Solution extraction._ Read $p = sum_i p_i 2^i$ and $q = sum_j q_j 2^j$ from the binary variables.
]

_Example: Factoring 15._ The following Rust code demonstrates the closed-loop reduction (requires `ilp` feature: `cargo add problemreductions --features ilp`):

```rust
use problemreductions::prelude::*;

// 1. Create factoring instance: find p (4-bit) × q (4-bit) = 15
let problem = Factoring::new(4, 4, 15);

// 2. Reduce to ILP
let reduction = ReduceTo::<ILP>::reduce_to(&problem);
let ilp = reduction.target_problem();

// 3. Solve ILP
let solver = ILPSolver::new();
let ilp_solution = solver.solve(ilp).unwrap();
Comment on lines +359 to +371
Copy link

Copilot AI Jan 31, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The example uses ILP / ILPSolver, which are behind the crate’s ilp feature. Consider noting in the paper snippet that consumers must enable the ilp feature (e.g., in Cargo.toml or via --features ilp), otherwise this example won’t compile when copied.

Copilot uses AI. Check for mistakes.

// 4. Extract factoring solution
let extracted = reduction.extract_solution(&ilp_solution);

// 5. Verify: reads factors and confirms p × q = 15
let (p, q) = problem.read_factors(&extracted);
assert_eq!(p * q, 15); // e.g., (3, 5) or (5, 3)
```

= Summary <sec:summary>

#let gray = rgb("#e8e8e8")
Expand All @@ -352,6 +400,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
[CircuitSAT $arrow.r$ SpinGlass], [$O(|"gates"|)$], [@whitfield2012 @lucas2014],
[Factoring $arrow.r$ CircuitSAT], [$O(m n)$], [Folklore],
[SpinGlass $arrow.l.r$ MaxCut], [$O(n + |J|)$], [@barahona1982 @lucas2014],
table.cell(fill: gray)[Factoring $arrow.r$ ILP], table.cell(fill: gray)[$O(m n)$], table.cell(fill: gray)[—],
),
caption: [Summary of reductions. Gray rows indicate trivial reductions.]
) <tab:summary>
Expand Down
Loading