CodingThrust
diff --git a/‎.claude/CLAUDE.md‎
Lines changed: 8 additions & 7 deletions b/‎.claude/CLAUDE.md‎
Lines changed: 8 additions & 7 deletions
diff --git a/‎.claude/skills/issue-to-pr.md‎
Lines changed: 1 addition & 1 deletion b/‎.claude/skills/issue-to-pr.md‎
Lines changed: 1 addition & 1 deletion
diff --git a/‎docs/paper/reductions.typ‎
Lines changed: 22 additions & 13 deletions b/‎docs/paper/reductions.typ‎
Lines changed: 22 additions & 13 deletions
diff --git a/‎docs/paper/petersen_source.json‎ ‎docs/paper/static/petersen_source.json‎docs/paper/petersen_source.json renamed to docs/paper/static/petersen_source.json b/‎docs/paper/petersen_source.json‎ ‎docs/paper/static/petersen_source.json‎docs/paper/petersen_source.json renamed to docs/paper/static/petersen_source.json
diff --git a/‎…cs/paper/petersen_square_unweighted.json‎ ‎…r/static/petersen_square_unweighted.json‎docs/paper/petersen_square_unweighted.json renamed to docs/paper/static/petersen_square_unweighted.json b/‎…cs/paper/petersen_square_unweighted.json‎ ‎…r/static/petersen_square_unweighted.json‎docs/paper/petersen_square_unweighted.json renamed to docs/paper/static/petersen_square_unweighted.json
diff --git a/‎docs/paper/petersen_square_weighted.json‎ ‎…per/static/petersen_square_weighted.json‎docs/paper/petersen_square_weighted.json renamed to docs/paper/static/petersen_square_weighted.json b/‎docs/paper/petersen_square_weighted.json‎ ‎…per/static/petersen_square_weighted.json‎docs/paper/petersen_square_weighted.json renamed to docs/paper/static/petersen_square_weighted.json
diff --git a/‎docs/paper/petersen_triangular.json‎ ‎…cs/paper/static/petersen_triangular.json‎docs/paper/petersen_triangular.json renamed to docs/paper/static/petersen_triangular.json b/‎docs/paper/petersen_triangular.json‎ ‎…cs/paper/static/petersen_triangular.json‎docs/paper/petersen_triangular.json renamed to docs/paper/static/petersen_triangular.json
diff --git a/‎docs/plans/2026-02-14-type-system-cleanup-design.md‎
Lines changed: 131 additions & 0 deletions b/‎docs/plans/2026-02-14-type-system-cleanup-design.md‎
Lines changed: 131 additions & 0 deletions
@@ -81,8 +81,9 @@ enum Direction { Maximize, Minimize }
 - `ReductionResult` provides `target_problem()` and `extract_solution()`
 - `Solver::find_best()` → `Option<Vec<usize>>` for optimization problems; `Solver::find_satisfying()` → `Option<Vec<usize>>` for `Metric = bool`
 - `BruteForce::find_all_best()` / `find_all_satisfying()` return `Vec<Vec<usize>>` for all optimal/satisfying solutions
-- Graph types: SimpleGraph, GridGraph, UnitDiskGraph, Hypergraph
-- Weight types: `Unweighted` (marker), `i32`, `f64`
+- Graph types: SimpleGraph, GridGraph, UnitDiskGraph, Triangular, HyperGraph
+- Weight types: `One` (unit weight marker), `i32`, `f64` — all implement `WeightElement` trait
+- `WeightElement` trait: `type Sum: NumericSize` + `fn to_sum(&self)` — converts weight to a summable numeric type
 - Weight management via inherent methods (`weights()`, `set_weights()`, `is_weighted()`), not traits
 - `NumericSize` supertrait bundles common numeric bounds (`Clone + Default + PartialOrd + Num + Zero + Bounded + AddAssign + 'static`)
 
@@ -93,11 +94,11 @@ Problem types use explicit optimization prefixes:
 - No prefix: `MaxCut`, `SpinGlass`, `QUBO`, `ILP`, `Satisfiability`, `KSatisfiability`, `CircuitSAT`, `Factoring`, `MaximalIS`, `PaintShop`, `BicliqueCover`, `BMF`
 
 ### Problem Variant IDs
-Reduction graph nodes use variant IDs: `ProblemName[/GraphType][/Weighted]`
-- Base: `MaximumIndependentSet` (SimpleGraph, unweighted)
-- Graph variant: `MaximumIndependentSet/GridGraph`
-- Weighted variant: `MaximumIndependentSet/Weighted`
-- Both: `MaximumIndependentSet/GridGraph/Weighted`
+Reduction graph nodes use variant key-value pairs from `Problem::variant()`:
+- Base: `MaximumIndependentSet` (empty variant = defaults)
+- Graph variant: `MaximumIndependentSet {graph: "GridGraph", weight: "i32"}`
+- Weight variant: `MaximumIndependentSet {graph: "SimpleGraph", weight: "f64"}`
+- Nodes come exclusively from `#[reduction]` registrations; natural edges between same-name variants are inferred from the graph/weight subtype partial order
 
 ## Conventions
 
 
@@ -49,7 +49,7 @@ Present issue summary to user.
 
 Check that the issue template is fully filled out:
 - For **[Model]** issues: A clear mathmatical definition, Type specification, Variables and fields, The complexity clarification, verify an existing solver can solve it, or a solving strategy is provided, A detailed example for human.
-- For **[Rule]** issues: Source, Target, Reference to verify information, Implementable reduction algorithm, Test dataset generation method, Size overhead, A clear example for human.
+- For **[Rule]** issues: Source, Target, Reference to verify information, Implementable reduction algorithm, Test dataset generation method, Size overhead, A reduction example for human to verify the reduction is correct. Please put a high standard on the example: it must be in tutorial style with clear intuition and is easy to understand.
 
 Verify facts provided by the user, feel free to ask user questions. If any piece is missing or unclear, comment on the issue via `gh issue comment <number> --body "..."` to ask user clarify. Then stop and wait — do NOT proceed until the issue is complete.
 
 
@@ -44,6 +44,7 @@
   "CircuitSAT": [CircuitSAT],
   "Factoring": [Factoring],
   "GridGraph": [GridGraph MIS],
+  "Triangular": [Triangular MIS],
 )
 
 // Definition label: "def:<ProblemName>" — each definition block must have a matching label
@@ -60,15 +61,15 @@
 // Extract reductions for a problem from graph-data (returns (name, label) pairs)
 #let get-reductions-to(problem-name) = {
   graph-data.edges
-    .filter(e => e.source.name == problem-name)
-    .map(e => (name: e.target.name, lbl: reduction-label(e.source.name, e.target.name)))
+    .filter(e => graph-data.nodes.at(e.source).name == problem-name)
+    .map(e => (name: graph-data.nodes.at(e.target).name, lbl: reduction-label(graph-data.nodes.at(e.source).name, graph-data.nodes.at(e.target).name)))
     .dedup(key: e => e.name)
 }
 
 #let get-reductions-from(problem-name) = {
   graph-data.edges
-    .filter(e => e.target.name == problem-name)
-    .map(e => (name: e.source.name, lbl: reduction-label(e.source.name, e.target.name)))
+    .filter(e => graph-data.nodes.at(e.target).name == problem-name)
+    .map(e => (name: graph-data.nodes.at(e.source).name, lbl: reduction-label(graph-data.nodes.at(e.source).name, graph-data.nodes.at(e.target).name)))
     .dedup(key: e => e.name)
 }
 
@@ -166,9 +167,9 @@
 
 // Find edge in graph-data by source/target names
 #let find-edge(source, target) = {
-  let edge = graph-data.edges.find(e => e.source.name == source and e.target.name == target)
+  let edge = graph-data.edges.find(e => graph-data.nodes.at(e.source).name == source and graph-data.nodes.at(e.target).name == target)
   if edge == none {
-    edge = graph-data.edges.find(e => e.source.name == target and e.target.name == source)
+    edge = graph-data.edges.find(e => graph-data.nodes.at(e.source).name == target and graph-data.nodes.at(e.target).name == source)
   }
   edge
 }
@@ -205,9 +206,9 @@
 ) = {
   let arrow = sym.arrow.r
   let edge = find-edge(source, target)
-  let src-disp = if edge != none { variant-display(edge.source) }
+  let src-disp = if edge != none { variant-display(graph-data.nodes.at(edge.source)) }
                  else { display-name.at(source) }
-  let tgt-disp = if edge != none { variant-display(edge.target) }
+  let tgt-disp = if edge != none { variant-display(graph-data.nodes.at(edge.target)) }
                  else { display-name.at(target) }
   let src-lbl = label("def:" + source)
   let tgt-lbl = label("def:" + target)
@@ -851,10 +852,10 @@ The following reductions to Integer Linear Programming are straightforward formu
 *Example: Petersen Graph.*#footnote[Generated using `cargo run --example export_petersen_mapping` from the accompanying code repository.] The Petersen graph ($n=10$, MIS$=4$) maps to a $30 times 42$ King's subgraph with 219 nodes and overhead $Delta = 89$. Solving MIS on the grid yields $"MIS"(G_"grid") = 4 + 89 = 93$. The weighted and unweighted KSG mappings share identical grid topology (same node positions and edges); only the vertex weights differ. With triangular lattice encoding @nguyen2023, the same graph maps to a $42 times 60$ grid with 395 nodes and overhead $Delta = 375$, giving $"MIS"(G_"tri") = 4 + 375 = 379$.
 
 // Load JSON data
-#let petersen = json("petersen_source.json")
-#let square_weighted = json("petersen_square_weighted.json")
-#let square_unweighted = json("petersen_square_unweighted.json")
-#let triangular_mapping = json("petersen_triangular.json")
+#let petersen = json("static/petersen_source.json")
+#let square_weighted = json("static/petersen_square_weighted.json")
+#let square_unweighted = json("static/petersen_square_unweighted.json")
+#let triangular_mapping = json("static/petersen_triangular.json")
 
 #figure(
   grid(
@@ -884,6 +885,14 @@ The following reductions to Integer Linear Programming are straightforward formu
   caption: [Unit disk mappings of the Petersen graph. Blue: weight 1, red: weight 2, green: weight 3.],
 ) <fig:petersen-mapping>
 
+#reduction-rule("MaximumIndependentSet", "Triangular")[
+  @nguyen2023 Any MIS problem on a general graph $G$ can be reduced to MIS on a weighted triangular lattice graph with at most quadratic overhead in the number of vertices.
+][
+  _Construction._ Same copy-line method as the KSG mapping, but uses a triangular lattice instead of a square grid. Crossing and simplifier gadgets are adapted for triangular geometry, producing a unit disk graph on a triangular grid where edges connect nodes within unit distance under the triangular metric.
+
+  _Overhead._ Both vertex and edge counts grow as $O(n^2)$ where $n = |V|$, matching the KSG mapping.
+]
+
 *Weighted Extension.* For MWIS, copy lines use weighted vertices (weights 1, 2, or 3). Source weights $< 1$ are added to designated "pin" vertices.
 
 *QUBO Mapping.* A QUBO problem $min bold(x)^top Q bold(x)$ maps to weighted MIS on a grid by:
@@ -897,7 +906,7 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples
 #context {
   let covered = covered-rules.get()
   let json-edges = {
-    let edges = graph-data.edges.map(e => (e.source.name, e.target.name))
+    let edges = graph-data.edges.map(e => (graph-data.nodes.at(e.source).name, graph-data.nodes.at(e.target).name))
     let unique = ()
     for e in edges {
       if unique.find(u => u.at(0) == e.at(0) and u.at(1) == e.at(1)) == none {
 
@@ -0,0 +1,131 @@
+# Type System Cleanup Design
+
+## Problem
+
+The weight and trait system has several mathematical inconsistencies:
+
+1. **Weight dual role**: The type parameter `W` serves as both the per-element weight type and the accumulation/metric type. This prevents using a unit-weight type (`One`) because `One + One` can't produce `2` within the same type.
+
+2. **Dead abstractions**: `Unweighted(usize)` is never used as a type parameter. The `Weights` trait is implemented but never used outside its own tests. `NumericWeight` and `NumericSize` are nearly identical traits.
+
+3. **Missing satisfaction trait**: Satisfaction problems (SAT, CircuitSAT, KColoring, Factoring) use `Metric = bool` but have no shared trait. The `BruteForce::find_satisfying()` method uses `Problem<Metric = bool>` inline.
+
+## Design
+
+### 1. `WeightElement` trait + `One` type
+
+Introduce a trait that maps weight element types to their accumulation type:
+
+```rust
+/// Maps a weight element to its sum/metric type.
+pub trait WeightElement: Clone + Default + 'static {
+    /// The numeric type used for sums and comparisons.
+    type Sum: NumericSize;
+    /// Convert this weight element to the sum type.
+    fn to_sum(&self) -> Self::Sum;
+}
+```
+
+Implementations:
+
+```rust
+/// The constant 1. Unit weight for unweighted problems.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default, Serialize, Deserialize)]
+pub struct One;
+
+impl WeightElement for One {
+    type Sum = i32;
+    fn to_sum(&self) -> i32 { 1 }
+}
+
+impl WeightElement for i32 {
+    type Sum = i32;
+    fn to_sum(&self) -> i32 { *self }
+}
+
+impl WeightElement for f64 {
+    type Sum = f64;
+    fn to_sum(&self) -> f64 { *self }
+}
+```
+
+**Impact on problems:**
+
+Before:
+```rust
+impl<G, W> Problem for MaximumIndependentSet<G, W>
+where W: Clone + Default + PartialOrd + Num + Zero + AddAssign + 'static
+{
+    type Metric = SolutionSize<W>;
+    fn evaluate(&self, config: &[usize]) -> SolutionSize<W> {
+        let mut total = W::zero();
+        for (i, &sel) in config.iter().enumerate() {
+            if sel == 1 { total += self.weights[i].clone(); }
+        }
+        SolutionSize::Valid(total)
+    }
+}
+
+impl<G, W> OptimizationProblem for MaximumIndependentSet<G, W> {
+    type Value = W;
+}
+```
+
+After:
+```rust
+impl<G, W: WeightElement> Problem for MaximumIndependentSet<G, W>
+where W::Sum: PartialOrd
+{
+    type Metric = SolutionSize<W::Sum>;
+    fn evaluate(&self, config: &[usize]) -> SolutionSize<W::Sum> {
+        let mut total = W::Sum::zero();
+        for (i, &sel) in config.iter().enumerate() {
+            if sel == 1 { total += self.weights[i].to_sum(); }
+        }
+        SolutionSize::Valid(total)
+    }
+}
+
+impl<G, W: WeightElement> OptimizationProblem for MaximumIndependentSet<G, W> {
+    type Value = W::Sum;
+}
+```
+
+**Variant output:** `variant()` uses `short_type_name::<W>()` which returns `"One"`, `"i32"`, or `"f64"`. The variant label changes from `"Unweighted"` to `"One"`.
+
+### 2. `SatisfactionProblem` marker trait
+
+```rust
+/// Marker trait for satisfaction (decision) problems.
+pub trait SatisfactionProblem: Problem<Metric = bool> {}
+```
+
+Implemented by: `Satisfiability`, `KSatisfiability`, `CircuitSAT`, `KColoring`, `Factoring`.
+
+No new methods. Makes the problem category explicit in the type system. `BruteForce::find_satisfying()` can use `P: SatisfactionProblem` as its bound.
+
+### 3. Merge `NumericWeight` / `NumericSize`
+
+Delete `NumericWeight`. Keep `NumericSize` as the sole numeric bound trait:
+
+```rust
+pub trait NumericSize:
+    Clone + Default + PartialOrd + Num + Zero + Bounded + AddAssign + 'static
+{}
+```
+
+This is the bound on `WeightElement::Sum`. The extra `Bounded` requirement (vs the old `NumericWeight`) is needed for solver penalty calculations and is satisfied by `i32` and `f64`.
+
+### Removals
+
+- `Unweighted` struct (replaced by `One`)
+- `Weights` trait (unused, subsumed by `WeightElement`)
+- `NumericWeight` trait (merged into `NumericSize`)
+
+### Reduction impact
+
+Concrete `ReduceTo` impls change `Unweighted` references to `One`. The `ConcreteVariantEntry` registrations in `variants.rs` change `"Unweighted"` to `"One"`. The natural edge system (weight subtype hierarchy) adds `One` as a subtype of `i32`.
+
+### Variant impact
+
+The `variant()` output for unweighted problems changes from `("weight", "Unweighted")` to `("weight", "One")`. The reduction graph JSON, paper, and JavaScript visualization update accordingly.