CodingThrust
diff --git a/‎.claude/CLAUDE.md‎
Lines changed: 22 additions & 9 deletions b/‎.claude/CLAUDE.md‎
Lines changed: 22 additions & 9 deletions
diff --git a/‎.claude/rules/adding-models.md‎
Lines changed: 8 additions & 5 deletions b/‎.claude/rules/adding-models.md‎
Lines changed: 8 additions & 5 deletions
diff --git a/‎.claude/rules/adding-reductions.md‎
Lines changed: 3 additions & 3 deletions b/‎.claude/rules/adding-reductions.md‎
Lines changed: 3 additions & 3 deletions
diff --git a/‎.claude/rules/documentation.md‎
Lines changed: 36 additions & 22 deletions b/‎.claude/rules/documentation.md‎
Lines changed: 36 additions & 22 deletions
diff --git a/‎Makefile‎
Lines changed: 8 additions & 4 deletions b/‎Makefile‎
Lines changed: 8 additions & 4 deletions
diff --git a/‎benches/solver_benchmarks.rs‎
Lines changed: 13 additions & 13 deletions b/‎benches/solver_benchmarks.rs‎
Lines changed: 13 additions & 13 deletions
diff --git a/‎book.toml‎
Lines changed: 1 addition & 4 deletions b/‎book.toml‎
Lines changed: 1 addition & 4 deletions
@@ -16,15 +16,15 @@ make mdbook         # Build and serve mdBook with live reload
 make paper          # Build Typst paper (runs examples + exports first)
 make coverage       # Generate coverage report (>95% required)
 make check          # Quick pre-commit check (fmt + clippy + test)
-make export-graph   # Regenerate reduction graph JSON
+make rust-export    # Generate Rust mapping JSON exports
 make export-schemas # Regenerate problem schemas JSON
 make qubo-testdata  # Regenerate QUBO ground truth JSON
 make clean          # Clean build artifacts
 ```
 
 ## Verify Changes
 ```bash
-make test clippy export-graph  # Must pass before PR
+make test clippy  # Must pass before PR
 ```
 
 ## Architecture
@@ -47,7 +47,7 @@ make test clippy export-graph  # Must pass before PR
 ```
 Problem (core trait - all problems must implement)
 │
-├── const NAME: &'static str           // Problem name, e.g., "IndependentSet"
+├── const NAME: &'static str           // Problem name, e.g., "MaximumIndependentSet"
 ├── type GraphType: GraphMarker        // Graph topology marker
 ├── type Weight: NumericWeight         // Weight type (i32, f64, Unweighted)
 ├── type Size                          // Objective value type
@@ -75,20 +75,33 @@ ConstraintSatisfactionProblem : Problem (extension for CSPs)
 - Graph types: SimpleGraph, GridGraph, UnitDiskGraph, Hypergraph
 - Weight types: `Unweighted` (marker), `i32`, `f64`
 
+### Problem Names
+Problem types use explicit optimization prefixes:
+- `MaximumIndependentSet`, `MaximumClique`, `MaximumMatching`, `MaximumSetPacking`
+- `MinimumVertexCover`, `MinimumDominatingSet`, `MinimumSetCovering`
+- No prefix: `MaxCut`, `SpinGlass`, `QUBO`, `ILP`, `Satisfiability`, `KSatisfiability`, `CircuitSAT`, `Factoring`, `MaximalIS`
+
 ### Problem Variant IDs
 Reduction graph nodes use variant IDs: `ProblemName[/GraphType][/Weighted]`
-- Base: `IndependentSet` (SimpleGraph, unweighted)
-- Graph variant: `IndependentSet/GridGraph`
-- Weighted variant: `IndependentSet/Weighted`
-- Both: `IndependentSet/GridGraph/Weighted`
+- Base: `MaximumIndependentSet` (SimpleGraph, unweighted)
+- Graph variant: `MaximumIndependentSet/GridGraph`
+- Weighted variant: `MaximumIndependentSet/Weighted`
+- Both: `MaximumIndependentSet/GridGraph/Weighted`
 
 ## Conventions
 
 ### File Naming
-- Reduction files: `src/rules/<source>_<target>.rs`
-- Model files: `src/models/<category>/<name>.rs`
+- Reduction files: `src/rules/<source>_<target>.rs` (e.g., `maximumindependentset_qubo.rs`)
+- Model files: `src/models/<category>/<name>.rs` (e.g., `maximum_independent_set.rs`)
+- Example files: `examples/reduction_<source>_to_<target>.rs`
 - Test naming: `test_<source>_to_<target>_closed_loop`
 
+### Paper (docs/paper/reductions.typ)
+- `problem-def(name, title, body)` — defines a problem with auto-generated schema, reductions list, and label `<def:ProblemName>`
+- `reduction-rule(source, target, ...)` — generates a theorem with label `<thm:Source-to-Target>` and registers in `covered-rules` state
+- Completeness warnings auto-check that all JSON graph nodes/edges are covered in the paper
+- `display-name` dict maps `ProblemName` to display text
+
 ## Contributing
 See `.claude/rules/` for detailed guides:
 - `adding-reductions.md` - How to add reduction rules
 
@@ -36,9 +36,9 @@ pub use my_problem::MyProblem;
 
 ## 3. Categories
 Place models in appropriate category:
-- `src/models/satisfiability/` - SAT, K-SAT, CircuitSAT
-- `src/models/graph/` - IndependentSet, VertexCovering, Coloring, etc.
-- `src/models/set/` - SetCovering, SetPacking
+- `src/models/satisfiability/` - Satisfiability, KSatisfiability, CircuitSAT
+- `src/models/graph/` - MaximumIndependentSet, MinimumVertexCover, KColoring, etc.
+- `src/models/set/` - MinimumSetCovering, MaximumSetPacking
 - `src/models/optimization/` - SpinGlass, QUBO, ILP
 
 ## 4. Required Traits
@@ -47,8 +47,11 @@ Place models in appropriate category:
 - `Problem` - Core trait with `num_variables()`, `problem_size()`, `is_valid_solution()`
 - Consider `ConstraintSatisfactionProblem` if applicable
 
-## 5. Documentation
-Document in `docs/paper/reductions.typ`
+## 5. Naming
+Use explicit optimization prefixes: `Maximum` for maximization, `Minimum` for minimization (e.g., `MaximumIndependentSet`, `MinimumVertexCover`).
+
+## 6. Documentation
+Document in `docs/paper/reductions.typ` using `#problem-def("ProblemName", "Display Title")[...]`
 
 ## Anti-patterns
 - Don't create models without JSON serialization support
 
@@ -20,7 +20,7 @@ Before writing any Rust code, follow this workflow:
    # Example: generate QUBO test data
    cd scripts && uv run python generate_qubo_tests.py
    ```
-3. **Create a practical example** — design a small, explainable instance for `examples/` (e.g., "wireless tower placement" for IndependentSet, "map coloring" for Coloring). This example will also appear in the `docs/paper/reductions.typ`.
+3. **Create a practical example** — design a small, explainable instance for `examples/` (e.g., "wireless tower placement" for MaximumIndependentSet, "map coloring" for KColoring). This example will also appear in the `docs/paper/reductions.typ`.
 4. **Write the implementation plan** — save to `docs/plans/` using `superpowers:writing-plans`. The plan must include implementation details from the brainstorming session (formulas, penalty terms, matrix construction, variable indexing).
 
 ## 1. Implementation
@@ -84,9 +84,9 @@ Add a round-trip demo to `examples/` showing a practical, explainable instance:
 ## 4. Documentation
 
 Update `docs/paper/reductions.typ` (see `rules/documentation.md` for the pattern):
-- Add theorem + proof sketch
+- Add `reduction-rule("Source", "Target", ...)` theorem with proof sketch
 - Add Rust code example from the example program
-- Add to summary table with overhead and citation
+- Add `display-name` entry if the problem is new
 
 The goal is to 1. prove the correctness of the reduction to human beings. 2. provide a minimal working example to the readers.
 
 
@@ -7,34 +7,48 @@ paths:
 
 The technical paper (`docs/paper/reductions.typ`) must include:
 
-1. **Table of Contents** - Auto-generated outline of all sections
-2. **Problem Data Structures** - Rust struct with fields in a code block
-3. **Reduction Examples** - Minimal working example showing reduce → solve → extract
+1. **Problem Definitions** — using `problem-def` wrapper
+2. **Reduction Theorems** — using `reduction-rule` function
+3. **Reduction Examples** — minimal working example showing reduce → solve → extract
 
-## Pattern
+## Adding a Problem Definition
 
 ```typst
-#definition("Problem Name")[
+#problem-def("MaximumIndependentSet", "Maximum Independent Set (MIS)")[
   Mathematical definition...
 ]
+```
 
-// Rust data structure
-```rust
-pub struct ProblemName<W = i32> {
-    field1: Type1,
-    field2: Type2,
-}
-`` `
+This auto-generates:
+- A label `<def:MaximumIndependentSet>` for cross-references
+- The problem's schema (fields from Rust struct)
+- The list of available reductions
 
-#theorem[
-  *(Source → Target)* Reduction description...
-]
+Also add an entry to the `display-name` dictionary:
+```typst
+"MaximumIndependentSet": "MIS",
+```
+
+## Adding a Reduction Theorem
 
-// Minimal working example from closed-loop tests
-```rust
-let source = SourceProblem::new(...);
-let reduction = ReduceTo::<TargetProblem>::reduce_to(&source);
-let target = reduction.target_problem();
-// ... solve and extract
-`` `
+```typst
+#reduction-rule(
+  "MaximumIndependentSet", "QUBO",
+  example: "maximumindependentset_to_qubo",
+  overhead: (n: 0, m: 1),
+)[
+  Proof sketch...
+]
 ```
+
+This auto-generates:
+- A theorem label `<thm:MaximumIndependentSet-to-QUBO>`
+- References to source/target problem definitions (if they exist)
+- Registration in `covered-rules` state for completeness checking
+- The example code block from `examples/reduction_<example>.rs`
+
+## Completeness Warnings
+
+The paper auto-checks completeness:
+- After Problem Definitions: warns if JSON graph nodes are missing from `display-name`
+- After Reductions section: warns if JSON graph edges are missing from `covered-rules`
@@ -51,14 +51,18 @@ doc:
 	rm -rf docs/book/api
 	cp -r target/doc docs/book/api
 
-# Build and serve mdBook with live reload
+# Build and serve mdBook with API docs
 mdbook:
 	cargo run --example export_graph
 	cp docs/paper/reduction_graph.json docs/src/reductions/
 	cargo doc --all-features --no-deps
-	rm -rf docs/book/api
-	cp -r target/doc docs/book/api
-	mdbook serve docs --open
+	mdbook build
+	rm -rf book/api
+	cp -r target/doc book/api
+	@-fuser -k 3001/tcp 2>/dev/null || true
+	@echo "Serving at http://localhost:3001"
+	python3 -m http.server 3001 -d book &
+	@sleep 1 && xdg-open http://localhost:3001
 
 # Generate all example JSON files for the paper
 REDUCTION_EXAMPLES := $(patsubst examples/%.rs,%,$(wildcard examples/reduction_*.rs))
 
@@ -9,14 +9,14 @@ use problemreductions::models::set::*;
 use problemreductions::models::specialized::*;
 use problemreductions::prelude::*;
 
-/// Benchmark IndependentSet on graphs of varying sizes.
+/// Benchmark MaximumIndependentSet on graphs of varying sizes.
 fn bench_independent_set(c: &mut Criterion) {
-    let mut group = c.benchmark_group("IndependentSet");
+    let mut group = c.benchmark_group("MaximumIndependentSet");
 
     for n in [4, 6, 8, 10].iter() {
         // Create a path graph with n vertices
         let edges: Vec<(usize, usize)> = (0..*n - 1).map(|i| (i, i + 1)).collect();
-        let problem = IndependentSet::<SimpleGraph, i32>::new(*n, edges);
+        let problem = MaximumIndependentSet::<SimpleGraph, i32>::new(*n, edges);
         let solver = BruteForce::new();
 
         group.bench_with_input(BenchmarkId::new("path", n), n, |b, _| {
@@ -27,13 +27,13 @@ fn bench_independent_set(c: &mut Criterion) {
     group.finish();
 }
 
-/// Benchmark VertexCovering on graphs of varying sizes.
+/// Benchmark MinimumVertexCover on graphs of varying sizes.
 fn bench_vertex_covering(c: &mut Criterion) {
-    let mut group = c.benchmark_group("VertexCovering");
+    let mut group = c.benchmark_group("MinimumVertexCover");
 
     for n in [4, 6, 8, 10].iter() {
         let edges: Vec<(usize, usize)> = (0..*n - 1).map(|i| (i, i + 1)).collect();
-        let problem = VertexCovering::<SimpleGraph, i32>::new(*n, edges);
+        let problem = MinimumVertexCover::<SimpleGraph, i32>::new(*n, edges);
         let solver = BruteForce::new();
 
         group.bench_with_input(BenchmarkId::new("path", n), n, |b, _| {
@@ -109,16 +109,16 @@ fn bench_spin_glass(c: &mut Criterion) {
     group.finish();
 }
 
-/// Benchmark SetCovering on varying sizes.
+/// Benchmark MinimumSetCovering on varying sizes.
 fn bench_set_covering(c: &mut Criterion) {
-    let mut group = c.benchmark_group("SetCovering");
+    let mut group = c.benchmark_group("MinimumSetCovering");
 
     for num_sets in [4, 6, 8, 10].iter() {
         // Create overlapping sets
         let sets: Vec<Vec<usize>> = (0..*num_sets)
             .map(|i| vec![i, (i + 1) % *num_sets, (i + 2) % *num_sets])
             .collect();
-        let problem = SetCovering::<i32>::new(*num_sets, sets);
+        let problem = MinimumSetCovering::<i32>::new(*num_sets, sets);
         let solver = BruteForce::new();
 
         group.bench_with_input(
@@ -154,7 +154,7 @@ fn bench_matching(c: &mut Criterion) {
 
     for n in [4, 6, 8, 10].iter() {
         let edges: Vec<(usize, usize, i32)> = (0..*n - 1).map(|i| (i, i + 1, 1)).collect();
-        let problem = Matching::new(*n, edges);
+        let problem = MaximumMatching::new(*n, edges);
         let solver = BruteForce::new();
 
         group.bench_with_input(BenchmarkId::new("path", n), n, |b, _| {
@@ -192,9 +192,9 @@ fn bench_comparison(c: &mut Criterion) {
 
     let solver = BruteForce::new();
 
-    // IndependentSet with 8 vertices
-    let is_problem = IndependentSet::<SimpleGraph, i32>::new(8, vec![(0, 1), (2, 3), (4, 5), (6, 7)]);
-    group.bench_function("IndependentSet", |b| {
+    // MaximumIndependentSet with 8 vertices
+    let is_problem = MaximumIndependentSet::<SimpleGraph, i32>::new(8, vec![(0, 1), (2, 3), (4, 5), (6, 7)]);
+    group.bench_function("MaximumIndependentSet", |b| {
         b.iter(|| solver.find_best(black_box(&is_problem)))
     });
 
 
@@ -5,11 +5,8 @@ description = "A Rust library for reducing NP-hard problems"
 language = "en"
 src = "docs/src"
 
-[preprocessor.mermaid]
-command = "mdbook-mermaid"
-
 [output.html]
-default-theme = "rust"
+default-theme = "navy"
 git-repository-url = "https://github.com/CodingThrust/problem-reductions"
 edit-url-template = "https://github.com/CodingThrust/problem-reductions/edit/main/{path}"
 additional-css = []