CodingThrust
diff --git a/‎Makefile‎
Lines changed: 6 additions & 5 deletions b/‎Makefile‎
Lines changed: 6 additions & 5 deletions
diff --git a/‎docs/src/design.md‎
Lines changed: 258 additions & 185 deletions b/‎docs/src/design.md‎
Lines changed: 258 additions & 185 deletions
diff --git a/‎docs/src/getting-started.md‎
Lines changed: 56 additions & 10 deletions b/‎docs/src/getting-started.md‎
Lines changed: 56 additions & 10 deletions
diff --git a/‎docs/src/static/lattices-dark.svg‎
Lines changed: 687 additions & 0 deletions b/‎docs/src/static/lattices-dark.svg‎
Lines changed: 687 additions & 0 deletions
diff --git a/‎docs/src/static/lattices.svg‎
Lines changed: 687 additions & 0 deletions b/‎docs/src/static/lattices.svg‎
Lines changed: 687 additions & 0 deletions
diff --git a/‎docs/src/static/lattices.typ‎
Lines changed: 212 additions & 0 deletions b/‎docs/src/static/lattices.typ‎
Lines changed: 212 additions & 0 deletions
@@ -56,13 +56,14 @@ doc:
 	cp -r target/doc docs/book/api
 
 # Generate SVG diagrams from Typst sources (light + dark themes)
-TYPST_DIAGRAMS := $(wildcard docs/src/static/*.typ)
+TYPST_DOC_DIAGRAMS := $(wildcard docs/src/static/*.typ)
+TYPST_PAPER_DIAGRAMS := $(wildcard docs/paper/static/*.typ)
 diagrams:
-	@for src in $(TYPST_DIAGRAMS); do \
+	@for src in $(TYPST_DOC_DIAGRAMS); do \
 		base=$$(basename $$src .typ); \
-		echo "Compiling $$base..."; \
-		typst compile $$src --input dark=false docs/src/static/$$base.svg; \
-		typst compile $$src --input dark=true docs/src/static/$$base-dark.svg; \
+		echo "Compiling $$base (doc)..."; \
+		typst compile $$src --root=. --input dark=false docs/src/static/$$base.svg; \
+		typst compile $$src --root=. --input dark=true docs/src/static/$$base-dark.svg; \
 	done
 
 # Build and serve mdBook with API docs
 
@@ -55,25 +55,71 @@ assert!(metric.is_valid());
 
 ### Chaining Reductions
 
-Reductions can be chained. Each step preserves the solution mapping:
+Reductions compose into multi-step chains. A `ResolvedPath` describes the plan —
+each step carries the problem name and variant, each edge is either a `Reduction`
+(with overhead) or a `NaturalCast` (free subtype relaxation).
+Here we solve a 3-SAT formula by chaining through Satisfiability
+and MaximumIndependentSet:
 
 ```rust
+use std::collections::BTreeMap;
 use problemreductions::prelude::*;
 use problemreductions::topology::SimpleGraph;
+use problemreductions::rules::{ReductionGraph, EdgeKind};
+use problemreductions::solvers::ILPSolver;
 
-// SetPacking -> IndependentSet -> VertexCover
-let sp = MaximumSetPacking::<i32>::new(vec![vec![0, 1], vec![1, 2], vec![2, 3]]);
+// --- Plan: obtain a ResolvedPath ---
 
-let r1 = ReduceTo::<MaximumIndependentSet<SimpleGraph, i32>>::reduce_to(&sp);
-let r2 = ReduceTo::<MinimumVertexCover<SimpleGraph, i32>>::reduce_to(r1.target_problem());
+let graph = ReductionGraph::new();
+let path = graph.find_shortest_path_by_name("KSatisfiability", "MaximumIndependentSet").unwrap();
+let source = BTreeMap::from([("k".to_string(), "K3".to_string())]);
+let resolved = graph.resolve_path(&path, &source, &BTreeMap::new()).unwrap();
 
-// Solve final target, extract back through chain
-let solver = BruteForce::new();
-let vc_sol = solver.find_best(r2.target_problem()).unwrap();
-let is_sol = r2.extract_solution(&vc_sol);
-let sp_sol = r1.extract_solution(&is_sol);
+// The resolved path:
+//   step 0: KSatisfiability {k: "K3"}
+//   step 1: Satisfiability  {}
+//   step 2: MaximumIndependentSet {graph: "SimpleGraph", weight: "i32"}
+//   edge 0: Reduction  (K3-SAT → SAT, trivial embedding)
+//   edge 1: Reduction  (SAT → MIS, Karp 1972)
+
+// --- Execute: create, reduce, solve, extract ---
+
+// Create: 3-SAT formula (a∨b∨¬c)∧(¬a∨¬b∨¬c)∧(¬a∨b∨c)∧(a∨¬b∨c)
+let ksat = KSatisfiability::<K3>::new(3, vec![
+    CNFClause::new(vec![1, 2, -3]),    // a ∨ b ∨ ¬c
+    CNFClause::new(vec![-1, -2, -3]),  // ¬a ∨ ¬b ∨ ¬c
+    CNFClause::new(vec![-1, 2, 3]),    // ¬a ∨ b ∨ c
+    CNFClause::new(vec![1, -2, 3]),    // a ∨ ¬b ∨ c
+]);
+
+// Widen: 3-SAT → N-SAT (natural variant cast, KN accepts any clause size)
+let nsat = KSatisfiability::<KN>::new(ksat.num_vars(), ksat.clauses().to_vec());
+
+// Reduce: N-SAT → Satisfiability (trivial embedding)
+let r1 = ReduceTo::<Satisfiability>::reduce_to(&nsat);
+
+// Reduce: Satisfiability → MaximumIndependentSet (Karp reduction)
+let r2 = ReduceTo::<MaximumIndependentSet<SimpleGraph, i32>>::reduce_to(r1.target_problem());
+
+// Solve: MIS via ILP (internally: MIS → ILP → solve → extract)
+let ilp = ILPSolver::new();
+let mis_solution = ilp.solve_reduced(r2.target_problem()).unwrap();
+
+// Extract: trace back through the reduction chain
+let sat_solution = r2.extract_solution(&mis_solution);
+let nsat_solution = r1.extract_solution(&sat_solution);
+
+// Verify: satisfies the original 3-SAT formula
+assert!(ksat.evaluate(&nsat_solution));
 ```
 
+The `ILPSolver::solve_reduced()` handles the final MIS → ILP reduction,
+solve, and extraction internally. The caller traces back the explicit chain
+with `extract_solution()` at each step, recovering a satisfying assignment
+for the original formula.
+
+> **Note:** `ILPSolver` requires the `ilp` feature flag (see [Solvers](#solvers)).
+
 ## Solvers
 
 Two solvers for testing purposes are available:
 
@@ -0,0 +1,212 @@
+// Demonstration of graph types used in the problem-reductions library.
+// Compile:
+//   typst compile lattices.typ --input dark=false lattices.svg
+//   typst compile lattices.typ --input dark=true  lattices-dark.svg
+#import "@preview/cetz:0.4.2": canvas, draw
+#import "../../paper/lib.typ": g-node, g-edge
+
+#set page(width: auto, height: auto, margin: 12pt, fill: none)
+
+#let lattices(dark: false) = {
+  // ── Theme colors ────────────────────────────────────────────────
+  let (fg, edge-color, secondary) = if dark {
+    (rgb("#e2e8f0"), rgb("#94a3b8"), rgb("#94a3b8"))
+  } else {
+    (rgb("#1e293b"), rgb("#64748b"), rgb("#64748b"))
+  }
+
+  let (node-fill, node-highlight) = if dark {
+    (rgb("#1e3a5f"), rgb("#2563eb"))
+  } else {
+    (rgb("#dbeafe"), rgb("#93c5fd"))
+  }
+
+  let hyper-colors = if dark {
+    (
+      (fill: rgb("#1e3a5f").transparentize(30%), stroke: rgb("#60a5fa")),
+      (fill: rgb("#7f1d1d").transparentize(30%), stroke: rgb("#f87171")),
+      (fill: rgb("#064e3b").transparentize(30%), stroke: rgb("#34d399")),
+    )
+  } else {
+    (
+      (fill: rgb("#dbeafe").transparentize(40%), stroke: rgb("#4e79a7")),
+      (fill: rgb("#fecaca").transparentize(40%), stroke: rgb("#e15759")),
+      (fill: rgb("#d1fae5").transparentize(40%), stroke: rgb("#059669")),
+    )
+  }
+
+  let hyper-node-fill = if dark { rgb("#1e293b") } else { white }
+
+  let disk-fill = if dark {
+    rgb("#1e3a5f").transparentize(70%)
+  } else {
+    rgb("#dbeafe").transparentize(70%)
+  }
+
+  set text(fill: fg, size: 9pt)
+
+  // ── (a) SimpleGraph ──────────────────────────────────────────────
+  let simple-graph-fig() = {
+    import draw: *
+    let vs = ((0, 0), (2, 0), (0, 1.5), (2, 1.5), (1, 2.5))
+    let es = ((0,1),(0,2),(1,3),(2,3),(2,4),(3,4))
+    for (u, v) in es { g-edge(vs.at(u), vs.at(v), stroke: 1pt + edge-color) }
+    for (k, pos) in vs.enumerate() {
+      g-node(pos, name: "s" + str(k), fill: node-fill, stroke: 0.5pt + edge-color, label: str(k))
+    }
+  }
+
+  // ── (b) HyperGraph ──────────────────────────────────────────────
+  let hypergraph-fig() = {
+    import draw: *
+    let vs = ((0, 0), (1.5, 0.3), (2.5, 0), (0.5, 1.5), (2, 1.5), (1.2, 2.5))
+
+    // Hyperedge A: {0, 1, 3}
+    draw.hobby(
+      (-.3, -.3), (0.8, -.2), (1.9, 0.2), (0.8, 1.8), (-.2, 1.8), (-.5, 0.5),
+      close: true,
+      fill: hyper-colors.at(0).fill,
+      stroke: 0.8pt + hyper-colors.at(0).stroke,
+    )
+    // Hyperedge B: {1, 2, 4}
+    draw.hobby(
+      (1.1, -.2), (2.8, -.3), (2.6, 1.8), (1.6, 1.8), (0.9, 0.8),
+      close: true,
+      fill: hyper-colors.at(1).fill,
+      stroke: 0.8pt + hyper-colors.at(1).stroke,
+    )
+    // Hyperedge C: {3, 4, 5}
+    draw.hobby(
+      (0.1, 1.2), (1.6, 1.0), (2.4, 1.8), (1.5, 2.9), (0.1, 2.2),
+      close: true,
+      fill: hyper-colors.at(2).fill,
+      stroke: 0.8pt + hyper-colors.at(2).stroke,
+    )
+
+    for (k, pos) in vs.enumerate() {
+      g-node(pos, name: "h" + str(k), fill: hyper-node-fill, stroke: 1pt + edge-color, label: str(k))
+    }
+  }
+
+  // ── (c) UnitDiskGraph ────────────────────────────────────────────
+  let unit-disk-fig() = {
+    import draw: *
+    let vs = ((0.2, 0.2), (1.0, 0.0), (2.2, 0.3), (0.0, 1.2), (1.2, 1.5), (2.0, 1.1), (0.8, 2.3))
+    let r = 1.25
+
+    // Radius disk around vertex 4
+    draw.circle(vs.at(4), radius: r, fill: disk-fill, stroke: (dash: "dashed", paint: edge-color, thickness: 0.6pt))
+
+    // Compute edges: connect pairs within distance r
+    let es = ()
+    for i in range(vs.len()) {
+      for j in range(i + 1, vs.len()) {
+        let dx = vs.at(i).at(0) - vs.at(j).at(0)
+        let dy = vs.at(i).at(1) - vs.at(j).at(1)
+        if calc.sqrt(dx * dx + dy * dy) <= r {
+          es.push((i, j))
+        }
+      }
+    }
+
+    for (u, v) in es { g-edge(vs.at(u), vs.at(v), stroke: 0.8pt + edge-color) }
+    for (k, pos) in vs.enumerate() {
+      let fill = if k == 4 { node-highlight } else { node-fill }
+      g-node(pos, name: "u" + str(k), fill: fill, stroke: 0.5pt + edge-color, label: str(k))
+    }
+
+    // Radius label
+    draw.content((vs.at(4).at(0) + r + 0.15, vs.at(4).at(1) + 0.1), text(7pt, fill: secondary)[$r$])
+  }
+
+  // ── (d) KingsSubgraph ────────────────────────────────────────────
+  let kings-fig() = {
+    import draw: *
+    let rows = 4
+    let cols = 5
+    let sp = 0.6
+    let vs = ()
+    for row in range(rows) {
+      for col in range(cols) {
+        vs.push((col * sp, -row * sp))
+      }
+    }
+
+    let es = ()
+    for row in range(rows) {
+      for col in range(cols) {
+        let i = row * cols + col
+        if col + 1 < cols { es.push((i, i + 1)) }
+        if row + 1 < rows { es.push((i, i + cols)) }
+        if row + 1 < rows and col + 1 < cols { es.push((i, i + cols + 1)) }
+        if row + 1 < rows and col > 0 { es.push((i, i + cols - 1)) }
+      }
+    }
+
+    for (u, v) in es { g-edge(vs.at(u), vs.at(v), stroke: 0.6pt + edge-color) }
+    for (k, pos) in vs.enumerate() {
+      g-node(pos, name: "k" + str(k), radius: 0.12, fill: node-fill, stroke: 0.5pt + edge-color)
+    }
+  }
+
+  // ── (e) TriangularSubgraph ───────────────────────────────────────
+  let triangular-fig() = {
+    import draw: *
+    let rows = 5
+    let cols = 6
+    let sp = 0.6
+    let sqrt3_2 = calc.sqrt(3) / 2
+    let vs = ()
+    for row in range(rows) {
+      let offset = if calc.rem(row, 2) == 0 { 0 } else { 0.5 * sp }
+      for col in range(cols) {
+        vs.push((col * sp + offset, -row * sqrt3_2 * sp))
+      }
+    }
+
+    let es = ()
+    for row in range(rows) {
+      for col in range(cols) {
+        let i = row * cols + col
+        if col + 1 < cols { es.push((i, i + 1)) }
+        if row + 1 < rows {
+          if calc.rem(row, 2) == 0 {
+            if col > 0 { es.push((i, (row + 1) * cols + col - 1)) }
+            es.push((i, (row + 1) * cols + col))
+          } else {
+            es.push((i, (row + 1) * cols + col))
+            if col + 1 < cols { es.push((i, (row + 1) * cols + col + 1)) }
+          }
+        }
+      }
+    }
+
+    for (u, v) in es { g-edge(vs.at(u), vs.at(v), stroke: 0.5pt + edge-color) }
+    for (k, pos) in vs.enumerate() {
+      g-node(pos, name: "t" + str(k), radius: 0.1, fill: node-fill, stroke: 0.4pt + edge-color)
+    }
+  }
+
+  // ── Layout ───────────────────────────────────────────────────────
+  let font-size = 12pt
+  canvas({
+    import draw: *
+    simple-graph-fig()
+    content((1, -1), text(font-size, [(a) SimpleGraph]))
+    set-origin((5, 0))
+    hypergraph-fig()
+    content((1, -1), text(font-size, [(b) HyperGraph]))
+    set-origin((5, 0))
+    unit-disk-fig()
+    content((1, -1), text(font-size, [(c) UnitDiskGraph]))
+    set-origin((-10, -2))
+    kings-fig()
+    content((1, -2.6), text(font-size, [(d) KingsSubgraph]))
+    set-origin((5, 0))
+    triangular-fig()
+    content((1, -2.6), text(font-size, [(e) TriangularSubgraph]))
+  })
+}
+
+#let standalone-dark = sys.inputs.at("dark", default: "false") == "true"
+#lattices(dark: standalone-dark)