From 83220633227f6b0f759bfb70212f00c52385de13 Mon Sep 17 00:00:00 2001
From: GiggleLiu <cacate0129@gmail.com>
Date: Tue, 17 Feb 2026 01:09:52 +0800
Subject: [PATCH 1/2] =?UTF-8?q?feat:=20rewrite=20getting-started=20with=20?=
 =?UTF-8?q?Factoring=E2=86=92SpinGlass=20example=20and=20path=20overhead?=
 =?UTF-8?q?=20API?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Rewrite getting-started.md Example 2 to Factoring→SpinGlass with notebook style
- Add path_overheads() as single source of truth for per-edge overhead lookup
- Refactor compose_path_overhead() and tests to build on path_overheads() (DRY)
- Remove evaluate_path_overhead() in favor of symbolic per-edge checks
- Add 7 rich paper examples recovered from stash (SAT→KColoring, SAT→DS, etc.)
- Fix rustdoc unresolved link to ProblemSize
- Add force-push prohibition to CLAUDE.md

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .claude/CLAUDE.md                             |   3 +
 docs/paper/reductions.typ                     |  99 ++++++++++-
 docs/src/getting-started.md                   | 160 ++++++++++++++----
 docs/src/reductions/reduction_graph.json      |  48 ++++--
 ...hained_reduction_factoring_to_spinglass.rs |  28 ++-
 src/rules/graph.rs                            | 132 +++++++--------
 src/rules/mod.rs                              |   4 +-
 src/traits.rs                                 |   2 +-
 src/unit_tests/reduction_graph.rs             |  41 ++---
 9 files changed, 366 insertions(+), 151 deletions(-)

diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index 74415bfc2..5fbed78a7 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -35,6 +35,9 @@ make release V=x.y.z  # Tag and push a new release (CI publishes to crates.io)
 make test clippy  # Must pass before PR
 ```
 
+## Git Safety
+- **NEVER force push** (`git push --force`, `git push -f`, `git push --force-with-lease`). This is an absolute rule with no exceptions. Force push can silently destroy other people's work and stashed changes.
+
 ## Architecture
 
 ### Core Modules
diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index c69117e35..39fe20b78 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -635,7 +635,18 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   _Solution extraction._ For $v_(j,i) in S$ with literal $x_k$: set $x_k = 1$; for $overline(x_k)$: set $x_k = 0$.
 ]
 
-#reduction-rule("Satisfiability", "KColoring")[
+#let sat_kc = load-example("satisfiability_to_kcoloring")
+#let sat_kc_r = load-results("satisfiability_to_kcoloring")
+#let sat_kc_sol = sat_kc_r.solutions.at(0)
+#reduction-rule("Satisfiability", "KColoring",
+  example: true,
+  example-caption: [5-variable SAT with 3 unit clauses to 3-coloring],
+  extra: [
+    SAT assignment: $(x_1, ..., x_5) = (#sat_kc_sol.source_config.map(str).join(", "))$ \
+    Construction: 3 base + $2 times #sat_kc.source.instance.num_vars$ variable gadgets + OR-gadgets $arrow.r$ #sat_kc.target.instance.num_vertices vertices, #sat_kc.target.instance.num_edges edges \
+    #sat_kc_r.solutions.len() valid 3-colorings (color symmetry of satisfying assignments) #sym.checkmark
+  ],
+)[
   @garey1979 Given CNF $phi$, construct graph $G$ such that $phi$ is satisfiable iff $G$ is 3-colorable.
 ][
   _Construction._ (1) Base triangle: TRUE, FALSE, AUX vertices with all pairs connected. (2) Variable gadget for $x_i$: vertices $"pos"_i$, $"neg"_i$ connected to each other and to AUX. (3) Clause gadget: for $(ell_1 or ... or ell_k)$, apply OR-gadgets iteratively producing output $o$, then connect $o$ to FALSE and AUX.
@@ -645,7 +656,18 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   _Solution extraction._ Set $x_i = 1$ iff $"color"("pos"_i) = "color"("TRUE")$.
 ]
 
-#reduction-rule("Satisfiability", "MinimumDominatingSet")[
+#let sat_ds = load-example("satisfiability_to_minimumdominatingset")
+#let sat_ds_r = load-results("satisfiability_to_minimumdominatingset")
+#let sat_ds_sol = sat_ds_r.solutions.at(0)
+#reduction-rule("Satisfiability", "MinimumDominatingSet",
+  example: true,
+  example-caption: [5-variable 7-clause 3-SAT to dominating set],
+  extra: [
+    SAT assignment: $(x_1, ..., x_5) = (#sat_ds_sol.source_config.map(str).join(", "))$ \
+    Vertex structure: $#sat_ds.target.instance.num_vertices = 3 times #sat_ds.source.instance.num_vars + #sat_ds.source.instance.num_clauses$ (variable triangles + clause vertices) \
+    Dominating set of size $n = #sat_ds.source.instance.num_vars$: one vertex per variable triangle #sym.checkmark
+  ],
+)[
   @garey1979 Given CNF $phi$ with $n$ variables and $m$ clauses, $phi$ is satisfiable iff the constructed graph has a dominating set of size $n$.
 ][
   _Construction._ (1) Variable triangle for $x_i$: vertices $"pos"_i = 3i$, $"neg"_i = 3i+1$, $"dum"_i = 3i+2$ forming a triangle. (2) Clause vertex $c_j = 3n+j$ connected to $"pos"_i$ if $x_i in C_j$, to $"neg"_i$ if $overline(x_i) in C_j$.
@@ -661,7 +683,18 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   _Variable mapping:_ Identity — variables and clauses unchanged. _Solution extraction:_ identity.
 ]
 
-#reduction-rule("Satisfiability", "KSatisfiability")[
+#let sat_ksat = load-example("satisfiability_to_ksatisfiability")
+#let sat_ksat_r = load-results("satisfiability_to_ksatisfiability")
+#let sat_ksat_sol = sat_ksat_r.solutions.at(0)
+#reduction-rule("Satisfiability", "KSatisfiability",
+  example: true,
+  example-caption: [Mixed-size clauses (sizes 1 to 5) to 3-SAT],
+  extra: [
+    Source: #sat_ksat.source.instance.num_vars variables, #sat_ksat.source.instance.num_clauses clauses (sizes 1, 2, 3, 3, 4, 5) \
+    Target 3-SAT: $#sat_ksat.target.instance.num_vars = #sat_ksat.source.instance.num_vars + 7$ variables, #sat_ksat.target.instance.num_clauses clauses (small padded, large split) \
+    First solution: $(x_1, ..., x_5) = (#sat_ksat_sol.source_config.map(str).join(", "))$, auxiliary vars are don't-cares #sym.checkmark
+  ],
+)[
   @cook1971 @garey1979 Any SAT formula converts to $k$-SAT ($k >= 3$) preserving satisfiability.
 ][
   _Small clauses ($|C| < k$):_ Pad $(ell_1 or ... or ell_r)$ with auxiliary $y$: $(ell_1 or ... or ell_r or y or overline(y) or ...)$ to length $k$.
@@ -672,7 +705,17 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   _Correctness._ Original clause true $arrow.l.r$ auxiliary chain can propagate truth through new clauses.
 ]
 
-#reduction-rule("CircuitSAT", "SpinGlass")[
+#let cs_sg = load-example("circuitsat_to_spinglass")
+#let cs_sg_r = load-results("circuitsat_to_spinglass")
+#reduction-rule("CircuitSAT", "SpinGlass",
+  example: true,
+  example-caption: [1-bit full adder to Ising model],
+  extra: [
+    Circuit: #cs_sg.source.instance.num_gates gates (2 XOR, 2 AND, 1 OR), #cs_sg.source.instance.num_variables variables \
+    Target: #cs_sg.target.instance.num_spins spins (each gate allocates I/O + auxiliary spins) \
+    #cs_sg_r.solutions.len() ground states ($= 2^3$ valid input combinations for the full adder) #sym.checkmark
+  ],
+)[
   @whitfield2012 @lucas2014 Each gate maps to a gadget whose ground states encode valid I/O.
 ][
   _Spin mapping:_ $sigma in {0,1} arrow.bar s = 2sigma - 1 in {-1, +1}$.
@@ -694,7 +737,26 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   caption: [Ising gadgets for logic gates. Ground states match truth tables.]
 ) <tab:gadgets>
 
-#reduction-rule("Factoring", "CircuitSAT")[
+#let fact_cs = load-example("factoring_to_circuitsat")
+#let fact_cs_r = load-results("factoring_to_circuitsat")
+#let fact-decode(config, start, count) = {
+  let pow2 = (1, 2, 4, 8, 16, 32)
+  range(count).fold(0, (acc, i) => acc + config.at(start + i) * pow2.at(i))
+}
+#let fact-nbf = fact_cs.source.instance.num_bits_first
+#let fact-nbs = fact_cs.source.instance.num_bits_second
+#reduction-rule("Factoring", "CircuitSAT",
+  example: true,
+  example-caption: [Factor $N = #fact_cs.source.instance.number$],
+  extra: [
+    Circuit: $#fact-nbf times #fact-nbs$ array multiplier with #fact_cs.target.instance.num_gates gates, #fact_cs.target.instance.num_variables variables \
+    #fact_cs_r.solutions.len() solutions: #fact_cs_r.solutions.map(sol => {
+      let p = fact-decode(sol.source_config, 0, fact-nbf)
+      let q = fact-decode(sol.source_config, fact-nbf, fact-nbs)
+      $#p times #q = #fact_cs.source.instance.number$
+    }).join(" and ") #sym.checkmark
+  ],
+)[
   An array multiplier with output constrained to $N$ is satisfiable iff $N$ factors within bit bounds. _(Folklore; no canonical reference.)_
 ][
   _Construction._ Build $m times n$ array multiplier for $p times q$:
@@ -708,13 +770,36 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   _Solution extraction._ $p = sum_i p_i 2^(i-1)$, $q = sum_j q_j 2^(j-1)$.
 ]
 
-#reduction-rule("MaxCut", "SpinGlass")[
+#let mc_sg = load-example("maxcut_to_spinglass")
+#let mc_sg_r = load-results("maxcut_to_spinglass")
+#let mc_sg_sol = mc_sg_r.solutions.at(0)
+#let mc_sg_cut = mc_sg.source.instance.edges.filter(e => mc_sg_sol.source_config.at(e.at(0)) != mc_sg_sol.source_config.at(e.at(1))).len()
+#reduction-rule("MaxCut", "SpinGlass",
+  example: true,
+  example-caption: [Petersen graph ($n = 10$, unit weights) to Ising],
+  extra: [
+    Direct 1:1 mapping: vertices $arrow.r$ spins, $J_(i j) = w_(i j) = 1$, $h_i = 0$ \
+    Partition: $S = {#mc_sg_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ vs $overline(S) = {#mc_sg_sol.source_config.enumerate().filter(((i, x)) => x == 0).map(((i, x)) => str(i)).join(", ")}$ \
+    Cut value $= #mc_sg_cut$ ($#mc_sg_r.solutions.len()$-fold degenerate) #sym.checkmark
+  ],
+)[
   @barahona1982 Set $J_(i j) = w_(i j)$, $h_i = 0$. Maximizing cut equals minimizing $-sum J_(i j) s_i s_j$.
 ][
   Opposite-partition vertices satisfy $s_i s_j = -1$, contributing $-J_(i j)(-1) = J_(i j)$ to the energy. _Variable mapping:_ $J_(i j) = w_(i j)$, $h_i = 0$, spins $s_i = 2 sigma_i - 1$ where $sigma_i in {0, 1}$ is the partition label. _Solution extraction:_ partition $= {i : s_i = +1}$.
 ]
 
-#reduction-rule("SpinGlass", "MaxCut")[
+#let sg_mc = load-example("spinglass_to_maxcut")
+#let sg_mc_r = load-results("spinglass_to_maxcut")
+#let sg_mc_sol = sg_mc_r.solutions.at(0)
+#reduction-rule("SpinGlass", "MaxCut",
+  example: true,
+  example-caption: [10-spin Ising with alternating $J_(i j) in {plus.minus 1}$],
+  extra: [
+    All $h_i = 0$: no ancilla needed, direct 1:1 vertex mapping \
+    Edge weights $w_(i j) = J_(i j) in {plus.minus 1}$ (alternating couplings) \
+    Ground state ($#sg_mc_r.solutions.len()$-fold degenerate): partition $S = {#sg_mc_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ #sym.checkmark
+  ],
+)[
   @barahona1982 @lucas2014 Ground states of Ising models correspond to maximum cuts.
 ][
   _MaxCut $arrow.r$ SpinGlass:_ Set $J_(i j) = w_(i j)$, $h_i = 0$. Maximizing cut equals minimizing $-sum J_(i j) s_i s_j$ since $s_i s_j = -1$ when $s_i != s_j$.
diff --git a/docs/src/getting-started.md b/docs/src/getting-started.md
index 2307c3df3..42f4f0e70 100644
--- a/docs/src/getting-started.md
+++ b/docs/src/getting-started.md
@@ -28,66 +28,164 @@ The core workflow is: **create** a problem, **reduce** it to a target, **solve**
 
 </div>
 
-### Complete Example
+### Example 1: Direct reduction
 
-```rust
+Reduce Maximum Independent Set to Minimum Vertex Cover on a 4-vertex path
+graph, solve the target, and extract the solution back.
+
+#### Step 1 — Create the source problem
+
+A path graph `0–1–2–3` has 4 vertices and 3 edges.
+
+```rust,ignore
 use problemreductions::prelude::*;
 use problemreductions::topology::SimpleGraph;
 
-// 1. Create: Independent Set on a path graph (4 vertices)
-let problem = MaximumIndependentSet::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]), vec![1i32; 4]);
+let problem = MaximumIndependentSet::new(
+    SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]),
+    vec![1i32; 4],
+);
+```
+
+#### Step 2 — Reduce to Minimum Vertex Cover
+
+`ReduceTo` applies a single-step reduction. The result holds the target
+problem and knows how to map solutions back.
 
-// 2. Reduce: Transform to Minimum Vertex Cover
+```rust,ignore
+println!("Source: {} {:?}", MaximumIndependentSet::<SimpleGraph, i32>::NAME,
+    MaximumIndependentSet::<SimpleGraph, i32>::variant());
 let reduction = ReduceTo::<MinimumVertexCover<SimpleGraph, i32>>::reduce_to(&problem);
 let target = reduction.target_problem();
+println!("Target: {} {:?}, {} variables",
+    MinimumVertexCover::<SimpleGraph, i32>::NAME,
+    MinimumVertexCover::<SimpleGraph, i32>::variant(),
+    target.num_variables());
+```
+
+```text
+Source: MaximumIndependentSet [("graph", "SimpleGraph"), ("weight", "i32")]
+Target: MinimumVertexCover [("graph", "SimpleGraph"), ("weight", "i32")], 4 variables
+```
+
+#### Step 3 — Solve the target problem
+
+`BruteForce` enumerates all configurations and returns the optimal one.
 
-// 3. Solve: Find optimal solution to the target problem
+```rust,ignore
 let solver = BruteForce::new();
 let target_solution = solver.find_best(target).unwrap();
+println!("VC solution: {:?}", target_solution);
+```
 
-// 4. Extract: Map solution back to original problem
-let solution = reduction.extract_solution(&target_solution);
+```text
+VC solution: [1, 0, 1, 0]
+```
+
+#### Step 4 — Extract and verify
+
+`extract_solution` maps the Vertex Cover solution back to an Independent Set
+solution by complementing the configuration.
 
-// Verify: solution is valid for the original problem
+```rust,ignore
+let solution = reduction.extract_solution(&target_solution);
 let metric = problem.evaluate(&solution);
+println!("IS solution: {:?} -> size {:?}", solution, metric);
 assert!(metric.is_valid());
 ```
 
-### Chaining Reductions
+```text
+IS solution: [0, 1, 0, 1] -> size Valid(2)
+```
+
+S ⊆ V is an independent set iff V \ S is a vertex cover, so the complement
+maps optimality in one direction to optimality in the other.
+
+### Example 2: Reduction path search — integer factoring to spin glass
+
+Real-world problems often require **chaining** multiple reductions. Here we factor the integer 6 by reducing `Factoring` through the reduction graph to `SpinGlass`, through automatic reduction path search.
+
+```rust,ignore
+{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:imports}}
+
+{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:example}}
+```
+
+Let's walk through each step.
 
-Reductions compose into multi-step chains. The `ReductionGraph` discovers
-paths through the variant-level graph. Find a `ReductionPath` first, then
-convert it to a typed `ExecutablePath<S, T>` via `make_executable()`. Call
-`reduce()` once and get a `ChainedReduction` with `target_problem()` and
-`extract_solution()`, just like a single-step reduction.
+#### Step 1 — Discover the reduction path
 
-Here we solve a 3-SAT formula by chaining through Satisfiability
-and MaximumIndependentSet:
+`ReductionGraph` holds every registered reduction. `find_cheapest_path`
+searches for the shortest chain from a source problem variant to a target
+variant.
 
 ```rust,ignore
-{{#include ../../examples/chained_reduction_ksat_to_mis.rs:imports}}
+{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:step1}}
+```
 
-{{#include ../../examples/chained_reduction_ksat_to_mis.rs:example}}
+```text
+  Factoring → CircuitSAT → SpinGlass {graph: "SimpleGraph", weight: "i32"}
+```
+
+#### Step 2 — Create the Factoring problem
+
+`Factoring::new(m, n, target)` creates a factoring instance: find two factors
+`p` (m-bit) and `q` (n-bit) such that `p × q = target`. Here we factor **6**
+with two 2-bit factors, expecting **2 × 3** or **3 × 2**.
 
-{{#include ../../examples/chained_reduction_ksat_to_mis.rs:overhead}}
+```rust,ignore
+{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:step2}}
 ```
 
-The `ExecutablePath` handles variant casts (e.g., `K3` → `KN`) and
-cross-problem reductions (e.g., SAT → MIS) uniformly. The `ChainedReduction`
-extracts solutions back through the entire chain in one call.
+#### Step 3 — Solve with ILPSolver
 
-`compose_path_overhead` composes the per-step polynomial overheads into a
-symbolic formula mapping source variables to final target variables:
+`solve_reduced` reduces the problem to ILP internally and solves it in one
+call. It returns a configuration vector for the original problem — no manual
+extraction needed. For small instances you can also use `BruteForce`, but
+`ILPSolver` scales to much larger problems.
+
+```rust,ignore
+{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:step3}}
+```
+
+#### Step 4 — Read and verify the factors
+
+`read_factors` decodes the binary configuration back into the two integer
+factors.
+
+```rust,ignore
+{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:step4}}
+```
 
 ```text
-  num_vertices = num_literals
-  num_edges = num_literals^2
+6 = 3 × 2
 ```
 
-This result comes from composing two steps: KSatisfiability → Satisfiability
-is identity (same size fields), then Satisfiability → MIS maps
-`num_vertices = num_literals` and `num_edges = num_literals²`.
-Substituting the identity through gives the final polynomials above.
+#### Step 5 — Inspect the overhead
+
+Each reduction edge carries a polynomial overhead mapping source problem
+sizes to target sizes. `path_overheads` returns the per-edge
+polynomials, and `compose_path_overhead` composes them symbolically into a
+single end-to-end formula.
+
+```rust,ignore
+{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:overhead}}
+```
+
+```text
+Factoring → CircuitSAT:
+  num_variables = num_bits_first * num_bits_second
+  num_assignments = num_bits_first * num_bits_second
+CircuitSAT → SpinGlass {graph: "SimpleGraph", weight: "i32"}:
+  num_spins = num_assignments
+  num_interactions = num_assignments
+SpinGlass {graph: "SimpleGraph", weight: "i32"} → SpinGlass {graph: "SimpleGraph", weight: "f64"}:
+  num_spins = num_spins
+  num_interactions = num_interactions
+Composed (source → target):
+  num_spins = num_bits_first * num_bits_second
+  num_interactions = num_bits_first * num_bits_second
+```
 
 ## Solvers
 
diff --git a/docs/src/reductions/reduction_graph.json b/docs/src/reductions/reduction_graph.json
index 01d93b988..7f6e9f683 100644
--- a/docs/src/reductions/reduction_graph.json
+++ b/docs/src/reductions/reduction_graph.json
@@ -228,7 +228,11 @@
       "target": 0,
       "overhead": [
         {
-          "field": "num_gates",
+          "field": "num_variables",
+          "formula": "num_bits_first * num_bits_second"
+        },
+        {
+          "field": "num_assignments",
           "formula": "num_bits_first * num_bits_second"
         }
       ],
@@ -269,8 +273,8 @@
           "formula": "num_vertices"
         },
         {
-          "field": "num_colors",
-          "formula": "num_colors"
+          "field": "num_edges",
+          "formula": "num_edges"
         }
       ],
       "doc_path": "rules/kcoloring_casts/index.html"
@@ -281,11 +285,11 @@
       "overhead": [
         {
           "field": "num_vars",
-          "formula": "num_vertices * num_colors"
+          "formula": "num_vertices^2"
         },
         {
           "field": "num_constraints",
-          "formula": "num_vertices + num_edges * num_colors"
+          "formula": "num_vertices + num_vertices * num_edges"
         }
       ],
       "doc_path": "rules/coloring_ilp/index.html"
@@ -296,7 +300,7 @@
       "overhead": [
         {
           "field": "num_vars",
-          "formula": "num_vertices * num_colors"
+          "formula": "num_vertices^2"
         }
       ],
       "doc_path": "rules/coloring_qubo/index.html"
@@ -338,6 +342,10 @@
         {
           "field": "num_vars",
           "formula": "num_vars"
+        },
+        {
+          "field": "num_literals",
+          "formula": "num_literals"
         }
       ],
       "doc_path": "rules/sat_ksat/index.html"
@@ -379,6 +387,10 @@
         {
           "field": "num_vars",
           "formula": "num_vars"
+        },
+        {
+          "field": "num_literals",
+          "formula": "num_literals"
         }
       ],
       "doc_path": "rules/sat_ksat/index.html"
@@ -394,6 +406,10 @@
         {
           "field": "num_vars",
           "formula": "num_vars"
+        },
+        {
+          "field": "num_literals",
+          "formula": "num_literals"
         }
       ],
       "doc_path": "rules/sat_ksat/index.html"
@@ -497,7 +513,7 @@
           "formula": "num_vertices"
         },
         {
-          "field": "num_elements",
+          "field": "universe_size",
           "formula": "num_vertices"
         }
       ],
@@ -598,7 +614,7 @@
           "formula": "num_edges"
         },
         {
-          "field": "num_elements",
+          "field": "universe_size",
           "formula": "num_vertices"
         }
       ],
@@ -654,8 +670,8 @@
           "formula": "num_sets"
         },
         {
-          "field": "num_elements",
-          "formula": "num_elements"
+          "field": "universe_size",
+          "formula": "universe_size"
         }
       ],
       "doc_path": "rules/maximumsetpacking_casts/index.html"
@@ -729,7 +745,7 @@
           "formula": "num_vertices"
         },
         {
-          "field": "num_elements",
+          "field": "universe_size",
           "formula": "num_edges"
         }
       ],
@@ -763,7 +779,11 @@
       "overhead": [
         {
           "field": "num_variables",
-          "formula": "num_variables + num_clauses + 1"
+          "formula": "num_vars + num_clauses + 1"
+        },
+        {
+          "field": "num_assignments",
+          "formula": "num_clauses + 2"
         }
       ],
       "doc_path": "rules/sat_circuitsat/index.html"
@@ -777,8 +797,8 @@
           "formula": "2 * num_vars + 5 * num_literals - 5 * num_clauses + 3"
         },
         {
-          "field": "num_colors",
-          "formula": "3"
+          "field": "num_edges",
+          "formula": "3 * num_vars + 11 * num_literals - 9 * num_clauses + 3"
         }
       ],
       "doc_path": "rules/sat_coloring/index.html"
diff --git a/examples/chained_reduction_factoring_to_spinglass.rs b/examples/chained_reduction_factoring_to_spinglass.rs
index a22b7bd73..dadb6a2f2 100644
--- a/examples/chained_reduction_factoring_to_spinglass.rs
+++ b/examples/chained_reduction_factoring_to_spinglass.rs
@@ -14,6 +14,7 @@ use problemreductions::types::ProblemSize;
 
 pub fn run() {
     // ANCHOR: example
+    // ANCHOR: step1
     let graph = ReductionGraph::new();
 
     // Find reduction path: Factoring -> ... -> SpinGlass
@@ -29,19 +30,44 @@ pub fn run() {
             &MinimizeSteps,
         )
         .unwrap();
-    println!("Reduction path: {:?}", rpath.type_names());
+    println!("  {}", rpath);
+    // ANCHOR_END: step1
 
+    // ANCHOR: step2
     // Create: factor 6 = p × q with 2-bit factors (mirrors Julia's Factoring(2, 2, 6))
     let factoring = Factoring::new(2, 2, 6);
+    // ANCHOR_END: step2
 
+    // ANCHOR: step3
     // Solve Factoring via ILP
     let solver = ILPSolver::new();
     let solution = solver.solve_reduced(&factoring).unwrap();
+    // ANCHOR_END: step3
 
+    // ANCHOR: step4
     // Extract and display the factors
     let (p, q) = factoring.read_factors(&solution);
     println!("{} = {} × {}", factoring.target(), p, q);
     assert_eq!(p * q, 6, "Factors should multiply to 6");
+    // ANCHOR_END: step4
+
+    // ANCHOR: overhead
+    // Print per-edge overhead polynomials
+    let edge_overheads = graph.path_overheads(&rpath);
+    for (i, overhead) in edge_overheads.iter().enumerate() {
+        println!("{} → {}:", rpath.steps[i], rpath.steps[i + 1]);
+        for (field, poly) in &overhead.output_size {
+            println!("  {} = {}", field, poly);
+        }
+    }
+
+    // Compose overheads symbolically along the full path
+    let composed = graph.compose_path_overhead(&rpath);
+    println!("Composed (source → target):");
+    for (field, poly) in &composed.output_size {
+        println!("  {} = {}", field, poly);
+    }
+    // ANCHOR_END: overhead
     // ANCHOR_END: example
 }
 
diff --git a/src/rules/graph.rs b/src/rules/graph.rs
index be67eee8d..eeec09934 100644
--- a/src/rules/graph.rs
+++ b/src/rules/graph.rs
@@ -137,6 +137,23 @@ impl ReductionPath {
     }
 }
 
+impl std::fmt::Display for ReductionPath {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let mut prev_name = "";
+        for step in &self.steps {
+            if step.name != prev_name {
+                if prev_name.is_empty() {
+                    write!(f, "{step}")?;
+                } else {
+                    write!(f, " → {step}")?;
+                }
+                prev_name = &step.name;
+            }
+        }
+        Ok(())
+    }
+}
+
 /// A node in a variant-level reduction path.
 #[derive(Debug, Clone, Serialize)]
 pub struct ReductionStep {
@@ -146,6 +163,21 @@ pub struct ReductionStep {
     pub variant: BTreeMap<String, String>,
 }
 
+impl std::fmt::Display for ReductionStep {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}", self.name)?;
+        if !self.variant.is_empty() {
+            let vars: Vec<_> = self
+                .variant
+                .iter()
+                .map(|(k, v)| format!("{k}: {v:?}"))
+                .collect();
+            write!(f, " {{{}}}", vars.join(", "))?;
+        }
+        Ok(())
+    }
+}
+
 /// Classify a problem's category from its module path.
 /// Expected format: "problemreductions::models::<category>::<module_name>"
 pub(crate) fn classify_problem_category(module_path: &str) -> &str {
@@ -540,15 +572,14 @@ impl ReductionGraph {
         self.nodes.len()
     }
 
-    /// Compose overheads along a path symbolically.
+    /// Get the per-edge overhead polynomials along a reduction path.
     ///
-    /// Returns a single `ReductionOverhead` whose polynomials map from the
-    /// source problem's size variables directly to the final target's size variables.
+    /// Returns one `ReductionOverhead` per edge (i.e., `path.steps.len() - 1` items).
     ///
     /// Panics if any step in the path does not correspond to an edge in the graph.
-    pub fn compose_path_overhead(&self, path: &ReductionPath) -> ReductionOverhead {
+    pub fn path_overheads(&self, path: &ReductionPath) -> Vec<ReductionOverhead> {
         if path.steps.len() <= 1 {
-            return ReductionOverhead::default();
+            return vec![];
         }
 
         let node_indices: Vec<NodeIndex> = path
@@ -560,75 +591,36 @@ impl ReductionGraph {
             })
             .collect();
 
-        let mut composed: Option<ReductionOverhead> = None;
-        for pair in node_indices.windows(2) {
-            let edge_idx = self
-                .graph
-                .find_edge(pair[0], pair[1])
-                .unwrap_or_else(|| {
-                    let src = &self.nodes[self.graph[pair[0]]];
-                    let dst = &self.nodes[self.graph[pair[1]]];
-                    panic!(
-                        "No edge from {} {:?} to {} {:?}",
-                        src.name, src.variant, dst.name, dst.variant
-                    )
-                });
-            let edge_overhead = &self.graph[edge_idx].overhead;
-            composed = Some(match composed {
-                None => edge_overhead.clone(),
-                Some(prev) => prev.compose(edge_overhead),
-            });
-        }
-
-        composed.unwrap_or_default()
+        node_indices
+            .windows(2)
+            .map(|pair| {
+                let edge_idx = self
+                    .graph
+                    .find_edge(pair[0], pair[1])
+                    .unwrap_or_else(|| {
+                        let src = &self.nodes[self.graph[pair[0]]];
+                        let dst = &self.nodes[self.graph[pair[1]]];
+                        panic!(
+                            "No edge from {} {:?} to {} {:?}",
+                            src.name, src.variant, dst.name, dst.variant
+                        )
+                    });
+                self.graph[edge_idx].overhead.clone()
+            })
+            .collect()
     }
 
-    /// Evaluate the cumulative overhead along a reduction path.
-    ///
-    /// Starting from `input_size`, chains each edge's overhead to compute
-    /// intermediate and final problem sizes. Returns the sizes at each step
-    /// (including the initial input size), so the length is `path.steps.len()`.
+    /// Compose overheads along a path symbolically.
     ///
-    /// Panics if any step in the path does not correspond to an edge in the graph.
-    pub fn evaluate_path_overhead(
-        &self,
-        path: &ReductionPath,
-        input_size: &ProblemSize,
-    ) -> Vec<ProblemSize> {
-        let mut sizes = vec![input_size.clone()];
-        if path.steps.len() <= 1 {
-            return sizes;
-        }
-
-        let node_indices: Vec<NodeIndex> = path
-            .steps
-            .iter()
-            .map(|step| {
-                self.lookup_node(&step.name, &step.variant)
-                    .unwrap_or_else(|| panic!("Node not found: {} {:?}", step.name, step.variant))
-            })
-            .collect();
-
-        let mut current_size = input_size.clone();
-        for pair in node_indices.windows(2) {
-            let edge_idx = self
-                .graph
-                .find_edge(pair[0], pair[1])
-                .unwrap_or_else(|| {
-                    let src = &self.nodes[self.graph[pair[0]]];
-                    let dst = &self.nodes[self.graph[pair[1]]];
-                    panic!(
-                        "No edge from {} {:?} to {} {:?}",
-                        src.name, src.variant, dst.name, dst.variant
-                    )
-                });
-            let overhead = &self.graph[edge_idx].overhead;
-            current_size = overhead.evaluate_output_size(&current_size);
-            sizes.push(current_size.clone());
-        }
-
-        sizes
+    /// Returns a single `ReductionOverhead` whose polynomials map from the
+    /// source problem's size variables directly to the final target's size variables.
+    pub fn compose_path_overhead(&self, path: &ReductionPath) -> ReductionOverhead {
+        self.path_overheads(path)
+            .into_iter()
+            .reduce(|acc, oh| acc.compose(&oh))
+            .unwrap_or_default()
     }
+
 }
 
 impl Default for ReductionGraph {
diff --git a/src/rules/mod.rs b/src/rules/mod.rs
index 785ba9049..b3919e8bb 100644
--- a/src/rules/mod.rs
+++ b/src/rules/mod.rs
@@ -65,8 +65,8 @@ pub use circuit_spinglass::{
 pub use coloring_qubo::ReductionKColoringToQUBO;
 pub use factoring_circuit::ReductionFactoringToCircuit;
 pub use graph::{
-    ChainedReduction, EdgeJson, ExecutablePath, NodeJson, ReductionGraph, ReductionGraphJson,
-    ReductionPath, ReductionStep,
+    ChainedReduction, EdgeJson, ExecutablePath, NodeJson, ReductionGraph,
+    ReductionGraphJson, ReductionPath, ReductionStep,
 };
 #[cfg(test)]
 pub(crate) use graph::validate_overhead_variables;
diff --git a/src/traits.rs b/src/traits.rs
index 3f25924a8..cba13e442 100644
--- a/src/traits.rs
+++ b/src/traits.rs
@@ -31,7 +31,7 @@ pub trait Problem: Clone {
     fn problem_size_values(&self) -> Vec<usize>;
 }
 
-/// Combine type-level names and instance-level values into a [`ProblemSize`].
+/// Combine type-level names and instance-level values into a [`crate::types::ProblemSize`].
 pub fn problem_size<P: Problem>(p: &P) -> crate::types::ProblemSize {
     crate::types::ProblemSize::from_names_values(P::problem_size_names(), &p.problem_size_values())
 }
diff --git a/src/unit_tests/reduction_graph.rs b/src/unit_tests/reduction_graph.rs
index 2bc78855a..fb589bc57 100644
--- a/src/unit_tests/reduction_graph.rs
+++ b/src/unit_tests/reduction_graph.rs
@@ -290,31 +290,22 @@ fn test_3sat_to_mis_triangular_overhead() {
     );
     assert_eq!(path.len(), 3);
 
-    // Evaluate overhead at each step
-    let sizes = graph.evaluate_path_overhead(&path, &input_size);
-    assert_eq!(sizes.len(), 4); // initial + 3 steps
-
-    // Step 0: K3SAT input (V=3, C=2, L=6)
-    assert_eq!(sizes[0].get("num_vars"), Some(3));
-    assert_eq!(sizes[0].get("num_clauses"), Some(2));
-    assert_eq!(sizes[0].get("num_literals"), Some(6));
-
-    // Step 1: K3SAT → SAT (identity: V=3, C=2, L=6)
-    assert_eq!(sizes[1].get("num_vars"), Some(3));
-    assert_eq!(sizes[1].get("num_clauses"), Some(2));
-    assert_eq!(sizes[1].get("num_literals"), Some(6));
-
-    // Step 2: SAT → MIS{SimpleGraph,i32}
-    //   num_vertices = num_literals = 6
-    //   num_edges = num_literals² = 36
-    assert_eq!(sizes[2].get("num_vertices"), Some(6));
-    assert_eq!(sizes[2].get("num_edges"), Some(36));
-
-    // Step 3: MIS{SimpleGraph,i32} → MIS{TriangularSubgraph,i32}
-    //   num_vertices = num_vertices² = 36
-    //   num_edges = num_vertices² = 36
-    assert_eq!(sizes[3].get("num_vertices"), Some(36));
-    assert_eq!(sizes[3].get("num_edges"), Some(36));
+    // Per-edge symbolic overheads
+    let edges = graph.path_overheads(&path);
+    assert_eq!(edges.len(), 3);
+
+    // Edge 0: K3SAT → SAT (identity)
+    assert_eq!(edges[0].get("num_vars").unwrap().normalized(), poly!(num_vars));
+    assert_eq!(edges[0].get("num_clauses").unwrap().normalized(), poly!(num_clauses));
+    assert_eq!(edges[0].get("num_literals").unwrap().normalized(), poly!(num_literals));
+
+    // Edge 1: SAT → MIS{SimpleGraph,i32}
+    assert_eq!(edges[1].get("num_vertices").unwrap().normalized(), poly!(num_literals));
+    assert_eq!(edges[1].get("num_edges").unwrap().normalized(), poly!(num_literals ^ 2));
+
+    // Edge 2: MIS{SimpleGraph,i32} → MIS{TriangularSubgraph,i32}
+    assert_eq!(edges[2].get("num_vertices").unwrap().normalized(), poly!(num_vertices ^ 2));
+    assert_eq!(edges[2].get("num_edges").unwrap().normalized(), poly!(num_vertices ^ 2));
 
     // Compose overheads symbolically along the path.
     // The composed overhead maps 3-SAT input variables to final MIS{Triangular} output.

From c96d22da8abe32b2d0f1e8346e17866758b811a1 Mon Sep 17 00:00:00 2001
From: GiggleLiu <cacate0129@gmail.com>
Date: Tue, 17 Feb 2026 01:28:42 +0800
Subject: [PATCH 2/2] test: add coverage for ReductionPath and ReductionStep
 Display impls

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/unit_tests/reduction_graph.rs | 35 +++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/src/unit_tests/reduction_graph.rs b/src/unit_tests/reduction_graph.rs
index fb589bc57..df8ed6c9c 100644
--- a/src/unit_tests/reduction_graph.rs
+++ b/src/unit_tests/reduction_graph.rs
@@ -241,6 +241,41 @@ fn test_bidirectional_paths() {
         .is_empty());
 }
 
+// ---- Display ----
+
+#[test]
+fn test_reduction_path_display() {
+    let graph = ReductionGraph::new();
+    let src_var = ReductionGraph::variant_to_map(&Factoring::variant());
+    let dst_var = ReductionGraph::variant_to_map(&SpinGlass::<SimpleGraph, f64>::variant());
+    let path = graph
+        .find_cheapest_path(
+            "Factoring",
+            &src_var,
+            "SpinGlass",
+            &dst_var,
+            &ProblemSize::new(vec![]),
+            &MinimizeSteps,
+        )
+        .unwrap();
+
+    let s = format!("{path}");
+    // Should contain arrow-separated problem names with variant info
+    assert!(s.contains("Factoring"));
+    assert!(s.contains("→"));
+    assert!(s.contains("SpinGlass"));
+
+    // Step with empty variant
+    let step = &path.steps[0];
+    assert_eq!(format!("{step}"), "Factoring");
+
+    // Step with non-empty variant
+    let last = path.steps.last().unwrap();
+    let last_s = format!("{last}");
+    assert!(last_s.contains("SpinGlass"));
+    assert!(last_s.contains("{"));
+}
+
 // ---- Overhead evaluation along a path ----
 
 #[test]
