diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 7aa4e1bba..b6b58ec6b 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -49,10 +49,15 @@ jobs:
node scripts/generate_reduction_graph_layout.js
cargo run --example export_schemas
cargo run --example export_module_graph
+ cargo build -p problemreductions-cli --bin pred
+ bash scripts/generate_doc_snippets.sh target/debug/pred
- name: Build mdBook
run: mdbook build
+ - name: Build research website
+ run: python3 scripts/build_website.py
+
- name: Build PDF
run: typst compile --root . docs/paper/reductions.typ book/reductions.pdf
diff --git a/Makefile b/Makefile
index ce9056ca2..1c3bbdfa9 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
# Makefile for problemreductions
-.PHONY: help build test mcp-test fmt clippy doc mdbook paper clean coverage rust-export compare qubo-testdata export-schemas release run-plan run-issue run-pipeline run-pipeline-forever run-review run-review-forever board-next board-claim board-ack board-move issue-context issue-guards pr-context pr-wait-ci worktree-issue worktree-pr diagrams jl-testdata cli cli-demo copilot-review papers papers-lookup papers-download papers-scihub papers-status papers-push papers-pull papers-index
+.PHONY: help build test mcp-test fmt clippy doc mdbook website paper clean coverage rust-export compare qubo-testdata export-schemas release run-plan run-issue run-pipeline run-pipeline-forever run-review run-review-forever board-next board-claim board-ack board-move issue-context issue-guards pr-context pr-wait-ci worktree-issue worktree-pr diagrams jl-testdata cli cli-demo copilot-review papers papers-lookup papers-download papers-scihub papers-status papers-push papers-pull papers-index
RUNNER ?= codex
CLAUDE_MODEL ?= opus
@@ -21,6 +21,7 @@ help:
@echo " doc - Build mdBook documentation"
@echo " diagrams - Generate SVG diagrams from Typst (light + dark)"
@echo " mdbook - Build and serve mdBook (with live reload)"
+ @echo " website - Build the research website and documentation"
@echo " paper - Build Typst paper from checked-in fixtures (requires typst)"
@echo " coverage - Generate coverage report (requires cargo-llvm-cov)"
@echo " clean - Clean build artifacts"
@@ -93,11 +94,23 @@ doc: node_modules/elkjs/package.json
node scripts/generate_reduction_graph_layout.js
cargo run --example export_schemas
cargo run --example export_module_graph
- bash scripts/generate_doc_snippets.sh target/release/pred
- mdbook build docs
+ cargo build -p problemreductions-cli --bin pred
+ bash scripts/generate_doc_snippets.sh target/debug/pred
+ mdbook build
+ python3 scripts/build_website.py
RUSTDOCFLAGS="--default-theme=dark" cargo doc --features ilp-highs --no-deps
- rm -rf docs/book/api
- cp -r target/doc docs/book/api
+ rm -rf book/api
+ cp -r target/doc book/api
+
+# Build the product website with fresh atlas data; API/PDF builds remain in doc/paper.
+website:
+ cargo run --example export_graph
+ cargo run --example export_schemas
+ cargo run --example export_module_graph
+ cargo build -p problemreductions-cli --bin pred
+ bash scripts/generate_doc_snippets.sh target/debug/pred
+ mdbook build
+ python3 scripts/build_website.py
# Generate SVG diagrams from Typst sources (light + dark themes)
TYPST_DOC_DIAGRAMS := $(wildcard docs/src/static/*.typ)
@@ -121,11 +134,13 @@ mdbook: node_modules/elkjs/package.json
@echo "Exporting module graph..."
@cargo run --example export_module_graph 2>&1 | tail -1
@echo "Generating CLI doc snippets..."
- @bash scripts/generate_doc_snippets.sh target/release/pred 2>&1 | tail -1
+ @cargo build -p problemreductions-cli --bin pred
+ @bash scripts/generate_doc_snippets.sh target/debug/pred
@echo "Building API docs..."
@RUSTDOCFLAGS="--default-theme=dark" cargo doc --features ilp-highs --no-deps 2>&1 | tail -1
@echo "Building mdBook..."
@mdbook build
+ @python3 scripts/build_website.py
rm -rf book/api
cp -r target/doc book/api
@-lsof -ti:3001 | xargs kill 2>/dev/null || true
diff --git a/book.toml b/book.toml
index bda4b2cf9..5c64bdbd7 100644
--- a/book.toml
+++ b/book.toml
@@ -9,9 +9,9 @@ src = "docs/src"
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 = ["docs/src/static/theme-images.css", "docs/src/static/reduction-graph.css", "docs/src/static/module-graph.css"]
-additional-js = ["docs/src/static/cytoscape.min.js", "docs/src/static/reduction-graph.js", "docs/src/static/module-graph.js"]
-no-section-label = false
+additional-css = ["docs/src/static/docs-theme.css", "docs/src/static/theme-images.css", "docs/src/static/reduction-graph.css", "docs/src/static/module-graph.css"]
+additional-js = ["docs/src/static/docs-theme.js", "docs/src/static/cytoscape.min.js", "docs/src/static/reduction-graph.js", "docs/src/static/module-graph.js"]
+no-section-label = true
[output.html.fold]
enable = true
diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md
index 35b5a14fa..c9ce4eece 100644
--- a/docs/src/SUMMARY.md
+++ b/docs/src/SUMMARY.md
@@ -1,18 +1,54 @@
# Summary
-[Introduction](./introduction.md)
+[Overview](introduction.md)
-# User Guide
+# Start here
-- [CLI Tool](./cli.md)
-- [AI Agent Skills](./skills.md)
+- [CLI in action](cli-demo.md)
+- [Start with an agent](skills.md)
+- [Install the CLI](install.md)
+- [First solve](cli.md)
-# Rust Library
+# Agent workflows
-- [Getting Started](./getting-started.md)
-- [Design](./design.md)
-- [API Reference](./api.md)
+- [Find a solver](agent-find-solver.md)
+- [Extend a solver's reach](agent-find-problem.md)
+- [Propose a model or rule](agent-propose.md)
+- [Implement and review](agent-pipeline.md)
+- [Connect with MCP](mcp.md)
+ - [Tool reference](mcp-tools.md)
+ - [Example session](mcp-walkthrough.md)
-# Reference
+# CLI reference
-- [MCP Server](./mcp.md)
+- [Explore the catalog](cli-catalog.md)
+- [Names and variants](cli-variants.md)
+- [Find reduction paths](cli-paths.md)
+- [Create an instance](cli-create.md)
+ - [Input examples](cli-examples.md)
+ - [Random instances](cli-random.md)
+- [Inspect and evaluate](cli-inspect.md)
+- [Reduce an instance](cli-reduce.md)
+- [Solve an instance](cli-solve.md)
+- [JSON and automation](cli-automation.md)
+- [Shell completions](cli-completions.md)
+
+# Rust library
+
+- [First Rust program](getting-started.md)
+- [Apply a reduction](rust-reduction.md)
+- [Discover and execute paths](rust-paths.md)
+- [Solver contracts](rust-solvers.md)
+- [API reference](api.md)
+
+# Internals
+
+- [Architecture](design.md)
+- [Problem contract](design-problem.md)
+- [Variant system](design-variants.md)
+ - [Register variants](design-variant-registration.md)
+- [Reduction contracts](design-reductions.md)
+- [Path costs and overhead](design-paths.md)
+- [JSON serialization](design-serialization.md)
+- [Reduction graph](reduction-graph.md)
+- [Contributing](contributing.md)
diff --git a/docs/src/agent-find-problem.md b/docs/src/agent-find-problem.md
new file mode 100644
index 000000000..8b5feff57
--- /dev/null
+++ b/docs/src/agent-find-problem.md
@@ -0,0 +1,29 @@
+# Extend a solver's reach
+
+Find source problems that can reduce to a solver you already have.
+
+**Before you start:** complete [agent setup](skills.md). Specify the solver's accepted model, topology, weights, and practical size limit.
+
+## Prompt
+
+```text
+Read .claude/skills/find-problem/SKILL.md and follow it.
+My solver accepts: [exact model and variant].
+Its time complexity and practical size limit: [details].
+Find incoming reduction routes and rank useful source problems.
+Show the assumptions and composed size overhead for each recommendation.
+Write the findings to docs/solutions/.
+```
+
+## Check the direction
+
+A solver for a target can handle sources that reduce **to** it. For example:
+
+```bash
+pred to QUBO
+pred path MIS QUBO
+```
+
+A route in the opposite direction does not establish that capability. Confirm each candidate's exact variants and measure the constructed target size on a small instance.
+
+Next: [reduce an instance](cli-reduce.md).
diff --git a/docs/src/agent-find-solver.md b/docs/src/agent-find-solver.md
new file mode 100644
index 000000000..1e54b9b82
--- /dev/null
+++ b/docs/src/agent-find-solver.md
@@ -0,0 +1,26 @@
+# Find a solver
+
+Map a concrete problem to a library model and a usable solver route.
+
+**Before you start:** complete [agent setup](skills.md). Describe the inputs, constraints, objective, and expected instance sizes.
+
+## Prompt
+
+```text
+Read .claude/skills/find-solver/SKILL.md and follow it.
+My problem: [describe inputs, constraints, and objective].
+Typical size: [counts and ranges].
+Available solvers or hardware: [list, or no preference].
+Check the exact model variant and current reduction paths with pred.
+Separate implemented routes from suggestions that need new work.
+```
+
+## Expected result
+
+A solution document in `docs/solutions/` with the proposed model, assumptions, reduction route, size overheads, and solver recommendation.
+
+## Check the recommendation
+
+Ask the agent to construct a small instance, solve it, and evaluate the recovered configuration on the original problem. If several models fit, resolve the modeling differences before scaling up.
+
+Next: [first solve](cli.md) or [inspect a route](cli-paths.md).
diff --git a/docs/src/agent-pipeline.md b/docs/src/agent-pipeline.md
new file mode 100644
index 000000000..7c3e757e6
--- /dev/null
+++ b/docs/src/agent-pipeline.md
@@ -0,0 +1,31 @@
+# Implement and review
+
+Move a prepared issue through the repository's agent workflow. These commands act on GitHub issues, project status, and pull requests; run them in a configured maintainer checkout.
+
+## Implement one issue
+
+```bash
+make run-issue N=42
+```
+
+Replace `42` with the issue number. The task follows `.claude/skills/issue-to-pr/SKILL.md`. Model and rule skills define the source, tests, examples, and paper changes required.
+
+To pick one eligible Ready issue from the project board:
+
+```bash
+make run-pipeline
+```
+
+## Review one pull request
+
+```bash
+make run-review N=570
+```
+
+Replace `570` with the PR number. The review workflow checks structure, quality, and user-facing behavior, then moves the PR to Final review. Maintainer review controls acceptance.
+
+## Evidence to retain
+
+Keep the mathematical argument, constructor and adversarial checks, closed-loop tests, canonical example, and review findings with the work. A passing test suite is evidence for tested instances, not a proof for all inputs.
+
+For exact workflow rules, read [the repository instructions](https://github.com/CodingThrust/problem-reductions/blob/main/.claude/CLAUDE.md).
diff --git a/docs/src/agent-propose.md b/docs/src/agent-propose.md
new file mode 100644
index 000000000..c936b496c
--- /dev/null
+++ b/docs/src/agent-propose.md
@@ -0,0 +1,24 @@
+# Propose a model or rule
+
+Turn a mathematical idea or published construction into a precise proposal for the atlas.
+
+**Before you start:** complete [agent setup](skills.md). Bring a definition, a source reference, or a candidate source → target connection.
+
+## Prompt
+
+```text
+Read .claude/skills/propose/SKILL.md and follow it.
+I want to propose: [model or source-to-target reduction].
+Reference or construction: [details].
+Check the current catalog for existing models and exact variant endpoints.
+Clarify the objective, solution mapping, correctness argument, and overhead.
+Prepare the proposal for the issue workflow.
+```
+
+## Expected result
+
+A model or rule proposal with explicit assumptions and enough mathematical detail to assess usefulness and correctness. The skill guides issue creation.
+
+For a rule, distinguish a construction supported by literature from a new conjecture. Record proof gaps and counterexamples explicitly.
+
+Next: [implementation and review](agent-pipeline.md) once the issue is ready.
diff --git a/docs/src/api.md b/docs/src/api.md
index 3025182bf..e534bb8d9 100644
--- a/docs/src/api.md
+++ b/docs/src/api.md
@@ -1,9 +1,7 @@
-# API Reference
+# API reference
-
+[Browse the Rust API →](api/problemreductions/index.html)
-Full API documentation is auto-generated from source code via `rustdoc`.
+The API is generated from Rust source with rustdoc. Start with [models](api/problemreductions/models/index.html), [reduction contracts](api/problemreductions/rules/index.html), or [solvers](api/problemreductions/solvers/index.html).
-**[Browse the API →](api/problemreductions/index.html)**
-
-If not redirected automatically, run `make doc` to generate the API docs.
+Run `make doc` to build the guides and API locally. For short runnable examples, see [first Rust program](getting-started.md) and [apply a reduction](rust-reduction.md).
diff --git a/docs/src/cli-automation.md b/docs/src/cli-automation.md
new file mode 100644
index 000000000..b2624f6be
--- /dev/null
+++ b/docs/src/cli-automation.md
@@ -0,0 +1,37 @@
+# JSON and automation
+
+Use structured output for agent tools and scripts.
+
+```bash
+pred list --json
+pred show MIS --json
+pred path MIS QUBO --json
+pred solve problem.json -o solution.json
+```
+
+| Global flag | Effect |
+|---|---|
+| `--json` | Request JSON output for data commands |
+| `-o, --output ` | Save JSON to a file |
+| `-q, --quiet` | Suppress informational messages on stderr |
+
+Check the process exit status before consuming a result. Preserve `type` and `variant` with each instance; an alias alone is insufficient to replay an exact endpoint.
+
+## Pipe instances
+
+```bash
+pred create MIS --graph 0-1,1-2,2-3 | pred solve - --json
+pred create MIS --graph 0-1,1-2,2-3 | pred reduce - --to QUBO | pred solve - --solver brute-force --json
+```
+
+`-` reads a problem or bundle from stdin. In shell automation, enable `set -o pipefail` so a failed earlier command fails the pipeline.
+
+## Registry exports
+
+```bash
+pred export-graph -o reduction_graph.json
+```
+
+The docs build publishes [reduction_graph.json](reductions/reduction_graph.json) and [problem_schemas.json](reductions/problem_schemas.json). The graph includes exact variants, directed edges, capabilities, and symbolic overheads; schemas describe model fields.
+
+Use the [Markdown index](markdown/index.md) for task instructions and these JSON files for structured registry queries. The exports describe the website's build; local CLI output describes the installed version.
diff --git a/docs/src/cli-catalog.md b/docs/src/cli-catalog.md
new file mode 100644
index 000000000..47c53cb53
--- /dev/null
+++ b/docs/src/cli-catalog.md
@@ -0,0 +1,22 @@
+# Explore the catalog
+
+Use the installed registry to discover models, accepted fields, and reductions.
+
+```bash
+pred list
+pred show MIS
+pred show MIS --json
+```
+
+`list` reports names and aliases. `show` describes the resolved variant, its size fields, input schema, and incoming/outgoing reductions. Use that schema before constructing an instance.
+
+
+Example: inspect Maximum Independent Set
+
+```text
+{{#include generated/pred-show-mis.txt}}
+```
+
+
+
+For machine-readable catalog data, use `pred list --json`. Use [names and variants](cli-variants.md) to select exact endpoints and [path queries](cli-paths.md) to explore their connections.
diff --git a/docs/src/cli-completions.md b/docs/src/cli-completions.md
new file mode 100644
index 000000000..a5ee8f3f5
--- /dev/null
+++ b/docs/src/cli-completions.md
@@ -0,0 +1,16 @@
+# Shell completions
+
+Enable tab completion by adding one line to your shell config:
+
+```bash
+# bash (~/.bashrc)
+eval "$(pred completions bash)"
+
+# zsh (~/.zshrc)
+eval "$(pred completions zsh)"
+
+# fish (~/.config/fish/config.fish)
+pred completions fish | source
+```
+
+If the shell argument is omitted, `pred completions` auto-detects your current shell.
diff --git a/docs/src/cli-create.md b/docs/src/cli-create.md
new file mode 100644
index 000000000..51318def0
--- /dev/null
+++ b/docs/src/cli-create.md
@@ -0,0 +1,26 @@
+# Create an instance
+
+**Input:** a model name or exact variant, plus fields from `pred show `.
+**Output:** a JSON problem file containing `type`, `variant`, and `data`.
+
+```bash
+pred create MIS --graph 0-1,1-2,2-3 -o problem.json
+pred create MIS/SimpleGraph/i32 --graph 0-1,1-2,2-3 --weights 2,1,3,1 -o weighted.json
+pred inspect weighted.json
+```
+
+Vertices use zero-based indices. `--graph` is a comma-separated edge list; weights must match the model's expected vertices or edges.
+
+## Use a canonical example
+
+```bash
+pred create --example MIS/SimpleGraph/i32 -o model.json
+pred create --example MVC/SimpleGraph/i32 --to MIS/SimpleGraph/i32 -o source.json
+pred create --example MVC/SimpleGraph/i32 --to MIS/SimpleGraph/i32 --example-side target -o target.json
+```
+
+The first command loads a model fixture. The next two load the source and target of a documented reduction example.
+
+CLI fields follow schema names: `universe_size` becomes `--universe-size`, and `subsets` becomes `--subsets`.
+
+Next: [input examples](cli-examples.md), [random instances](cli-random.md), or [inspect and evaluate](cli-inspect.md).
diff --git a/docs/src/cli-demo.md b/docs/src/cli-demo.md
new file mode 100644
index 000000000..b7e90437e
--- /dev/null
+++ b/docs/src/cli-demo.md
@@ -0,0 +1,35 @@
+# CLI in action
+
+From a graph to a checked solution in six commands. This recording runs the real CLI: discover a route, transform the instance, solve, and verify the result.
+
+
+
+[Open the player](static/cli-demo.html) · [Download the cast](static/cli-demo.cast) · [Download the offline HTML](static/cli-demo.html)
+
+## Run it yourself
+
+[Install `pred`](install.md), then run in a fresh directory. The recording uses `./pred`, a local build of the same executable.
+
+```bash
+pred path MIS ILP
+pred create MIS --graph 0-1,1-2,2-3,3-4,4-0 -o cycle.json
+pred reduce cycle.json --to ILP -o reduced.json
+pred solve reduced.json
+pred evaluate cycle.json --config 1,0,1,0,0
+pred solve cycle.json --solver brute-force
+```
+
+## What to check
+
+The recorded route goes through Maximum Set Packing and a weight cast before reaching binary ILP. `reduced.json` preserves the source instance and path so the solver can recover a source solution.
+
+| Check | Recorded result |
+|---|---|
+| Solve the reduction bundle | `Max(2)`, configuration `[1,0,1,0,0]` |
+| Evaluate that source configuration | `Max(2)` |
+| Exhaustive source solve | `Max(2)`, configuration `[0,0,1,0,1]` |
+| Command exit codes | All six returned `0` |
+
+Different configurations can have the same optimum. This cross-check validates this instance; a reduction's general correctness requires a mathematical argument.
+
+Next: [JSON output for agents](cli-automation.md) or [find another route](cli-paths.md).
diff --git a/docs/src/cli-examples.md b/docs/src/cli-examples.md
new file mode 100644
index 000000000..f2b9cf90b
--- /dev/null
+++ b/docs/src/cli-examples.md
@@ -0,0 +1,42 @@
+# Input examples
+
+Create small instances for different input structures. Use `pred show ` for its schema and `pred create --help` for flag syntax.
+
+## Boolean formula
+
+```bash
+pred create SAT --num-vars 3 --clauses '1,2;-1,3' -o sat.json
+```
+
+Clauses are separated by semicolons. Literals are signed, one-based variable indices; `-1` negates variable 1.
+
+## Quadratic matrix
+
+```bash
+pred create QUBO --matrix '1,0.5;0.5,2' -o qubo.json
+```
+
+Semicolons separate rows; commas separate entries.
+
+## Set system
+
+```bash
+pred create X3C --universe-size 6 --subsets '0,1,2;3,4,5;0,3,4' -o x3c.json
+```
+
+Subset elements use zero-based indices into the universe.
+
+## Integer factoring
+
+```bash
+pred create Factoring --target 6 --m 2 --n 2 -o factoring.json
+```
+
+## Check an instance
+
+```bash
+pred inspect sat.json
+pred solve sat.json --solver brute-force
+```
+
+For other models, start from `pred create --example ` and inspect its fields. Brute-force cost is the product of variable domain sizes; use tiny examples.
diff --git a/docs/src/cli-inspect.md b/docs/src/cli-inspect.md
new file mode 100644
index 000000000..4dde633bd
--- /dev/null
+++ b/docs/src/cli-inspect.md
@@ -0,0 +1,31 @@
+# Inspect and evaluate
+
+Use `inspect` to identify a problem file or reduction bundle. Use `evaluate` to check a specific configuration against the original instance.
+
+## Inspect a file
+
+```bash
+pred create MIS --graph 0-1,1-2,2-3 -o problem.json
+pred inspect problem.json
+pred inspect problem.json --json
+```
+
+Inspect the resolved variant and sizes before choosing a solver.
+
+## Evaluate a configuration
+
+```bash
+pred evaluate problem.json --config 1,0,1,0
+```
+
+This selects vertices 0 and 2 and returns `Max(2)`. Selecting adjacent vertices is invalid and returns `Max(None)`.
+
+Configurations follow each problem's variable domains; they are not always binary. Check the model definition before constructing one.
+
+## Read from stdin
+
+```bash
+pred create MIS --graph 0-1,1-2,2-3 | pred evaluate - --config 1,0,1,0
+```
+
+Evaluation checks one candidate. It does not establish optimality; compare with [a solver](cli-solve.md).
diff --git a/docs/src/cli-paths.md b/docs/src/cli-paths.md
new file mode 100644
index 000000000..740350dc5
--- /dev/null
+++ b/docs/src/cli-paths.md
@@ -0,0 +1,34 @@
+# Find reduction paths
+
+Choose source and target [variants](cli-variants.md), then query their direction of reachability.
+
+```bash
+pred path MIS ILP
+pred from MIS
+pred to QUBO
+```
+
+`from` explores outgoing routes; `to` explores incoming routes. `path` finds a route between the supplied endpoints. Search defaults to witness-capable reductions.
+
+## Save and compare routes
+
+```bash
+pred path MIS QUBO -o path.json
+pred path MIS QUBO --all --max-paths 50
+pred path MIS QUBO --cost minimize-steps
+pred path MIS QUBO --cost minimize:num_variables
+```
+
+`--all` is capped (20 paths by default); inspect the truncation indicator. A saved single path can be used with `pred reduce --via path.json`.
+
+The default cost minimizes steps. Size-based costs use reduction overhead metadata; inspect available size fields with `pred show`. Overhead formulas describe scaling bounds, not exact constructed instance sizes.
+
+## Multi-step example
+
+```text
+{{#include generated/pred-path-factoring-spinglass.txt}}
+```
+
+A discovered path does not imply the target will be inexpensive to solve. Measure the target size and solver behavior on representative instances.
+
+Next: [apply a path](cli-reduce.md) or [understand overhead](design-paths.md).
diff --git a/docs/src/cli-random.md b/docs/src/cli-random.md
new file mode 100644
index 000000000..c421a655c
--- /dev/null
+++ b/docs/src/cli-random.md
@@ -0,0 +1,13 @@
+# Random instances
+
+Generate a small graph for exploration:
+
+```bash
+pred create MIS --random --num-vertices 10 -o random.json
+pred inspect random.json
+pred solve random.json --solver brute-force
+```
+
+Use `pred create --help` for generation options supported by the current build. Random generation is available for selected input structures; it is not a constructor for every model.
+
+Save the generated JSON when reporting results so another agent can reproduce the exact instance. Use [canonical examples](cli-create.md#use-a-canonical-example) for stable demonstrations.
diff --git a/docs/src/cli-reduce.md b/docs/src/cli-reduce.md
new file mode 100644
index 000000000..48071c9a3
--- /dev/null
+++ b/docs/src/cli-reduce.md
@@ -0,0 +1,31 @@
+# Reduce an instance
+
+**Before you start:** [create a problem file](cli-create.md) and [find a route](cli-paths.md).
+
+## Choose a target
+
+```bash
+pred reduce problem.json --to QUBO -o reduced.json
+pred inspect reduced.json
+```
+
+The reduction bundle contains the source instance, target instance, and variant-level path. Keep the whole bundle to preserve solution recovery.
+
+## Use a saved path
+
+```bash
+pred path MIS QUBO -o path.json
+pred reduce problem.json --via path.json -o reduced.json
+```
+
+The path determines the target; `--to` is unnecessary. The input must match the path's source variant. For a weighted input, find a path from its exact weighted variant.
+
+## Solve and recover
+
+```bash
+pred solve reduced.json --solver brute-force
+```
+
+The solver solves the target and maps the result back through the bundle. Keep targets small when using brute force. For JSON output, the `intermediate` field records the target result alongside the recovered source solution.
+
+Next: [solver options](cli-solve.md) or [pipeline commands](cli-automation.md).
diff --git a/docs/src/cli-solve.md b/docs/src/cli-solve.md
new file mode 100644
index 000000000..6afd49824
--- /dev/null
+++ b/docs/src/cli-solve.md
@@ -0,0 +1,37 @@
+# Solve an instance
+
+**Input:** a problem JSON file or a complete reduction bundle.
+**Output:** the evaluation and, for witness-capable problems, a solution configuration.
+
+```bash
+pred solve problem.json
+pred solve problem.json --solver brute-force
+pred solve problem.json --timeout 30
+pred solve problem.json -o solution.json
+```
+
+## Choose a solver
+
+| Solver | Behavior |
+|---|---|
+| `ilp` (default) | Finds a witness-capable ILP route, solves the target, and recovers a source configuration |
+| `brute-force` | Enumerates configurations; use for tiny instances and cross-checks |
+| `customized` | Uses exact backends for selected models; inspect `pred solve --help` for supported models |
+
+If ILP reports no route, inspect `pred path ILP` and try brute force on a small instance. A model's presence in the catalog does not guarantee every solver supports it.
+
+## Solve a bundle
+
+```bash
+pred solve reduced.json --json
+```
+
+A bundle requires a witness-capable target and path. Its result includes the recovered source solution and the intermediate target result.
+
+Aggregate-only problems produce values without representative configurations. Do not assume every successful solve contains a witness.
+
+## Verify the result
+
+Evaluate the returned configuration on the original instance using `pred evaluate`. For a tiny example, compare its objective with an exhaustive solve. Different optimal configurations are acceptable when their evaluations agree.
+
+Next: [JSON and automation](cli-automation.md).
diff --git a/docs/src/cli-variants.md b/docs/src/cli-variants.md
new file mode 100644
index 000000000..0f8cce33f
--- /dev/null
+++ b/docs/src/cli-variants.md
@@ -0,0 +1,20 @@
+# Names and variants
+
+Aliases such as `MIS` resolve to full problem names. A bare name selects that model's declared default variant; `MIS` resolves to `MaximumIndependentSet/SimpleGraph/One`.
+
+## Select an exact variant
+
+```bash
+pred show MIS/SimpleGraph/i32
+pred path MIS/SimpleGraph/i32 ILP/bool
+```
+
+Slash-separated parameters select graph, weight, or other variant values. Use `pred list` and `pred show` to inspect the registry instead of guessing a variant.
+
+`One` means unit weights. Providing non-unit `--weights` when creating a default MIS instance upgrades it to `i32`. Specify `MIS/SimpleGraph/i32` explicitly when a reproducible endpoint matters.
+
+## Common aliases
+
+{{#include generated/pred-aliases.txt}}
+
+Next: [find a path](cli-paths.md).
diff --git a/docs/src/cli.md b/docs/src/cli.md
index e94f4456e..6a7282587 100644
--- a/docs/src/cli.md
+++ b/docs/src/cli.md
@@ -1,449 +1,25 @@
# CLI Tool
-The `pred` command-line tool lets you explore the reduction graph, create problem instances, solve problems, and perform reductions — all from your terminal.
+Create and solve your first problem with `pred`. [Install the CLI](install.md) before running these commands in a fresh working directory.
-## Installation
-
-Install from crates.io:
-
-```bash
-cargo install problemreductions-cli
-```
-
-Or build from source:
+## Create a graph problem
```bash
-git clone https://github.com/CodingThrust/problem-reductions
-cd problem-reductions
-cargo build -p problemreductions-cli --release # builds target/release/pred
-cargo install --path problemreductions-cli # optional: installs `pred` to ~/.cargo/bin
+pred create MIS --graph 0-1,1-2,2-3,3-4,4-0 -o cycle.json
```
-Verify the installation:
-
-```bash
-pred --version
-```
+`MIS` means Maximum Independent Set: select as many pairwise non-adjacent vertices as possible. This graph is a cycle with five vertices.
-For a workspace-local run without installing globally, use:
+## Solve and check
```bash
-cargo run -p problemreductions-cli --bin pred -- --version
-```
-
-### ILP Backend
-
-The default ILP backend is HiGHS. To use a different backend:
-
-```bash
-cargo install problemreductions-cli --features coin-cbc
-cargo install problemreductions-cli --features scip
-cargo install problemreductions-cli --no-default-features --features clarabel
-```
-
-Available backends: `highs` (default), `coin-cbc`, `clarabel`, `scip`, `lpsolve`, `microlp`.
-
-## Quick Start
-
-```bash
-# Create a Maximum Independent Set problem
-pred create MIS --graph 0-1,1-2,2-3 -o problem.json
-
-# Create a weighted instance (variant auto-upgrades to i32)
-pred create MIS --graph 0-1,1-2,2-3 --weights 3,1,2,1 -o weighted.json
-
-# Create a Steiner Tree instance
-pred create SteinerTree --graph 0-1,0-3,1-2,1-3,2-3,2-4,3-4 --edge-weights 2,5,2,1,5,6,1 --terminals 0,2,4 -o steiner.json
-
-# Create a Length-Bounded Disjoint Paths instance
-pred create LengthBoundedDisjointPaths --graph 0-1,1-6,0-2,2-3,3-6,0-4,4-5,5-6 --source 0 --sink 6 --bound 4 -o lbdp.json
-
-# Create a Consecutive Block Minimization instance (alias: CBM)
-pred create CBM --matrix '[[true,false,true],[false,true,true]]' --bound 2 -o cbm.json
-
-# CBM currently needs the brute-force solver
-pred solve cbm.json --solver brute-force
-
-# Or start from a canonical model example
-pred create --example MIS/SimpleGraph/i32 -o example.json
-
-# Or from a canonical rule example
-pred create --example MVC/SimpleGraph/i32 --to MIS/SimpleGraph/i32 -o example.json
-
-# Inspect what's inside a problem file
-pred inspect problem.json
-
-# Inspect the new path problem
-pred inspect lbdp.json
-
-# Solve it (auto-reduces to ILP)
-pred solve problem.json
-
-# Or solve with brute-force
-pred solve problem.json --solver brute-force
-
-# LengthBoundedDisjointPaths currently needs brute-force
-pred solve lbdp.json --solver brute-force
-
-# Evaluate a specific configuration (shows the aggregate value, e.g. Max(2) or Min(None))
-pred evaluate problem.json --config 1,0,1,0
-
-# Reduce to another problem type and solve via brute-force
-pred reduce problem.json --to QUBO -o reduced.json
-pred solve reduced.json --solver brute-force
-
-# Pipe commands together (use - to read from stdin)
-pred create MIS --graph 0-1,1-2,2-3 | pred solve - # when an ILP reduction path exists
-pred create StringToStringCorrection --source-string "0,1,2,3,1,0" --target-string "0,1,3,2,1" --bound 2 | pred solve - --solver brute-force
-pred create MIS --graph 0-1,1-2,2-3 | pred reduce - --to QUBO | pred solve -
-```
-
-> **Note:** When you provide `--weights` with non-unit values (e.g., `3,1,2,1`), the variant is
-> automatically upgraded from the default unit-weight (`One`) to `i32`. You can also specify the
-> weighted variant explicitly: `pred create MIS/SimpleGraph/i32 --graph 0-1 --weights 3,1`.
-
-## Global Flags
-
-| Flag | Description |
-|------|-------------|
-| `-o, --output ` | Save JSON output to a file |
-| `--json` | Output JSON to stdout instead of human-readable text |
-| `-q, --quiet` | Suppress informational messages on stderr |
-
-## Commands
-
-### `pred list` — List all problem types
-
-Lists all registered problem types with their short aliases.
-
-```text
-{{#include generated/pred-list.txt}}
-```
-
-### `pred show` — Inspect a problem
-
-Show fields, size fields, and reductions for a problem's default variant. Use short aliases like `MIS` for `MaximumIndependentSet`. Use `pred to` or `pred from` for variant-level neighborhood exploration.
-
-```text
-{{#include generated/pred-show-mis.txt}}
+pred solve cycle.json
+pred evaluate cycle.json --config 1,0,1,0,0
+pred solve cycle.json --solver brute-force
```
-### `pred to` — Explore incoming neighbors
+Both solvers return `Max(2)`. The configuration `1,0,1,0,0` selects vertices 0 and 2 and evaluates to the same value. Several optimal configurations exist, so the solvers may return different selections.
-Explore which problems can reduce **to** the given problem within k hops:
+The default solver discovers a route to ILP and maps the solution back. Brute force checks all configurations; keep instances small.
-```text
-{{#include generated/pred-to-mis.txt}}
-```
-
-### `pred from` — Explore outgoing neighbors
-
-Explore which problems the given problem can reduce to, starting **from** it:
-
-```text
-{{#include generated/pred-from-qubo.txt}}
-```
-
-### `pred path` — Find a reduction path
-
-Find the cheapest chain of reductions between two problems:
-
-```text
-{{#include generated/pred-path-mis-qubo.txt}}
-```
-
-Multi-step paths are discovered automatically:
-
-```text
-{{#include generated/pred-path-factoring-spinglass.txt}}
-```
-
-Show all paths or save for later use with `pred reduce --via`:
-
-```bash
-pred path MIS QUBO --all # all paths (up to 20)
-pred path MIS QUBO --all --max-paths 50 # increase limit
-pred path MIS QUBO -o path.json # save path for `pred reduce --via`
-pred path MIS QUBO --all -o paths/ # save all paths to a folder
-```
-
-When using `--all`, the output is capped at `--max-paths` (default: 20). If more paths exist, the output indicates truncation.
-
-Use `--cost` to change the optimization strategy:
-
-```bash
-pred path MIS QUBO --cost minimize-steps # default
-pred path MIS QUBO --cost minimize:num_variables # minimize a size field
-```
-
-Use `pred show ` to see which size fields are available.
-
-### `pred export-graph` — Export the reduction graph
-
-Export the full reduction graph as JSON:
-
-```bash
-pred export-graph # print to stdout
-pred export-graph -o reduction_graph.json # save to file
-```
-
-### `pred create` — Create a problem instance
-
-Construct a problem instance from CLI arguments and save as JSON:
-
-```bash
-pred create --example MIS/SimpleGraph/i32 -o model.json
-pred create --example MVC/SimpleGraph/i32 --to MIS/SimpleGraph/i32 -o problem.json
-pred create --example MVC/SimpleGraph/i32 --to MIS/SimpleGraph/i32 --example-side target -o target.json
-pred create MIS --graph 0-1,1-2,2-3 -o problem.json
-pred create MIS --graph 0-1,1-2,2-3 --weights 2,1,3,1 -o problem.json
-pred create SAT --num-vars 3 --clauses "1,2;-1,3" -o sat.json
-pred create QUBO --matrix "1,0.5;0.5,2" -o qubo.json
-pred create CBM --matrix '[[true,false,true],[false,true,true]]' --bound 2 -o cbm.json
-pred create KColoring --k 3 --graph 0-1,1-2,2-0 -o kcol.json
-pred create KthBestSpanningTree --graph 0-1,0-2,1-2 --edge-weights 2,3,1 --k 1 --bound 3 -o kth.json
-pred create SpinGlass --graph 0-1,1-2 -o sg.json
-pred create MaxCut --graph 0-1,1-2,2-0 -o maxcut.json
-pred create MinMaxMulticenter --graph 0-1,1-2,2-3 --weights 1,1,1,1 --edge-weights 1,1,1 --k 2 -o pcenter.json
-pred create ShortestWeightConstrainedPath --graph 0-1,0-2,1-3,2-3,2-4,3-5,4-5,1-4 --edge-lengths 2,4,3,1,5,4,2,6 --edge-weights 5,1,2,3,2,3,1,1 --source-vertex 0 --target-vertex 5 --weight-bound 8 -o swcp.json
-pred create RectilinearPictureCompression --matrix "1,1,0,0;1,1,0,0;0,0,1,1;0,0,1,1" --k 2 -o rpc.json
-pred solve rpc.json --solver brute-force
-pred create MinimumMultiwayCut --graph 0-1,1-2,2-3,3-0 --terminals 0,2 --edge-weights 3,1,2,4 -o mmc.json
-pred create SteinerTree --graph 0-1,0-3,1-2,1-3,2-3,2-4,3-4 --edge-weights 2,5,2,1,5,6,1 --terminals 0,2,4 -o steiner.json
-pred create UndirectedTwoCommodityIntegralFlow --graph 0-2,1-2,2-3 --capacities 1,1,2 --source-1 0 --sink-1 3 --source-2 1 --sink-2 3 --requirement-1 1 --requirement-2 1 -o utcif.json
-pred create LengthBoundedDisjointPaths --graph 0-1,1-6,0-2,2-3,3-6,0-4,4-5,5-6 --source 0 --sink 6 --bound 4 -o lbdp.json
-pred create Factoring --target 15 --bits-m 4 --bits-n 4 -o factoring.json
-pred create Factoring --target 21 --bits-m 3 --bits-n 3 -o factoring2.json
-pred create X3C --universe 9 --sets "0,1,2;0,2,4;3,4,5;3,5,7;6,7,8;1,4,6;2,5,8" -o x3c.json
-pred create MinimumCardinalityKey --num-attributes 6 --dependencies "0,1>2;0,2>3;1,3>4;2,4>5" -o mck.json
-pred create MinimumTardinessSequencing --n 5 --deadlines 5,5,5,3,3 --precedence-pairs "0>3,1>3,1>4,2>4" -o mts.json
-pred create SchedulingWithIndividualDeadlines --n 7 --deadlines 2,1,2,2,3,3,2 --num-processors 3 --precedence-pairs "0>3,1>3,1>4,2>4,2>5" -o swid.json
-pred solve swid.json --solver brute-force
-pred create SequencingToMinimizeWeightedCompletionTime --lengths 2,1,3,1,2 --weights 3,5,1,4,2 --precedence-pairs "0>2,1>4" -o stmwct.json
-pred create StringToStringCorrection --source-string "0,1,2,3,1,0" --target-string "0,1,3,2,1" --bound 2 | pred solve - --solver brute-force
-pred create StrongConnectivityAugmentation --arcs "0>1,1>2,2>0,3>4,4>3,2>3,4>5,5>3" --candidate-arcs "3>0:5,3>1:3,3>2:4,4>0:6,4>1:2,4>2:7,5>0:4,5>1:3,5>2:1,0>3:8,0>4:3,0>5:2,1>3:6,1>4:4,1>5:5,2>4:3,2>5:7,1>0:2" --bound 1 -o sca.json
-```
-
-For `LengthBoundedDisjointPaths`, the CLI flag `--bound` maps to the JSON field
-`max_length`.
-
-For `ConsecutiveBlockMinimization`, the `--matrix` flag expects a JSON 2D bool array such as
-`'[[true,false,true],[false,true,true]]'`. The example above shows the accepted shape, and solving
-CBM instances currently requires `--solver brute-force`.
-
-For problem-specific create help, run `pred create ` with no additional flags.
-The generic `pred create --help` output lists all flags across all problem types.
-
-Canonical examples are useful when you want a known-good instance from the paper/example database.
-For model examples, `pred create --example ` emits the canonical instance for that
-graph node.
-For rule examples, `pred create --example --to ` emits the source
-instance by default; use `--example-side target` to emit the reduction target instance instead.
-
-Generate random instances for graph-based problems:
-
-```bash
-pred create MIS --random --num-vertices 10 --edge-prob 0.3
-pred create MIS --random --num-vertices 100 --seed 42 -o big.json
-pred create MaxCut --random --num-vertices 20 --edge-prob 0.5 -o maxcut.json
-```
-
-Without `-o`, the problem JSON is printed to stdout, which can be piped to other commands:
-
-```bash
-pred create MIS --graph 0-1,1-2,2-3 | pred solve - # when an ILP reduction path exists
-pred create StringToStringCorrection --source-string "0,1,2,3,1,0" --target-string "0,1,3,2,1" --bound 2 | pred solve - --solver brute-force
-pred create MIS --random --num-vertices 10 | pred inspect -
-```
-
-The output file uses a standard wrapper format:
-
-```json
-{
- "type": "MaximumIndependentSet",
- "variant": {"graph": "SimpleGraph", "weight": "i32"},
- "data": { ... }
-}
-```
-
-#### Example: Bounded Component Spanning Forest
-
-`BoundedComponentSpanningForest` uses one component label per vertex in the
-evaluation config. If the graph has `n` vertices and limit `k`, then
-`--config` expects `n` comma-separated integers in `0..k-1`.
-
-```bash
-pred create BoundedComponentSpanningForest \
- --graph 0-1,1-2,2-3,3-4,4-5,5-6,6-7,0-7,1-5,2-6 \
- --weights 2,3,1,2,3,1,2,1 \
- --k 3 \
- --bound 6 \
- -o bcsf.json
-
-pred evaluate bcsf.json --config 0,0,1,1,1,2,2,0
-pred solve bcsf.json --solver brute-force
-```
-
-The brute-force solver is required here because this model does not yet have an
-ILP reduction path.
-
-### `pred evaluate` — Evaluate a configuration
-
-Evaluate a configuration against a problem instance:
-
-```text
-{{#include generated/pred-evaluate.txt}}
-```
-
-Stdin is supported with `-`:
-
-```bash
-pred create MIS --graph 0-1,1-2,2-3 | pred evaluate - --config 1,0,1,0
-```
-
-### `pred inspect` — Inspect a problem file
-
-Show a summary of what's inside a problem JSON or reduction bundle:
-
-```bash
-$ pred inspect problem.json
-Type: MaximumIndependentSet {graph=SimpleGraph, weight=i32}
-Size: 5 vertices, 5 edges
-```
-
-Works with reduction bundles and stdin:
-
-```bash
-pred inspect bundle.json
-pred create MIS --graph 0-1,1-2 | pred inspect -
-```
-
-### `pred reduce` — Reduce a problem
-
-Reduce a problem to a target type. Outputs a reduction bundle containing source, target, and path:
-
-```bash
-pred reduce problem.json --to QUBO -o reduced.json
-```
-
-Use a specific reduction path (from `pred path -o`). The target is inferred from the path file, so `--to` is not needed:
-
-```bash
-pred reduce problem.json --via path.json -o reduced.json
-```
-
-Stdin is supported with `-`:
-
-```bash
-pred create MIS --graph 0-1,1-2,2-3 | pred reduce - --to QUBO
-```
-
-The bundle contains everything needed to map solutions back:
-
-```json
-{
- "source": { "type": "MaximumIndependentSet", "variant": {...}, "data": {...} },
- "target": { "type": "QUBO", "variant": {...}, "data": {...} },
- "path": [
- {"name": "MaximumIndependentSet", "variant": {"graph": "SimpleGraph", "weight": "i32"}},
- {"name": "QUBO", "variant": {"weight": "f64"}}
- ]
-}
-```
-
-### `pred solve` — Solve a problem
-
-Solve a problem instance using ILP (default), brute-force, or the customized solver:
-
-```bash
-pred solve problem.json # ILP solver (default)
-pred solve problem.json --solver brute-force # brute-force solver
-pred solve problem.json --solver customized # structure-exploiting exact solver
-pred solve problem.json --timeout 30 # abort after 30 seconds
-```
-
-Stdin is supported with `-`:
-
-```bash
-pred create MIS --graph 0-1,1-2,2-3 | pred solve -
-pred create MIS --graph 0-1,1-2,2-3 | pred solve - --solver brute-force
-pred create MinMaxMulticenter --graph 0-1,1-2,2-3 --weights 1,1,1,1 --edge-weights 1,1,1 --k 2 | pred solve - --solver brute-force
-pred create TwoDimensionalConsecutiveSets --alphabet-size 6 --sets "0,1,2;3,4,5;1,3;2,4;0,5" | pred solve - --solver brute-force
-```
-
-Output is JSON. When the problem is not ILP, the solver automatically reduces it to ILP, solves, and maps the solution back:
-
-```json
-{{#include generated/pred-solve-ilp.txt}}
-```
-
-Solve a reduction bundle (from `pred reduce`):
-
-```json
-{{#include generated/pred-solve-bundle.txt}}
-```
-
-> **Note:** The ILP solver requires a reduction path from the target problem to ILP.
-> Some problems do not currently have one. Examples include BoundedComponentSpanningForest,
-> LengthBoundedDisjointPaths, MinimumCardinalityKey, QUBO, SpinGlass, MaxCut, CircuitSAT, MinMaxMulticenter, and MultiprocessorScheduling.
-> Use `pred solve --solver brute-force` for these, or reduce to a problem that supports ILP first.
-> For other problems, use `pred path ILP` to check whether an ILP reduction path exists.
-
-For example, the canonical Minimum Cardinality Key instance can be created and solved with:
-
-```bash
-pred create MinimumCardinalityKey --num-attributes 6 --dependencies "0,1>2;0,2>3;1,3>4;2,4>5" -o mck.json
-pred solve mck.json --solver brute-force
-```
-
-## Shell Completions
-
-Enable tab completion by adding one line to your shell config:
-
-```bash
-# bash (~/.bashrc)
-eval "$(pred completions bash)"
-
-# zsh (~/.zshrc)
-eval "$(pred completions zsh)"
-
-# fish (~/.config/fish/config.fish)
-pred completions fish | source
-```
-
-If the shell argument is omitted, `pred completions` auto-detects your current shell.
-
-## JSON Output
-
-All commands support `-o` to write JSON to a file and `--json` to print JSON to stdout:
-
-```bash
-pred list -o problems.json # save to file
-pred list --json # print JSON to stdout
-pred show MIS --json # works on any command
-pred path MIS QUBO --json
-pred solve problem.json --json
-```
-
-This is useful for scripting and piping:
-
-```bash
-pred list --json | jq '.variants[].name'
-pred path MIS QUBO --json | jq '.path'
-```
-
-## Problem Name Aliases
-
-You can use short aliases instead of full problem names (shown in `pred list`):
-
-{{#include generated/pred-aliases.txt}}
-
-You can also specify variants with a slash: `MIS/UnitDiskGraph`, `SpinGlass/SimpleGraph`.
-
-When a bare name (no slash) is used in commands like `path`, `to`, `from`, `create`, or `reduce`, it resolves to the **declared default variant** for that problem type. For example, `MIS` resolves to `MaximumIndependentSet/SimpleGraph/One`.
-
-If you mistype a problem name, `pred` will suggest the closest match:
-
-```text
-{{#include generated/pred-show-typo.txt}}
-```
+Next: [watch the full run](cli-demo.md), [inspect the path](cli-paths.md), or [save a reduction bundle](cli-reduce.md).
diff --git a/docs/src/contributing.md b/docs/src/contributing.md
new file mode 100644
index 000000000..1c7eaa2ae
--- /dev/null
+++ b/docs/src/contributing.md
@@ -0,0 +1,15 @@
+# Contributing
+
+Propose a model or reduction through the [agent proposal workflow](agent-propose.md), or use the repository's [issue templates](https://github.com/CodingThrust/problem-reductions/issues/new/choose).
+
+For implementation, read [AGENTS.md](https://github.com/CodingThrust/problem-reductions/blob/main/AGENTS.md) and the canonical `.claude/CLAUDE.md` instructions. Model and rule skills describe required code, tests, examples, and mathematical documentation.
+
+## What a rule contributes
+
+A useful rule includes exact endpoint variants, a construction, solution or value extraction, a correctness argument, and overhead metadata. Closed-loop tests and independently checked examples provide concrete evidence alongside the proof.
+
+## Authorship and license
+
+The project's authorship policy adds contributors of 10 non-trivial reduction rules to the [paper](reductions.pdf). The software is MIT licensed.
+
+Next: [implement and review](agent-pipeline.md).
diff --git a/docs/src/design-paths.md b/docs/src/design-paths.md
new file mode 100644
index 000000000..101cde4c6
--- /dev/null
+++ b/docs/src/design-paths.md
@@ -0,0 +1,32 @@
+# Path costs and overhead
+
+`ReductionGraph` searches a directed graph of exact `(name, variant)` pairs. Registered reductions carry capabilities; natural variant connections reflect graph and weight subtype relations.
+
+## Choose a cost
+
+| Cost | Purpose |
+|---|---|
+| `MinimizeSteps` | Fewest reduction steps |
+| `Minimize("field")` | Cost based on an output size field |
+| `CustomCost(closure)` | User-defined edge cost from overhead and current size |
+
+`find_cheapest_path` accepts source/target variant maps, an input `ProblemSize`, and a cost function. `find_all_paths` enumerates simple paths. Use bounded enumeration when exploring a large graph.
+
+## Interpret an overhead
+
+```rust,ignore
+#[reduction(overhead = {
+ num_vars = "num_vertices + num_edges",
+ num_clauses = "3 * num_edges",
+})]
+```
+
+Expressions refer to getters on the source type. The macro validates those names at compile time. The metadata describes scaling bounds; it does not promise exact target counts for each input.
+
+For a concrete instance, inspect the constructed target. For a chain, `path_overheads` returns each edge's expressions and `compose_path_overhead` substitutes them to obtain an end-to-end bound.
+
+## Keep costs separate from solve time
+
+A shorter route can produce a harder target. Compare target sizes and solver measurements as well as hop counts; do not present symbolic overheads as measured runtime.
+
+Next: [execute a path](rust-paths.md) or [download the graph](reductions/reduction_graph.json).
diff --git a/docs/src/design-problem.md b/docs/src/design-problem.md
new file mode 100644
index 000000000..1e5b25ca3
--- /dev/null
+++ b/docs/src/design-problem.md
@@ -0,0 +1,23 @@
+# Problem contract
+
+Every problem implements `Problem`. The associated `Value` type is the per-configuration aggregate returned by `evaluate()`. Solvers fold these values across the configuration space, and witness-capable aggregates can also recover representative configurations.
+
+```rust,ignore
+trait Problem {
+ const NAME: &'static str; // e.g., "MaximumIndependentSet"
+ type Value: Clone; // e.g., Max, Or, Sum
+ fn dims(&self) -> Vec; // config space per variable
+ fn evaluate(&self, config: &[usize]) -> Self::Value;
+ fn variant() -> Vec<(&'static str, &'static str)>; // e.g., [("graph", "SimpleGraph"), ("weight", "i32")]
+ fn num_variables(&self) -> usize; // default: dims().len()
+ fn problem_type() -> ProblemType; // default: registry lookup by NAME
+}
+```
+
+- **`Problem`** — the base trait. Every problem declares a `NAME` (e.g., `"MaximumIndependentSet"`). The solver explores the configuration space defined by `dims()` and scores each configuration with `evaluate()`. For example, a 4-vertex MIS has `dims() = [2, 2, 2, 2]` (each vertex is selected or not); `evaluate(&[1, 0, 1, 0])` returns `Max(Some(2))` if vertices 0 and 2 form an independent set, or `Max(None)` if they share an edge. Each problem also provides inherent getter methods (e.g., `num_vertices()`, `num_edges()`) used by reduction overhead expressions.
+- **Witness-capable objective problems** — typically use `Max`, `Min`, or `Extremum` as `Value`.
+- **Witness-capable feasibility problems** — typically use `Or`.
+- **Aggregate-only problems** — use fold values such as `Sum` or `And`; these solve to a value but do not admit representative witness configurations.
+- **Common aggregate wrappers** — `Max`, `Min`, `Sum`, `Or`, `And`, `Extremum`, `ExtremumSense`.
+
+Next: [variant registration](design-variant-registration.md).
diff --git a/docs/src/design-reductions.md b/docs/src/design-reductions.md
new file mode 100644
index 000000000..4141a9757
--- /dev/null
+++ b/docs/src/design-reductions.md
@@ -0,0 +1,36 @@
+# Reduction contracts
+
+A reduction connects exact source and target variants. Its contract determines how a result can be recovered.
+
+| Capability | Contract | Example |
+|---|---|---|
+| Witness | `ReduceTo` and `ReductionResult::extract_solution` | Solve a target, recover a source configuration |
+| Aggregate | `ReduceToAggregate` and `AggregateReductionResult::extract_value` | Solve a target value, recover a source value |
+| Turing | Multiple target queries | Optimize by querying a decision problem at several bounds |
+
+Search defaults to witness mode. Use `ReductionMode::Aggregate` or `ReductionMode::Turing` for the corresponding graph queries; do not replay those edges as a single witness mapping.
+
+## Register a witness reduction
+
+```rust,ignore
+#[reduction(overhead = {
+ num_vertices = "num_vertices",
+ num_edges = "num_edges",
+})]
+impl ReduceTo>
+ for MaximumIndependentSet
+{
+ // Provide Result and reduce_to(); the result owns the target
+ // and maps a vertex-cover witness to its independent-set complement.
+}
+```
+
+This is a schematic declaration. Read a [complete implementation](https://github.com/CodingThrust/problem-reductions/blob/main/src/rules/maximumindependentset_minimumvertexcover.rs) for the result type and constructor.
+
+The attribute requires overhead metadata and registers witness/configuration reductions. Aggregate and Turing edges currently use manual `ReductionEntry` registration. Keep one primitive registration for each exact endpoint pair.
+
+## Check correctness
+
+Prove that the construction and extraction preserve the required result. For a small witness example, solve source and target independently, extract the target solution, and compare its source evaluation with the direct optimum.
+
+Next: [overhead semantics](design-paths.md) or [implementation workflow](agent-pipeline.md).
diff --git a/docs/src/design-serialization.md b/docs/src/design-serialization.md
new file mode 100644
index 000000000..53f314ca5
--- /dev/null
+++ b/docs/src/design-serialization.md
@@ -0,0 +1,14 @@
+# JSON serialization
+
+All problem types support JSON serialization via serde:
+
+```rust,ignore
+use problemreductions::io::{to_json, from_json};
+
+let json: String = to_json(&problem)?;
+let restored: MaximumIndependentSet = from_json(&json)?;
+```
+
+These helpers serialize typed Rust problem data. The CLI additionally wraps data with `type` and `variant` for dynamic loading. Keep that wrapper when passing files between CLI commands.
+
+Next: [CLI JSON and automation](cli-automation.md).
diff --git a/docs/src/design-variant-registration.md b/docs/src/design-variant-registration.md
new file mode 100644
index 000000000..851429d43
--- /dev/null
+++ b/docs/src/design-variant-registration.md
@@ -0,0 +1,66 @@
+# Register variants
+
+## VariantParam trait
+
+Each variant parameter type implements `VariantParam`, which declares its category, value, and optional parent:
+
+```rust,ignore
+pub trait VariantParam: 'static {
+ const CATEGORY: &'static str; // e.g., "graph", "weight", "k"
+ const VALUE: &'static str; // e.g., "SimpleGraph", "i32"
+ const PARENT_VALUE: Option<&'static str>; // None for root types
+}
+```
+
+Types with a parent also implement `CastToParent`, providing the runtime conversion for variant casts:
+
+```rust,ignore
+pub trait CastToParent: VariantParam {
+ type Parent: VariantParam;
+ fn cast_to_parent(&self) -> Self::Parent;
+}
+```
+
+## Registration with `impl_variant_param!`
+
+The `impl_variant_param!` macro implements `VariantParam` (and optionally `CastToParent` / `KValue`) for a type:
+
+```rust,ignore
+// Root type (no parent):
+impl_variant_param!(SimpleGraph, "graph");
+
+// K root (arbitrary K):
+impl_variant_param!(KN, "k", k: None);
+
+// Specific K with parent:
+impl_variant_param!(K3, "k", parent: KN, cast: |_| KN, k: Some(3));
+```
+
+## Variant cast reductions with `impl_variant_reduction!`
+
+When a more specific variant needs to be treated as a less specific one, an explicit variant cast reduction is declared:
+
+```rust,ignore
+impl_variant_reduction!(
+ MaximumIndependentSet,
+ => ,
+ fields: [num_vertices, num_edges],
+ |src| MaximumIndependentSet::new(
+ src.graph().cast_to_parent(), src.weights().to_vec())
+);
+```
+
+## Composing `Problem::variant()`
+
+The `variant_params!` macro composes the `Problem::variant()` body from type parameter names:
+
+```rust,ignore
+// MaximumIndependentSet
+fn variant() -> Vec<(&'static str, &'static str)> {
+ crate::variant_params![G, W]
+ // e.g., MaximumIndependentSet
+ // -> vec![("graph", "UnitDiskGraph"), ("weight", "One")]
+}
+```
+
+Use `declare_variants!` in the model file to register concrete types and their dynamic load/serialize/solve metadata. See existing models and the [repository instructions](https://github.com/CodingThrust/problem-reductions/blob/main/.claude/CLAUDE.md) for the current macro contract.
diff --git a/docs/src/design-variants.md b/docs/src/design-variants.md
new file mode 100644
index 000000000..d177566a3
--- /dev/null
+++ b/docs/src/design-variants.md
@@ -0,0 +1,33 @@
+# Variant system
+
+A single problem name like `MaximumIndependentSet` can have multiple **variants** — carrying weights on vertices, or defined on a restricted topology (e.g., king's subgraph). Variants form a subtype hierarchy: independent sets on king's subgraphs are a subset of independent sets on unit-disk graphs. The reduction from a more specific variant to a less specific one is a **variant cast** — an identity mapping where indices are preserved.
+
+
+
+Variant types fall into three categories:
+
+- **Graph type** — `SimpleGraph` (root), `PlanarGraph`, `BipartiteGraph`, `UnitDiskGraph`, `KingsSubgraph`, `TriangularSubgraph`.
+- **Weight type** — `One` (unweighted), `i32`, `f64`.
+- **K value** — e.g., `K3` for 3-SAT, `KN` for arbitrary K.
+
+
+
+
+
+
+
+
+
+
+
+
+Next: [register variants](design-variant-registration.md).
diff --git a/docs/src/design.md b/docs/src/design.md
index 7f709edfc..203d7e52c 100644
--- a/docs/src/design.md
+++ b/docs/src/design.md
@@ -1,10 +1,19 @@
-# Design
+# Architecture
-This guide covers the library internals for contributors.
+The Rust library stores problem definitions, executable reductions, and their registry metadata. The CLI and MCP server expose that core to tools and agents.
-## Module Architecture
+| Location | Responsibility |
+|---|---|
+| `src/models/` | Models grouped by graph, formula, set, algebraic, or miscellaneous input |
+| `src/rules/` | Reduction implementations and solution/value mappings |
+| `src/registry/` | Concrete variant metadata and dynamic dispatch |
+| `src/solvers/` | Exhaustive, ILP, specialized, and decision-search solvers |
+| `problemreductions-cli/` | CLI and optional MCP server |
+| `src/example_db/` | Canonical model and rule examples |
+| `src/unit_tests/` | Tests mirroring the source tree |
+
+## Module map
-
@@ -23,317 +32,4 @@ This guide covers the library internals for contributors.
-## Problem Model
-
-Every problem implements `Problem`. The associated `Value` type is the per-configuration aggregate returned by `evaluate()`. Solvers fold these values across the configuration space, and witness-capable aggregates can also recover representative configurations.
-
-```rust,ignore
-trait Problem: Clone {
- const NAME: &'static str; // e.g., "MaximumIndependentSet"
- type Value: Clone; // e.g., Max, Or, Sum
- fn dims(&self) -> Vec; // config space per variable
- fn evaluate(&self, config: &[usize]) -> Self::Value;
- fn variant() -> Vec<(&'static str, &'static str)>; // e.g., [("graph", "SimpleGraph"), ("weight", "i32")]
- fn num_variables(&self) -> usize; // default: dims().len()
- fn problem_type() -> ProblemType; // default: registry lookup by NAME
-}
-```
-
-- **`Problem`** — the base trait. Every problem declares a `NAME` (e.g., `"MaximumIndependentSet"`). The solver explores the configuration space defined by `dims()` and scores each configuration with `evaluate()`. For example, a 4-vertex MIS has `dims() = [2, 2, 2, 2]` (each vertex is selected or not); `evaluate(&[1, 0, 1, 0])` returns `Max(Some(2))` if vertices 0 and 2 form an independent set, or `Max(None)` if they share an edge. Each problem also provides inherent getter methods (e.g., `num_vertices()`, `num_edges()`) used by reduction overhead expressions.
-- **Witness-capable objective problems** — typically use `Max`, `Min`, or `Extremum` as `Value`.
-- **Witness-capable feasibility problems** — typically use `Or`.
-- **Aggregate-only problems** — use fold values such as `Sum` or `And`; these solve to a value but do not admit representative witness configurations.
-- **Common aggregate wrappers** — `Max`, `Min`, `Sum`, `Or`, `And`, `Extremum`, `ExtremumSense`.
-
-## Variant System
-
-A single problem name like `MaximumIndependentSet` can have multiple **variants** — carrying weights on vertices, or defined on a restricted topology (e.g., king's subgraph). Variants form a subtype hierarchy: independent sets on king's subgraphs are a subset of independent sets on unit-disk graphs. The reduction from a more specific variant to a less specific one is a **variant cast** — an identity mapping where indices are preserved.
-
-
-
-Variant types fall into three categories:
-
-- **Graph type** — `SimpleGraph` (root), `PlanarGraph`, `BipartiteGraph`, `UnitDiskGraph`, `KingsSubgraph`, `TriangularSubgraph`.
-- **Weight type** — `One` (unweighted), `i32`, `f64`.
-- **K value** — e.g., `K3` for 3-SAT, `KN` for arbitrary K.
-
-
-
-
-
-
-
-
-
-
-
-
-
-Implementation details: VariantParam trait and macros
-
-### VariantParam trait
-
-Each variant parameter type implements `VariantParam`, which declares its category, value, and optional parent:
-
-```rust,ignore
-pub trait VariantParam: 'static {
- const CATEGORY: &'static str; // e.g., "graph", "weight", "k"
- const VALUE: &'static str; // e.g., "SimpleGraph", "i32"
- const PARENT_VALUE: Option<&'static str>; // None for root types
-}
-```
-
-Types with a parent also implement `CastToParent`, providing the runtime conversion for variant casts:
-
-```rust,ignore
-pub trait CastToParent: VariantParam {
- type Parent: VariantParam;
- fn cast_to_parent(&self) -> Self::Parent;
-}
-```
-
-### Registration with `impl_variant_param!`
-
-The `impl_variant_param!` macro implements `VariantParam` (and optionally `CastToParent` / `KValue`) for a type:
-
-```rust,ignore
-// Root type (no parent):
-impl_variant_param!(SimpleGraph, "graph");
-
-// K root (arbitrary K):
-impl_variant_param!(KN, "k", k: None);
-
-// Specific K with parent:
-impl_variant_param!(K3, "k", parent: KN, cast: |_| KN, k: Some(3));
-```
-
-### Variant cast reductions with `impl_variant_reduction!`
-
-When a more specific variant needs to be treated as a less specific one, an explicit variant cast reduction is declared:
-
-```rust,ignore
-impl_variant_reduction!(
- MaximumIndependentSet,
- => ,
- fields: [num_vertices, num_edges],
- |src| MaximumIndependentSet::new(
- src.graph().cast_to_parent(), src.weights().to_vec())
-);
-```
-
-### Composing `Problem::variant()`
-
-The `variant_params!` macro composes the `Problem::variant()` body from type parameter names:
-
-```rust,ignore
-// MaximumIndependentSet
-fn variant() -> Vec<(&'static str, &'static str)> {
- crate::variant_params![G, W]
- // e.g., MaximumIndependentSet
- // -> vec![("graph", "UnitDiskGraph"), ("weight", "One")]
-}
-```
-
-
-
-## Reduction Rules
-
-A reduction requires two pieces: a **result struct** and a **`ReduceTo` impl**.
-
-The result struct holds the target problem and the logic to map solutions back:
-
-```rust,ignore
-#[derive(Debug, Clone)]
-pub struct ReductionISToVC {
- target: MinimumVertexCover,
-}
-
-impl ReductionResult for ReductionISToVC {
- type Source = MaximumIndependentSet;
- type Target = MinimumVertexCover;
-
- fn target_problem(&self) -> &Self::Target { &self.target }
- fn extract_solution(&self, target_sol: &[usize]) -> Vec {
- target_sol.iter().map(|&x| 1 - x).collect() // complement
- }
-}
-```
-
-The `#[reduction]` attribute on the `ReduceTo` impl registers the reduction in the global registry (via `inventory`):
-
-```rust,ignore
-#[reduction(overhead = {
- num_vertices = "num_vertices",
- num_edges = "num_edges",
-})]
-impl ReduceTo>
- for MaximumIndependentSet
-{
- type Result = ReductionISToVC;
- fn reduce_to(&self) -> Self::Result { /* ... */ }
-}
-```
-
-
-What the #[reduction] macro generates
-
-The `#[reduction]` attribute expands to the original `impl` block plus an `inventory::submit!` call:
-
-```rust,ignore
-inventory::submit! {
- ReductionEntry {
- source_name: "MaximumIndependentSet",
- target_name: "MinimumVertexCover",
- source_variant_fn: || as Problem>::variant(),
- target_variant_fn: || as Problem>::variant(),
- overhead_fn: || ReductionOverhead {
- output_size: vec![
- ("num_vertices", Expr::Var("num_vertices")),
- ("num_edges", Expr::Var("num_edges")),
- ],
- },
- module_path: module_path!(),
- reduce_fn: |src: &dyn Any| -> Box {
- let src = src.downcast_ref::>().unwrap();
- Box::new(ReduceTo::>::reduce_to(src))
- },
- }
-}
-```
-
-Each `ReductionEntry` is collected by `inventory` at link time and iterated at runtime, making every reduction discoverable by `ReductionGraph` without manual registration. The `reduce_fn` field provides a type-erased executor that enables dynamically discovered paths to chain reductions automatically.
-
-
-
-## Reduction Graph
-
-`ReductionGraph::new()` iterates all registered `ReductionEntry` items (via `inventory`) and builds a variant-level directed graph:
-
-- **Nodes** are unique `(problem_name, variant)` pairs — e.g., `("MaximumIndependentSet", {graph: "KingsSubgraph", weight: "i32"})`.
-- **Edges** come exclusively from `#[reduction]` registrations — both cross-problem reductions and variant casts. There are no auto-generated edges.
-
-Exported files:
-
-- [reduction_graph.json](reductions/reduction_graph.json) — all problem variants and reduction edges
-- [problem_schemas.json](reductions/problem_schemas.json) — field definitions for each problem type
-
-These JSON assets are generated during `make doc`, `make mdbook`, and `make paper`; they are build artifacts, not committed source files.
-Generate them manually with `cargo run --example export_graph` and `cargo run --example export_schemas` when you need the raw exports locally.
-
-### Path finding
-
-All path-finding operates on **exact variant nodes**. Use `ReductionGraph::variant_to_map(&T::variant())` to convert a `Problem::variant()` into the required `BTreeMap`.
-
-| Method | Algorithm | Use case |
-|--------|-----------|----------|
-| `find_cheapest_path(src, src_var, dst, dst_var, input_size, cost_fn)` | Dijkstra | Optimal path under a cost function |
-| `find_all_paths(src, src_var, dst, dst_var)` | All simple paths | Enumerate every route |
-
-Use `find_cheapest_path` with `MinimizeSteps` for fewest-hops search.
-
-The `PathCostFn` trait (used by `find_cheapest_path`) computes edge cost from overhead and current problem size:
-
-| Cost function | Strategy |
-|--------------|----------|
-| `MinimizeSteps` | Minimize number of hops (unit edge cost) |
-| `Minimize("field")` | Minimize a single output field (e.g., `Minimize("num_variables")`) |
-| `CustomCost(closure)` | User-defined: `\|overhead: &ReductionOverhead, size: &ProblemSize\| -> f64` |
-
-`CustomCost` wraps a closure that receives the edge's `ReductionOverhead` (polynomial mapping from input to output size fields) and the current `ProblemSize` (accumulated field values at that point in the path), and returns an `f64` edge cost. Dijkstra minimizes the total cost along the path.
-
-**Example:** Finding a path from `MIS{KingsSubgraph, i32}` to `VC{SimpleGraph, i32}`:
-
-```
-MIS{KingsSubgraph,i32} -> MIS{UnitDiskGraph,i32} -> MIS{SimpleGraph,i32} -> VC{SimpleGraph,i32}
- variant cast variant cast reduction
-```
-
-### Executable paths
-
-Convert a `ReductionPath` into a typed `ExecutablePath` via `make_executable()`, then call `reduce()`:
-
-```rust,ignore
-// find_cheapest_path returns a ReductionPath (list of variant node IDs)
-let rpath = graph.find_cheapest_path("Factoring", &src_var,
- "SpinGlass", &dst_var, &ProblemSize::new(vec![]), &MinimizeSteps).unwrap();
-
-// make_executable converts it into a typed, callable chain
-let path = graph.make_executable::>(&rpath).unwrap();
-
-// reduce() applies each step, returning a ChainedReduction
-let reduction = path.reduce(&factoring_instance);
-let target: &SpinGlass = reduction.target_problem();
-let solution: Vec = reduction.extract_solution(&target_solution);
-```
-
-`ExecutablePath` holds a type-erased `ReduceFn` per edge. `reduce()` applies them sequentially, producing a `ChainedReduction` that stores each intermediate result. `extract_solution` maps the final solution back through the chain in reverse order.
-
-For full type control, you can also chain `ReduceTo::reduce_to()` calls manually at each step.
-
-
-Overhead evaluation
-
-Each reduction declares how the output problem size relates to the input, expressed as symbolic `Expr` expressions. The `#[reduction]` macro parses overhead strings at compile time:
-
-```rust,ignore
-#[reduction(overhead = {
- num_vars = "num_vertices + num_edges",
- num_clauses = "3 * num_edges",
-})]
-impl ReduceTo for Source { ... }
-```
-
-Expressions support: constants, variables, `+`, `*`, `^`, `exp()`, `log()`, `sqrt()`. Each problem type provides inherent getter methods (e.g., `num_vertices()`, `num_edges()`) that the overhead expressions reference.
-
-`evaluate_output_size(input)` substitutes input values:
-
-```
-Input: ProblemSize { num_vertices: 10, num_edges: 15 }
-Output: ProblemSize { num_vars: 25, num_clauses: 45 }
-```
-
-For multi-step paths, overhead composes: the output of step N becomes the input of step N+1. Variant cast edges use `ReductionOverhead::identity()`, passing through all fields unchanged.
-
-
-
-## Solvers
-
-Solvers implement the `Solver` trait:
-
-```rust,ignore
-pub trait Solver {
- fn solve
(&self, problem: &P) -> P::Value
- where
- P: Problem,
- P::Value: Aggregate;
-}
-```
-
-| Solver | Description |
-|--------|-------------|
-| **BruteForce** | Enumerates all configurations. `solve()` works for any aggregate problem; `find_witness()`, `find_all_witnesses()`, and `solve_with_witnesses()` are available when `P::Value` supports witnesses. Used for testing and verification. |
-| **ILPSolver** | Enabled by default. Solves ILP instances directly with HiGHS via `good_lp`. Also provides `solve_reduced()` for witness-capable problems that implement `ReduceTo>`. |
-
-## JSON Serialization
-
-All problem types support JSON serialization via serde:
-
-```rust,ignore
-use problemreductions::io::{to_json, from_json};
-
-let json: String = to_json(&problem)?;
-let restored: MaximumIndependentSet = from_json(&json)?;
-```
-
-## Contributing
-
-See [Call for Contributions](./introduction.md#call-for-contributions) for the recommended issue-based workflow (no coding required).
+Read the [problem contract](design-problem.md), [reduction contracts](design-reductions.md), and [variant system](design-variants.md) before extending the library.
diff --git a/docs/src/getting-started.md b/docs/src/getting-started.md
index 5afc10916..06f077157 100644
--- a/docs/src/getting-started.md
+++ b/docs/src/getting-started.md
@@ -1,206 +1,28 @@
-# Getting Started
+# First Rust program
-## What This Library Does
-
-**problem-reductions** transforms hard computational problems into forms that efficient solvers can handle. You define a problem, reduce it to another problem type (like QUBO or ILP), solve the reduced problem, and extract the solution back. The [interactive reduction graph](./introduction.html) shows all available problem types and transformations.
-
-## Installation
+Add the library to a Rust project:
```bash
cargo add problemreductions
```
-## The Reduction Workflow
-
-The core workflow is: **create** a problem, **reduce** it to a target, **solve** the target, and **extract** the solution back.
-
-
-
-### Example 1: Direct reduction — Set Packing to ILP
+## Solve a small set-packing instance
-Reduce Maximum Set Packing to Integer Linear Programming (ILP), solve with the
-ILP solver, and extract the solution back.
-
-#### Step 1 — Create the source problem
-
-A small set system with pairwise overlaps gives a direct binary ILP.
-
-```rust,ignore
+```rust
use problemreductions::prelude::*;
-use problemreductions::models::algebraic::ILP;
-use problemreductions::solvers::ILPSolver;
-
-let problem = MaximumSetPacking::::new(vec![
- vec![0, 1],
- vec![1, 2],
- vec![2, 3],
- vec![4, 5],
-]);
-```
-
-#### Step 2 — Reduce to ILP
-
-`ReduceTo` applies a single-step reduction. The result holds the target
-problem and knows how to map solutions back. The ILP formulation introduces
-binary variable x_i for each set, constraint x_i + x_j ≤ 1 for each
-overlapping pair, and maximizes the weighted sum.
-
-```rust,ignore
-let reduction = ReduceTo::::reduce_to(&problem);
-let ilp = reduction.target_problem();
-println!("ILP: {} variables, {} constraints", ilp.num_vars, ilp.constraints.len());
-```
-
-```text
-ILP: 4 variables, 2 constraints
-```
-
-#### Step 3 — Solve the ILP
-
-`ILPSolver` uses the HiGHS solver to find optimal solutions efficiently.
-For small instances you can also use `BruteForce`, but `ILPSolver` scales
-to much larger problems.
-
-```rust,ignore
-let solver = ILPSolver::new();
-let ilp_solution = solver.solve(ilp).unwrap();
-println!("ILP solution: {:?}", ilp_solution);
-```
-
-```text
-ILP solution: [1, 0, 1, 0]
-```
-
-#### Step 4 — Extract and verify
-
-`extract_solution` maps the ILP solution back to the original problem's
-configuration space.
-
-```rust,ignore
-let solution = reduction.extract_solution(&ilp_solution);
-let metric = problem.evaluate(&solution);
-println!("Packing solution: {:?} -> size {}", solution, metric);
-assert!(metric.is_valid());
-```
-
-```text
-Packing solution: [1, 0, 1, 1] -> size Max(3)
-```
-
-For convenience, `ILPSolver::solve_reduced` combines reduce + solve + extract
-in a single call:
-
-```rust,ignore
-let solution = ILPSolver::new().solve_reduced(&problem).unwrap();
-assert!(problem.evaluate(&solution).is_valid());
-```
-
-### 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. ([full source](https://github.com/CodingThrust/problem-reductions/blob/main/examples/chained_reduction_factoring_to_spinglass.rs))
-
-Let's walk through each step.
-
-#### Step 1 — Discover the reduction path
-
-`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_factoring_to_spinglass.rs:step1}}
-```
-
-```text
-{{#include generated/factoring-path.txt}}
-```
-
-#### 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**.
-
-```rust,ignore
-{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:step2}}
-```
-
-#### Step 3 — Solve with ILPSolver
-
-`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}}
+fn main() {
+ let problem = MaximumSetPacking::::new(vec![
+ vec![0, 1], vec![1, 2], vec![2, 3], vec![4, 5],
+ ]);
+ let solver = BruteForce::new();
+ let solution = solver.find_witness(&problem).unwrap();
+ println!("{:?}: {}", solution, problem.evaluate(&solution));
+}
```
-```text
-{{#include generated/factoring-result.txt}}
-```
-
-#### 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
-{{#include generated/factoring-overhead.txt}}
-```
-
-## Solvers
-
-Three solvers are available:
-
-| Solver | Use Case | Notes |
-|--------|----------|-------|
-| [`BruteForce`](api/problemreductions/solvers/struct.BruteForce.html) | Small instances (<20 variables) | Enumerates all configurations |
-| [`ILPSolver`](api/problemreductions/solvers/ilp/struct.ILPSolver.html) | Larger instances | Enabled by default (`ilp` feature) |
-| [`CustomizedSolver`](api/problemreductions/solvers/customized/struct.CustomizedSolver.html) | Structure-exploiting | Uses problem-specific exact algorithms |
-
-ILP support is enabled by default. To disable it:
-
-```bash
-cargo add problemreductions --no-default-features
-```
-
-## JSON Resources
-
-The library exports machine-readable metadata useful for tooling and research:
-
-These files are generated when you build the docs locally.
-- [reduction_graph.json](reductions/reduction_graph.json) lists all problem variants and reduction edges
-- [problem_schemas.json](reductions/problem_schemas.json) lists field definitions for each problem type
-
+The optimal packing selects sets 0, 2, and 3 and evaluates to `Max(3)`. The witness vector is `[1,0,1,1]`.
-## Next Steps
+`Problem::evaluate` checks a configuration; `BruteForce` enumerates the configuration space to find an optimum. Keep exhaustive examples small.
-- Try the [CLI tool](./cli.md) to explore problems and reduction paths from your terminal
-- Explore the [interactive reduction graph](./introduction.html) to discover available reductions
-- Read the [Design](./design.md) guide for implementation details
-- Browse the [API Reference](./api.html) for full documentation
+Next: [apply an ILP reduction](rust-reduction.md) or [read solver contracts](rust-solvers.md).
diff --git a/docs/src/install.md b/docs/src/install.md
new file mode 100644
index 000000000..11db6abd4
--- /dev/null
+++ b/docs/src/install.md
@@ -0,0 +1,29 @@
+# Install the CLI
+
+The `pred` executable explores models and reductions, creates instances, and runs solvers.
+
+## Install a release
+
+```bash
+cargo install problemreductions-cli
+pred --version
+```
+
+Rust and a native build toolchain are required. The default solver backend is HiGHS.
+
+## Build the current repository
+
+```bash
+git clone https://github.com/CodingThrust/problem-reductions
+cd problem-reductions
+cargo install --path problemreductions-cli
+pred --version
+```
+
+The website catalog is built from the repository. A published crate may have fewer models or rules; use the source build when reproducing current catalog entries.
+
+## Optional features
+
+For the MCP server, install with `--features mcp`. The CLI also exposes `cplex` and `lp-solvers` for separately installed solver backends; consult the [CLI manifest](https://github.com/CodingThrust/problem-reductions/blob/main/problemreductions-cli/Cargo.toml) before configuring one.
+
+Next: [first solve](cli.md) or [connect with MCP](mcp.md).
diff --git a/docs/src/introduction.md b/docs/src/introduction.md
index 8b79aaff7..85eee55a6 100644
--- a/docs/src/introduction.md
+++ b/docs/src/introduction.md
@@ -1,81 +1,29 @@
-# Problem Reductions
+# Documentation
-**problem-reductions** is a rust library that provides implementations of various computational hard problems and reduction rules between them. It is designed for algorithm research, education, and industry applications.
+Use executable reductions to connect a hard problem to a solver. Explore the catalog, transform an instance, and check the recovered solution. These guides are organized around small tasks for agents and their operators.
-## Reduction Graph
+## See what works
-
+[Watch the CLI solve a graph problem →](cli-demo.md)
-
-
-
-
-
-
- Graph
- Formula
- Set
- Algebraic
- Misc
- Variant Cast
-
-
- Click a node to start path selection
-
-
-
-
-
- Click a problem node to expand/collapse its variants.
- Click a variant to filter its edges.
- Click two nodes to find a reduction path.
- Double-click for API docs (nodes) or source code (edges).
- Scroll to zoom, drag to pan.
-
-
+A real terminal run: discover a route, reduce to ILP, recover an independent set, and cross-check the optimum. Six commands, about half a minute.
-You can also explore this graph from the terminal with the [CLI tool](./cli.md). For theoretical background and correctness proofs, see the [PDF manual](https://codingthrust.github.io/problem-reductions/reductions.pdf).
+## Choose a task
-## Our Vision
+| You have… | Start here | You get… |
+|---|---|---|
+| A problem to solve | [Find a solver](agent-find-solver.md) | A model, reduction route, and solver recommendation |
+| A solver to reuse | [Extend its reach](agent-find-problem.md) | Reachable source problems and size overheads |
+| A candidate connection | [Propose a model or rule](agent-propose.md) | A precise research proposal |
+| An approved issue | [Implement and review](agent-pipeline.md) | A tested implementation for review |
+| An instance to run | [First solve](cli.md) | A solution checked against the original problem |
-Computational complexity theory has produced a rich body of polynomial-time reductions between NP-hard problems, yet these results largely remain confined to papers. The gap between theoretical algorithms and working software leads to two persistent inefficiencies:
+## Give an agent the right context
-- **Solver underutilization.** State-of-the-art solvers (SAT solvers, ILP solvers, QUBO annealers) each target a single problem formulation. In principle, any problem reducible to that formulation can leverage the same solver — but without a systematic reduction library, practitioners must re-derive and re-implement each transformation.
-- **Redundant effort.** Problems that are polynomial-time equivalent are, from a computational standpoint, interchangeable. Without infrastructure connecting them, the same algorithmic insights are independently reimplemented across domains.
+Start with [agent setup](skills.md). Every page has a **Markdown** link for direct reading; the [Markdown index](markdown/index.md) lists all tasks. Use [JSON exports](cli-automation.md) for registry data and [MCP](mcp.md) for tool access.
-Our goal is to build a comprehensive, machine-readable reduction graph: a directed graph in which every node is a computational problem and every edge is a verified polynomial-time reduction. Given such a graph, one can automatically compose reduction paths to route any source problem to any reachable target solver.
+## Research scope
-A key enabler is AI-assisted implementation. We propose a pipeline of `algorithm → paper → software`, in which AI agents translate published reduction proofs into tested code. The critical question — can AI-generated reductions be trusted? — has a concrete answer: nearly all reductions admit **closed-loop verification**. A round-trip test reduces a source instance to a target, solves the target, extracts the solution back, and checks it against a direct solve of the source. This property makes correctness mechanically verifiable, independent of how the code was produced.
+The long-term goal is autonomous discovery of new reduction rules. Today, this repository provides executable models, registered reductions, solver routing, and agent workflows for proposals, implementation, and review. A candidate rule needs a mathematical argument as well as tests; passing finite examples does not establish a general proof.
-
-
-
-
-
-
-
-
-
-
-
-This library is the foundation of that effort: an open-source, extensible reduction graph with verified implementations, designed for contributions from both human researchers and AI agents.
-
-## Call for Contributions
-
-> **No programming experience required.** You contribute domain knowledge — we handle the implementation.
-
-### How it works
-
-1. **File an issue** — use the [Problem](https://github.com/CodingThrust/problem-reductions/issues/new?template=problem.md) or [Rule](https://github.com/CodingThrust/problem-reductions/issues/new?template=rule.md) template. Describe the problem or reduction you have in mind; the template guides you through the details.
-2. **We implement it** — for reasonable requests, maintainers tag the issue `implement` and AI agents generate a tested implementation.
-3. **We present it to you** — all issue contributors are invited to community calls (via [Zulip](https://problem-reductions.zulipchat.com/)), where maintainers walk through the implementation — documentation, CLI behavior, correctness — and you provide feedback.
-
-### Authorship
-
-Contribute 10 non-trivial reduction rules and you'll be added to the author list of the [paper](https://codingthrust.github.io/problem-reductions/reductions.pdf).
-
-For manual implementation, see the [Design](./design.md#contributing) guide.
-
-## License
-
-MIT License
+[Explore the atlas](index.html#atlas) · [Read the mathematical manual](reductions.pdf) · [Browse the Rust API](api.md)
diff --git a/docs/src/mcp-tools.md b/docs/src/mcp-tools.md
new file mode 100644
index 000000000..a61dd8044
--- /dev/null
+++ b/docs/src/mcp-tools.md
@@ -0,0 +1,31 @@
+# MCP tool reference
+
+[Connect the server](mcp.md), then use its advertised tool schemas as the runtime contract. Tools return JSON strings; pass the returned instance or bundle as `problem_json` to the next operation.
+
+## Graph queries
+
+| Tool | Parameters | Description |
+|------|-----------|-------------|
+| `list_problems` | *(none)* | List all registered problem types with aliases, variant counts, and reduction counts |
+| `show_problem` | `problem` (string) | Show details for a problem type: variants, size fields, schema, and incoming/outgoing reductions |
+| `neighbors` | `problem` (string), `hops` (int, default: 1), `direction` ("out"\|"in"\|"both", default: "out") | Find neighboring problems reachable via reduction edges within a given hop distance |
+| `find_path` | `source` (string), `target` (string), `cost` (string, default: "minimize-steps"), `all` (bool, default: false), `max_paths` (int, default: 20) | Find a reduction path between two problems, optionally minimizing a size field or returning all paths |
+| `export_graph` | *(none)* | Export the full reduction graph as JSON (nodes, edges, overheads) |
+
+## Instances
+
+| Tool | Parameters | Description |
+|------|-----------|-------------|
+| `create_problem` | `problem_type` (string), `params` (JSON object) | Create a problem instance from parameters and return its JSON representation. Supports graph problems, SAT, QUBO, SpinGlass, KColoring, Factoring, and random graph generation |
+| `inspect_problem` | `problem_json` (string) | Inspect a problem JSON or reduction bundle: returns type, size metrics, available solvers, and reduction targets |
+| `evaluate` | `problem_json` (string), `config` (array of int) | Evaluate a configuration against a problem instance and return the objective value or feasibility |
+| `reduce` | `problem_json` (string), `target` (string) | Reduce a problem instance to a target type, returning a reduction bundle with the transformed instance and path metadata |
+| `solve` | `problem_json` (string), `solver` ("ilp"\|"brute-force"\|"customized", default: "ilp"), `timeout` (int, default: 0) | Solve a problem instance or reduction bundle using the chosen backend, with optional timeout |
+
+## Prompt templates
+
+The server also advertises `what_is`, `model_my_problem`, `compare`, `reduce`, `solve`, `find_reduction`, and `overview`. Inspect each prompt’s declared arguments in your MCP client.
+
+Creation supports selected models and uses MCP parameter names such as `edges`; CLI creation flags are a separate interface. For models outside MCP creation support, create JSON with the CLI and pass it to the instance tools.
+
+Next: [example session](mcp-walkthrough.md).
diff --git a/docs/src/mcp-walkthrough.md b/docs/src/mcp-walkthrough.md
new file mode 100644
index 000000000..b1ff2d747
--- /dev/null
+++ b/docs/src/mcp-walkthrough.md
@@ -0,0 +1,30 @@
+# MCP example session
+
+**Before you start:** [connect the server](mcp.md). This is a reproducible task specification; the [CLI recording](cli-demo.md) shows a real execution of the corresponding workflow.
+
+## Ask the agent
+
+```text
+Create Maximum Independent Set on the cycle with edges
+0-1, 1-2, 2-3, 3-4, 4-0. Discover a route to ILP, reduce and solve it.
+Evaluate the recovered source configuration on the original instance.
+Cross-check the optimum with brute force and report both evaluations.
+```
+
+## Expected tool sequence
+
+| Tool | Key input |
+|---|---|
+| `show_problem` | `problem: "MIS"` |
+| `find_path` | `source: "MIS", target: "ILP"` |
+| `create_problem` | `problem_type: "MIS", params: {"edges": "0-1,1-2,2-3,3-4,4-0"}` |
+| `reduce` | Original problem JSON, `target: "ILP"` |
+| `solve` | Reduction bundle JSON, `solver: "ilp"` |
+| `evaluate` | Original problem JSON, recovered `config` |
+| `solve` | Original problem JSON, `solver: "brute-force"` |
+
+## Check the result
+
+The maximum independent set has size 2. Both solves and the source evaluation should return `Max(2)`. Valid witnesses include `[1,0,1,0,0]` and `[0,0,1,0,1]`.
+
+Retain the original JSON for evaluation. Passing only the transformed target loses the context required to check the original problem.
diff --git a/docs/src/mcp.md b/docs/src/mcp.md
index 05913595c..d7adec2d2 100644
--- a/docs/src/mcp.md
+++ b/docs/src/mcp.md
@@ -1,107 +1,31 @@
-# MCP Server
+# Connect with MCP
-The [Model Context Protocol (MCP)](https://modelcontextprotocol.io/) is an open standard that allows AI assistants to interact with external tools and data sources. The `pred` CLI includes a built-in MCP server that exposes the full reduction graph, problem creation, solving, and reduction capabilities to any MCP-compatible AI assistant.
+`pred mcp` exposes catalog queries, instance creation, reductions, and solving over a local stdio MCP server.
-## Setup
-
-Install the `pred` CLI, then configure your AI assistant:
+## Install with MCP support
```bash
-cargo install problemreductions-cli
+cargo install problemreductions-cli --features mcp
+pred mcp --help
```
-**Claude Code:**
-
-```bash
-claude mcp add --scope user problemreductions -- pred mcp
-```
+For the current checkout, use `cargo install --path problemreductions-cli --features mcp`. MCP is an optional feature and is not included in the default CLI install.
-**Cursor / Windsurf** — add to `.cursor/mcp.json` or `~/.codeium/windsurf/mcp_config.json`:
-
-```json
-{ "mcpServers": { "problemreductions": { "command": "pred", "args": ["mcp"] } } }
-```
+## Configure your client
-**OpenCode** — add to `opencode.json`:
+Register a local stdio server with executable `pred` and argument `mcp`. Clients using an `mcpServers` configuration accept this shape:
```json
-{ "mcp": { "problemreductions": { "type": "local", "command": ["pred", "mcp"] } } }
+{
+ "mcpServers": {
+ "problemreductions": {
+ "command": "pred",
+ "args": ["mcp"]
+ }
+ }
+}
```
-Restart your AI assistant after configuration.
-
-## Walkthrough
-
-A complete Claude Code session showing how the AI assistant uses MCP tools behind the scenes to answer your questions.
-
-**You:** Create a weighted MIS problem on a 4-vertex graph with edges 0-1, 1-2, 2-3, 3-0, 0-2 and weights [1, 2, 3, 4], explain the result.
-
-> **Assistant:** I created a Maximum Independent Set instance on a SimpleGraph with 4 vertices, 5 edges, and integer weights [1, 2, 3, 4]. Each vertex has a weight, and the goal is to find a subset of non-adjacent vertices that maximizes total weight.
-
-**You:** What can I do with this problem? Explain the result.
-
-> **Assistant:** This instance has 4 binary variables (one per vertex). It can be reduced to 5 other problem types: ILP, MaximumSetPacking, MinimumVertexCover, QUBO, and other MIS variants. You can solve it directly using either an ILP solver or brute-force search.
-
-**You:** Check if selecting vertices 1 and 3 is a valid solution, explain the result.
-
-> **Assistant:** Yes! Selecting vertices 1 and 3 (configuration [0,1,0,1]) is a valid independent set — these two vertices are not adjacent. The total weight is 2 + 4 = 6.
-
-**You:** Reduce this to QUBO, explain the result.
-
-> **Assistant:** Done. The MIS instance was transformed into a 4x4 QUBO matrix:
->
-> ```
-> [-1.0, 11.0, 11.0, 11.0]
-> [ 0.0, -2.0, 11.0, 0.0]
-> [ 0.0, 0.0, -3.0, 11.0]
-> [ 0.0, 0.0, 0.0, -4.0]
-> ```
->
-> The diagonal entries (-1, -2, -3, -4) encode vertex weights negated for minimization. The off-diagonal entries (11.0) are large penalties on edges — selecting two adjacent vertices would incur a penalty that outweighs any benefit. The reduction path is: MaximumIndependentSet → MaximumSetPacking → QUBO.
-
-**You:** Now solve it through the reduction, explain the result.
-
-> **Assistant:** The ILP solver found the optimal solution by solving the QUBO, then mapping the result back to the original MIS:
->
-> - **QUBO solution:** [0,1,0,1] with objective -6.0 (minimization)
-> - **MIS solution:** vertices {1, 3} with weight **6** (maximization)
->
-> The QUBO objective of -6.0 corresponds to the MIS maximum of 6 — the reduction correctly inverts the sign. This confirms that {1, 3} is the optimal independent set.
-
-## Available Tools
-
-The MCP server provides 10 tools organized into two categories: **graph query tools** for exploring the reduction graph, and **instance tools** for working with concrete problem instances.
-
-### Graph Query Tools
-
-| Tool | Parameters | Description |
-|------|-----------|-------------|
-| `list_problems` | *(none)* | List all registered problem types with aliases, variant counts, and reduction counts |
-| `show_problem` | `problem` (string) | Show details for a problem type: variants, size fields, schema, and incoming/outgoing reductions |
-| `neighbors` | `problem` (string), `hops` (int, default: 1), `direction` ("out"\|"in"\|"both", default: "out") | Find neighboring problems reachable via reduction edges within a given hop distance |
-| `find_path` | `source` (string), `target` (string), `cost` (string, default: "minimize-steps"), `all` (bool, default: false) | Find a reduction path between two problems, optionally minimizing a size field or returning all paths |
-| `export_graph` | *(none)* | Export the full reduction graph as JSON (nodes, edges, overheads) |
-
-### Instance Tools
-
-| Tool | Parameters | Description |
-|------|-----------|-------------|
-| `create_problem` | `problem_type` (string), `params` (JSON object) | Create a problem instance from parameters and return its JSON representation. Supports graph problems, SAT, QUBO, SpinGlass, KColoring, Factoring, and random graph generation |
-| `inspect_problem` | `problem_json` (string) | Inspect a problem JSON or reduction bundle: returns type, size metrics, available solvers, and reduction targets |
-| `evaluate` | `problem_json` (string), `config` (array of int) | Evaluate a configuration against a problem instance and return the objective value or feasibility |
-| `reduce` | `problem_json` (string), `target` (string) | Reduce a problem instance to a target type, returning a reduction bundle with the transformed instance and path metadata |
-| `solve` | `problem_json` (string), `solver` ("ilp"\|"brute-force", default: "ilp"), `timeout` (int, default: 0) | Solve a problem instance or reduction bundle using ILP or brute-force, with optional timeout |
-
-## Available Prompts
-
-The server provides 7 task-oriented prompt templates:
+Ensure the client can resolve `pred` on its `PATH`, or supply the executable's absolute path. Reload the client and request the server's tool list to verify the connection.
-| Prompt | Arguments | Description |
-|--------|-----------|-------------|
-| `what_is` | `problem_type` (required) | Explain a problem type |
-| `model_my_problem` | `description` (required) | Map a real-world problem to an NP-hard type |
-| `compare` | `problem_a` (required), `problem_b` (required) | Compare two problem types |
-| `reduce` | `source` (required), `target` (required) | Step-by-step reduction walkthrough |
-| `solve` | `problem_type` (required), `params` (required) | Create and solve a problem instance |
-| `find_reduction` | `source` (required), `target` (required) | Find the best reduction path between two problems |
-| `overview` | *(none)* | Explore the full landscape of NP-hard problems |
+Next: [tool reference](mcp-tools.md) or [example session](mcp-walkthrough.md).
diff --git a/docs/src/reduction-graph.md b/docs/src/reduction-graph.md
new file mode 100644
index 000000000..8af87ecad
--- /dev/null
+++ b/docs/src/reduction-graph.md
@@ -0,0 +1,35 @@
+# Reduction graph
+
+
+
+
+
+
+
+
+
+ Graph
+ Formula
+ Set
+ Algebraic
+ Misc
+ Variant Cast
+
+
+ Click a node to start path selection
+
+
+
+
+
+ Click a problem node to expand/collapse its variants.
+ Click a variant to filter its edges.
+ Click two nodes to find a reduction path.
+ Double-click for API docs (nodes) or source code (edges).
+ Scroll to zoom, drag to pan.
+
+
+
+You can also explore this graph from the terminal with the [CLI tool](./cli.md). For theoretical background and correctness proofs, see the [PDF manual](https://codingthrust.github.io/problem-reductions/reductions.pdf).
+
+For exact variants and structured output, use [CLI path queries](cli-paths.md).
diff --git a/docs/src/rust-paths.md b/docs/src/rust-paths.md
new file mode 100644
index 000000000..3812533b8
--- /dev/null
+++ b/docs/src/rust-paths.md
@@ -0,0 +1,35 @@
+# Discover and execute paths
+
+Search uses exact variants. This example discovers a witness-capable route from `Factoring` to `SpinGlass`.
+
+```rust,ignore
+use problemreductions::prelude::*;
+use problemreductions::rules::{MinimizeSteps, ReductionGraph};
+use problemreductions::topology::SimpleGraph;
+use problemreductions::types::ProblemSize;
+{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:step1}}
+```
+
+## Execute the route
+
+```rust,ignore
+let factoring = Factoring::new(2, 2, 6);
+let reduction = graph
+ .reduce_along_path(&rpath, &factoring)
+ .unwrap();
+let target: &SpinGlass = reduction.target_problem();
+// Solve `target` with a compatible solver, then recover source bits:
+// let source_config = reduction.extract_solution(&target_config);
+```
+
+`extract_solution` walks the intermediate mappings in reverse. A discovered path establishes a registered transformation, not an efficient target solve.
+
+The [runnable factoring example](https://github.com/CodingThrust/problem-reductions/blob/main/examples/chained_reduction_factoring_to_spinglass.rs) discovers the SpinGlass route, then separately solves factoring through a direct integer ILP reduction. Run it with:
+
+```bash
+cargo run --example chained_reduction_factoring_to_spinglass
+```
+
+It checks that the recovered factors multiply to 6 and prints composed overheads.
+
+Next: [path costs and overhead](design-paths.md).
diff --git a/docs/src/rust-reduction.md b/docs/src/rust-reduction.md
new file mode 100644
index 000000000..4a4d56472
--- /dev/null
+++ b/docs/src/rust-reduction.md
@@ -0,0 +1,30 @@
+# Apply a reduction
+
+Reduce Maximum Set Packing to binary ILP, solve the target, and recover the original configuration. The default library features include the HiGHS backend.
+
+```rust
+use problemreductions::prelude::*;
+use problemreductions::models::algebraic::ILP;
+use problemreductions::solvers::ILPSolver;
+
+fn main() {
+ let problem = MaximumSetPacking::::new(vec![
+ vec![0, 1], vec![1, 2], vec![2, 3], vec![4, 5],
+ ]);
+ let reduction = ReduceTo::>::reduce_to(&problem);
+ let target = reduction.target_problem();
+ assert_eq!(target.num_vars(), 4);
+ assert_eq!(target.num_constraints(), 2);
+
+ let target_solution = ILPSolver::new().solve(target).unwrap();
+ let solution = reduction.extract_solution(&target_solution);
+ assert_eq!(solution, vec![1, 0, 1, 1]);
+ println!("{}", problem.evaluate(&solution)); // Max(3)
+}
+```
+
+The target has one binary variable per set and excludes overlapping pairs. `extract_solution` maps a target witness to the source configuration space.
+
+For types implementing `ReduceTo>`, `ILPSolver::new().solve_reduced(&problem)` combines these steps. It returns an optional source configuration; evaluate it against the original problem.
+
+Next: [discover a multi-step path](rust-paths.md).
diff --git a/docs/src/rust-solvers.md b/docs/src/rust-solvers.md
new file mode 100644
index 000000000..1a2a62263
--- /dev/null
+++ b/docs/src/rust-solvers.md
@@ -0,0 +1,27 @@
+# Solver contracts
+
+Choose a solver by its input and result contract.
+
+| API | Result | Scope |
+|---|---|---|
+| `Solver::solve` with `BruteForce` | Aggregate value | Any problem whose value implements `Aggregate` |
+| `BruteForce::find_witness` | Optional configuration | Values supporting representative witnesses |
+| `ILPSolver::solve` | Optional ILP configuration | ILP instances; requires an ILP backend |
+| `ILPSolver::solve_reduced` | Optional source configuration | Witness-capable problems implementing `ReduceTo>` |
+| `CustomizedSolver` | Model-specific exact solving | Selected models with specialized implementations |
+
+The aggregate `Solver::solve` contract differs from the inherent witness-returning ILP methods. Counting and other aggregate-only problems need a value, not a representative configuration.
+
+## Feature selection
+
+HiGHS is enabled by default through `ilp-highs`. To use the library without it:
+
+```bash
+cargo add problemreductions --no-default-features
+```
+
+See the [solver API](api/problemreductions/solvers/index.html) for exact method signatures and supported specialized backends.
+
+## Verification
+
+For witness results, evaluate the recovered configuration against the source. For aggregate results, compare values according to the reduction's extraction contract. Use small exhaustive solves as independent checks.
diff --git a/docs/src/skills.md b/docs/src/skills.md
index 98b26fee2..d382df1c4 100644
--- a/docs/src/skills.md
+++ b/docs/src/skills.md
@@ -1,19 +1,30 @@
-# AI Agent Skills
+# Start with an agent
-AI coding assistants ([Claude Code](https://claude.ai/claude-code), [OpenCode](https://github.com/opencode-ai/opencode), [Codex](https://github.com/openai/codex)) can call `pred` CLI commands directly and use interactive skills to work with the reduction graph.
+An agent can use the CLI directly from a repository checkout. Skills supply the task procedure; the CLI supplies current model and reduction data.
-## Quick Start
-
-Paste into Claude Code or Codex:
+## Prepare the workspace
+```bash
+git clone https://github.com/CodingThrust/problem-reductions
+cd problem-reductions
+make cli
```
-1. Clone https://github.com/CodingThrust/problem-reductions,
-2. Build the pred CLI with `make cli` in the root directory,
-3.1 Run `/find-solver` skill to help me find a solver for my scheduling problem.
-3.2 Run `/find-problem` skill to help me find problems that my QUBO solver can solve.
-3.3 Run `/propose` skill to help me propose a new problem or reduction to the project.
+
+This installs `pred` into Cargo’s binary directory (usually `~/.cargo/bin`). Confirm it is on your shell’s `PATH` with `pred --version`.
+
+## Give the agent this context
+
+```text
+Work in this repository. Read AGENTS.md and .claude/CLAUDE.md.
+Use the built pred CLI to inspect current models, variants, and paths.
+Read the SKILL.md for the task before following its workflow.
+Report the exact model variant, commands, results, and unresolved assumptions.
```
-The prompt 3.1 is for users who have a real-world problem and need help finding a solver for it.
-The prompt 3.2 is for users who have a solver and need help finding problems that it can solve.
-The prompt 3.3 is for contributors who want to propose a new problem or reduction rule to the project.
\ No newline at end of file
+Then choose [find a solver](agent-find-solver.md), [extend a solver's reach](agent-find-problem.md), or [propose a rule](agent-propose.md).
+
+## Read without a browser
+
+Use the [Markdown index](markdown/index.md) to retrieve only the relevant task pages. Code includes are expanded in those files. The [graph and schemas](cli-automation.md#registry-exports) provide structured data.
+
+An agent with MCP support can instead [connect to `pred mcp`](mcp.md). Repository skills still require access to the checkout.
diff --git a/docs/src/static/asciinema-player-LICENSE b/docs/src/static/asciinema-player-LICENSE
new file mode 100644
index 000000000..15258081e
--- /dev/null
+++ b/docs/src/static/asciinema-player-LICENSE
@@ -0,0 +1,201 @@
+ Apache License
+ Version 2.0, January 2004
+ http://www.apache.org/licenses/
+
+ TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+ 1. Definitions.
+
+ "License" shall mean the terms and conditions for use, reproduction,
+ and distribution as defined by Sections 1 through 9 of this document.
+
+ "Licensor" shall mean the copyright owner or entity authorized by
+ the copyright owner that is granting the License.
+
+ "Legal Entity" shall mean the union of the acting entity and all
+ other entities that control, are controlled by, or are under common
+ control with that entity. For the purposes of this definition,
+ "control" means (i) the power, direct or indirect, to cause the
+ direction or management of such entity, whether by contract or
+ otherwise, or (ii) ownership of fifty percent (50%) or more of the
+ outstanding shares, or (iii) beneficial ownership of such entity.
+
+ "You" (or "Your") shall mean an individual or Legal Entity
+ exercising permissions granted by this License.
+
+ "Source" form shall mean the preferred form for making modifications,
+ including but not limited to software source code, documentation
+ source, and configuration files.
+
+ "Object" form shall mean any form resulting from mechanical
+ transformation or translation of a Source form, including but
+ not limited to compiled object code, generated documentation,
+ and conversions to other media types.
+
+ "Work" shall mean the work of authorship, whether in Source or
+ Object form, made available under the License, as indicated by a
+ copyright notice that is included in or attached to the work
+ (an example is provided in the Appendix below).
+
+ "Derivative Works" shall mean any work, whether in Source or Object
+ form, that is based on (or derived from) the Work and for which the
+ editorial revisions, annotations, elaborations, or other modifications
+ represent, as a whole, an original work of authorship. For the purposes
+ of this License, Derivative Works shall not include works that remain
+ separable from, or merely link (or bind by name) to the interfaces of,
+ the Work and Derivative Works thereof.
+
+ "Contribution" shall mean any work of authorship, including
+ the original version of the Work and any modifications or additions
+ to that Work or Derivative Works thereof, that is intentionally
+ submitted to Licensor for inclusion in the Work by the copyright owner
+ or by an individual or Legal Entity authorized to submit on behalf of
+ the copyright owner. For the purposes of this definition, "submitted"
+ means any form of electronic, verbal, or written communication sent
+ to the Licensor or its representatives, including but not limited to
+ communication on electronic mailing lists, source code control systems,
+ and issue tracking systems that are managed by, or on behalf of, the
+ Licensor for the purpose of discussing and improving the Work, but
+ excluding communication that is conspicuously marked or otherwise
+ designated in writing by the copyright owner as "Not a Contribution."
+
+ "Contributor" shall mean Licensor and any individual or Legal Entity
+ on behalf of whom a Contribution has been received by Licensor and
+ subsequently incorporated within the Work.
+
+ 2. Grant of Copyright License. Subject to the terms and conditions of
+ this License, each Contributor hereby grants to You a perpetual,
+ worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+ copyright license to reproduce, prepare Derivative Works of,
+ publicly display, publicly perform, sublicense, and distribute the
+ Work and such Derivative Works in Source or Object form.
+
+ 3. Grant of Patent License. Subject to the terms and conditions of
+ this License, each Contributor hereby grants to You a perpetual,
+ worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+ (except as stated in this section) patent license to make, have made,
+ use, offer to sell, sell, import, and otherwise transfer the Work,
+ where such license applies only to those patent claims licensable
+ by such Contributor that are necessarily infringed by their
+ Contribution(s) alone or by combination of their Contribution(s)
+ with the Work to which such Contribution(s) was submitted. If You
+ institute patent litigation against any entity (including a
+ cross-claim or counterclaim in a lawsuit) alleging that the Work
+ or a Contribution incorporated within the Work constitutes direct
+ or contributory patent infringement, then any patent licenses
+ granted to You under this License for that Work shall terminate
+ as of the date such litigation is filed.
+
+ 4. Redistribution. You may reproduce and distribute copies of the
+ Work or Derivative Works thereof in any medium, with or without
+ modifications, and in Source or Object form, provided that You
+ meet the following conditions:
+
+ (a) You must give any other recipients of the Work or
+ Derivative Works a copy of this License; and
+
+ (b) You must cause any modified files to carry prominent notices
+ stating that You changed the files; and
+
+ (c) You must retain, in the Source form of any Derivative Works
+ that You distribute, all copyright, patent, trademark, and
+ attribution notices from the Source form of the Work,
+ excluding those notices that do not pertain to any part of
+ the Derivative Works; and
+
+ (d) If the Work includes a "NOTICE" text file as part of its
+ distribution, then any Derivative Works that You distribute must
+ include a readable copy of the attribution notices contained
+ within such NOTICE file, excluding those notices that do not
+ pertain to any part of the Derivative Works, in at least one
+ of the following places: within a NOTICE text file distributed
+ as part of the Derivative Works; within the Source form or
+ documentation, if provided along with the Derivative Works; or,
+ within a display generated by the Derivative Works, if and
+ wherever such third-party notices normally appear. The contents
+ of the NOTICE file are for informational purposes only and
+ do not modify the License. You may add Your own attribution
+ notices within Derivative Works that You distribute, alongside
+ or as an addendum to the NOTICE text from the Work, provided
+ that such additional attribution notices cannot be construed
+ as modifying the License.
+
+ You may add Your own copyright statement to Your modifications and
+ may provide additional or different license terms and conditions
+ for use, reproduction, or distribution of Your modifications, or
+ for any such Derivative Works as a whole, provided Your use,
+ reproduction, and distribution of the Work otherwise complies with
+ the conditions stated in this License.
+
+ 5. Submission of Contributions. Unless You explicitly state otherwise,
+ any Contribution intentionally submitted for inclusion in the Work
+ by You to the Licensor shall be under the terms and conditions of
+ this License, without any additional terms or conditions.
+ Notwithstanding the above, nothing herein shall supersede or modify
+ the terms of any separate license agreement you may have executed
+ with Licensor regarding such Contributions.
+
+ 6. Trademarks. This License does not grant permission to use the trade
+ names, trademarks, service marks, or product names of the Licensor,
+ except as required for reasonable and customary use in describing the
+ origin of the Work and reproducing the content of the NOTICE file.
+
+ 7. Disclaimer of Warranty. Unless required by applicable law or
+ agreed to in writing, Licensor provides the Work (and each
+ Contributor provides its Contributions) on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+ implied, including, without limitation, any warranties or conditions
+ of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+ PARTICULAR PURPOSE. You are solely responsible for determining the
+ appropriateness of using or redistributing the Work and assume any
+ risks associated with Your exercise of permissions under this License.
+
+ 8. Limitation of Liability. In no event and under no legal theory,
+ whether in tort (including negligence), contract, or otherwise,
+ unless required by applicable law (such as deliberate and grossly
+ negligent acts) or agreed to in writing, shall any Contributor be
+ liable to You for damages, including any direct, indirect, special,
+ incidental, or consequential damages of any character arising as a
+ result of this License or out of the use or inability to use the
+ Work (including but not limited to damages for loss of goodwill,
+ work stoppage, computer failure or malfunction, or any and all
+ other commercial damages or losses), even if such Contributor
+ has been advised of the possibility of such damages.
+
+ 9. Accepting Warranty or Additional Liability. While redistributing
+ the Work or Derivative Works thereof, You may choose to offer,
+ and charge a fee for, acceptance of support, warranty, indemnity,
+ or other liability obligations and/or rights consistent with this
+ License. However, in accepting such obligations, You may act only
+ on Your own behalf and on Your sole responsibility, not on behalf
+ of any other Contributor, and only if You agree to indemnify,
+ defend, and hold each Contributor harmless for any liability
+ incurred by, or claims asserted against, such Contributor by reason
+ of your accepting any such warranty or additional liability.
+
+ END OF TERMS AND CONDITIONS
+
+ APPENDIX: How to apply the Apache License to your work.
+
+ To apply the Apache License to your work, attach the following
+ boilerplate notice, with the fields enclosed by brackets "{}"
+ replaced with your own identifying information. (Don't include
+ the brackets!) The text should be enclosed in the appropriate
+ comment syntax for the file format. We also recommend that a
+ file or class name and description of purpose be included on the
+ same "printed page" as the copyright notice for easier
+ identification within third-party archives.
+
+ Copyright 2011-2021 Marcin Kulik
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+ http://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
diff --git a/docs/src/static/cli-demo.cast b/docs/src/static/cli-demo.cast
new file mode 100644
index 000000000..cd9afb3e8
--- /dev/null
+++ b/docs/src/static/cli-demo.cast
@@ -0,0 +1,267 @@
+{"version": 2, "width": 88, "height": 22, "title": "From a graph to a verified solution", "env": {"TERM": "xterm-256color", "SHELL": "/bin/bash"}}
+[0.0, "o", "\u001b[90m# Discover a route to an available solver\u001b[0m\r\n"]
+[0.45, "o", "$ "]
+[0.75, "o", "."]
+[0.798061, "o", "/"]
+[0.831401, "o", "p"]
+[0.852611, "o", "r"]
+[0.899118, "o", "e"]
+[0.946418, "o", "d"]
+[0.98372, "o", " "]
+[1.023524, "o", "p"]
+[1.046874, "o", "a"]
+[1.089336, "o", "t"]
+[1.116966, "o", "h"]
+[1.138829, "o", " "]
+[1.181915, "o", "M"]
+[1.212605, "o", "I"]
+[1.251057, "o", "S"]
+[1.2893, "o", " "]
+[1.31446, "o", "I"]
+[1.340586, "o", "L"]
+[1.36479, "o", "P"]
+[1.566199, "o", "\r\n"]
+[1.746434, "o", "Path (3 steps): MaximumIndependentSet/SimpleGraph/One → MaximumSetPacking/One → ILP/bool\r\n\r\n Step 1: MaximumIndependentSet/SimpleGraph/One → MaximumSetPacking/One\r\n num_sets = O(num_vertices)\r\n universe_size = O(num_edges)\r\n\r\n Step 2: MaximumSetPacking/One → MaximumSetPacking/i32\r\n num_sets = O(num_sets)\r\n universe_size = O(universe_size)\r\n\r\n Step 3: MaximumSetPacking/i32 → ILP/bool\r\n num_vars = O(num_sets)\r\n num_constraints = O(universe_size)\r\n\r\n Overall:\r\n num_vars = O(num_vertices)\r\n num_constraints = O(num_edges)\r\n\r\n"]
+[4.246434, "o", "\u001b[90m# Create a five-vertex cycle\u001b[0m\r\n"]
+[4.696434, "o", "$ "]
+[4.996434, "o", "."]
+[5.031063, "o", "/"]
+[5.07908, "o", "p"]
+[5.101888, "o", "r"]
+[5.138038, "o", "e"]
+[5.172084, "o", "d"]
+[5.209925, "o", " "]
+[5.233415, "o", "c"]
+[5.270627, "o", "r"]
+[5.299175, "o", "e"]
+[5.335755, "o", "a"]
+[5.374805, "o", "t"]
+[5.409274, "o", "e"]
+[5.440221, "o", " "]
+[5.468197, "o", "M"]
+[5.515335, "o", "I"]
+[5.54903, "o", "S"]
+[5.584875, "o", " "]
+[5.606415, "o", "-"]
+[5.641642, "o", "-"]
+[5.662804, "o", "g"]
+[5.687829, "o", "r"]
+[5.722069, "o", "a"]
+[5.753634, "o", "p"]
+[5.776151, "o", "h"]
+[5.813602, "o", " "]
+[5.839194, "o", "0"]
+[5.875799, "o", "-"]
+[5.900838, "o", "1"]
+[5.948083, "o", ","]
+[5.99067, "o", "1"]
+[6.038464, "o", "-"]
+[6.063419, "o", "2"]
+[6.09297, "o", ","]
+[6.115078, "o", "2"]
+[6.143828, "o", "-"]
+[6.187411, "o", "3"]
+[6.213376, "o", ","]
+[6.238704, "o", "3"]
+[6.286436, "o", "-"]
+[6.311764, "o", "4"]
+[6.356113, "o", ","]
+[6.378262, "o", "4"]
+[6.410075, "o", "-"]
+[6.440864, "o", "0"]
+[6.471432, "o", " "]
+[6.515293, "o", "-"]
+[6.549619, "o", "o"]
+[6.59254, "o", " "]
+[6.626723, "o", "c"]
+[6.670609, "o", "y"]
+[6.716293, "o", "c"]
+[6.749602, "o", "l"]
+[6.792471, "o", "e"]
+[6.836284, "o", "."]
+[6.865563, "o", "j"]
+[6.890032, "o", "s"]
+[6.916229, "o", "o"]
+[6.949439, "o", "n"]
+[7.153784, "o", "\r\n"]
+[7.304369, "o", "Wrote cycle.json\r\n"]
+[9.804369, "o", "\u001b[90m# Transform the instance and preserve the way back\u001b[0m\r\n"]
+[10.254369, "o", "$ "]
+[10.554369, "o", "."]
+[10.590203, "o", "/"]
+[10.634427, "o", "p"]
+[10.669013, "o", "r"]
+[10.712909, "o", "e"]
+[10.752288, "o", "d"]
+[10.791237, "o", " "]
+[10.821907, "o", "r"]
+[10.862582, "o", "e"]
+[10.90626, "o", "d"]
+[10.931661, "o", "u"]
+[10.978084, "o", "c"]
+[11.006626, "o", "e"]
+[11.031961, "o", " "]
+[11.076495, "o", "c"]
+[11.117658, "o", "y"]
+[11.160878, "o", "c"]
+[11.194385, "o", "l"]
+[11.217367, "o", "e"]
+[11.249433, "o", "."]
+[11.27177, "o", "j"]
+[11.300782, "o", "s"]
+[11.322846, "o", "o"]
+[11.358034, "o", "n"]
+[11.381488, "o", " "]
+[11.428607, "o", "-"]
+[11.46919, "o", "-"]
+[11.499066, "o", "t"]
+[11.546527, "o", "o"]
+[11.569382, "o", " "]
+[11.59759, "o", "I"]
+[11.620634, "o", "L"]
+[11.65357, "o", "P"]
+[11.680223, "o", " "]
+[11.712329, "o", "-"]
+[11.753066, "o", "o"]
+[11.798911, "o", " "]
+[11.833926, "o", "r"]
+[11.877845, "o", "e"]
+[11.90896, "o", "d"]
+[11.954003, "o", "u"]
+[11.989424, "o", "c"]
+[12.030092, "o", "e"]
+[12.055983, "o", "d"]
+[12.093349, "o", "."]
+[12.122799, "o", "j"]
+[12.166559, "o", "s"]
+[12.202521, "o", "o"]
+[12.237509, "o", "n"]
+[12.460162, "o", "\r\n"]
+[12.611677, "o", "Wrote reduced.json\r\n"]
+[15.111677, "o", "\u001b[90m# Solve the target and recover a source solution\u001b[0m\r\n"]
+[15.561677, "o", "$ "]
+[15.861677, "o", "."]
+[15.89805, "o", "/"]
+[15.928395, "o", "p"]
+[15.953061, "o", "r"]
+[15.991547, "o", "e"]
+[16.038457, "o", "d"]
+[16.083043, "o", " "]
+[16.105996, "o", "s"]
+[16.136104, "o", "o"]
+[16.157151, "o", "l"]
+[16.197043, "o", "v"]
+[16.235915, "o", "e"]
+[16.278136, "o", " "]
+[16.303288, "o", "r"]
+[16.330365, "o", "e"]
+[16.363482, "o", "d"]
+[16.405111, "o", "u"]
+[16.43191, "o", "c"]
+[16.475949, "o", "e"]
+[16.507623, "o", "d"]
+[16.553103, "o", "."]
+[16.600984, "o", "j"]
+[16.637033, "o", "s"]
+[16.683823, "o", "o"]
+[16.71664, "o", "n"]
+[16.936828, "o", "\r\n"]
+[17.089047, "o", "Problem: MaximumIndependentSet\r\nSolver: ilp (via ILP)\r\nSolution: [1, 0, 1, 0, 0]\r\nEvaluation: Max(2)\r\n\r\nHint: use -o to save full solution details (including intermediate results) as JSON.\r\n"]
+[19.589047, "o", "\u001b[90m# Check an independent set of size two\u001b[0m\r\n"]
+[20.039047, "o", "$ "]
+[20.339047, "o", "."]
+[20.38376, "o", "/"]
+[20.428246, "o", "p"]
+[20.451846, "o", "r"]
+[20.480135, "o", "e"]
+[20.512622, "o", "d"]
+[20.557641, "o", " "]
+[20.58639, "o", "e"]
+[20.610575, "o", "v"]
+[20.642085, "o", "a"]
+[20.669073, "o", "l"]
+[20.710128, "o", "u"]
+[20.747578, "o", "a"]
+[20.770048, "o", "t"]
+[20.815616, "o", "e"]
+[20.848952, "o", " "]
+[20.891705, "o", "c"]
+[20.917334, "o", "y"]
+[20.946955, "o", "c"]
+[20.970008, "o", "l"]
+[21.002068, "o", "e"]
+[21.035078, "o", "."]
+[21.075196, "o", "j"]
+[21.109624, "o", "s"]
+[21.141839, "o", "o"]
+[21.176222, "o", "n"]
+[21.205097, "o", " "]
+[21.236444, "o", "-"]
+[21.274258, "o", "-"]
+[21.301027, "o", "c"]
+[21.336556, "o", "o"]
+[21.383587, "o", "n"]
+[21.417394, "o", "f"]
+[21.457107, "o", "i"]
+[21.496583, "o", "g"]
+[21.54002, "o", " "]
+[21.581336, "o", "1"]
+[21.620835, "o", ","]
+[21.644739, "o", "0"]
+[21.676005, "o", ","]
+[21.719239, "o", "1"]
+[21.742064, "o", ","]
+[21.766985, "o", "0"]
+[21.813335, "o", ","]
+[21.850799, "o", "0"]
+[22.079244, "o", "\r\n"]
+[22.220535, "o", "Max(2)\r\n"]
+[24.720535, "o", "\u001b[90m# Cross-check the optimum by exhaustive search\u001b[0m\r\n"]
+[25.170535, "o", "$ "]
+[25.470535, "o", "."]
+[25.512635, "o", "/"]
+[25.561514, "o", "p"]
+[25.590875, "o", "r"]
+[25.631085, "o", "e"]
+[25.661342, "o", "d"]
+[25.708829, "o", " "]
+[25.738055, "o", "s"]
+[25.764502, "o", "o"]
+[25.808302, "o", "l"]
+[25.837115, "o", "v"]
+[25.873068, "o", "e"]
+[25.91093, "o", " "]
+[25.94144, "o", "c"]
+[25.971798, "o", "y"]
+[26.001788, "o", "c"]
+[26.030278, "o", "l"]
+[26.072549, "o", "e"]
+[26.110047, "o", "."]
+[26.146398, "o", "j"]
+[26.190474, "o", "s"]
+[26.218674, "o", "o"]
+[26.243513, "o", "n"]
+[26.265307, "o", " "]
+[26.287353, "o", "-"]
+[26.336092, "o", "-"]
+[26.384359, "o", "s"]
+[26.424024, "o", "o"]
+[26.472762, "o", "l"]
+[26.508201, "o", "v"]
+[26.541368, "o", "e"]
+[26.576796, "o", "r"]
+[26.599728, "o", " "]
+[26.641996, "o", "b"]
+[26.671541, "o", "r"]
+[26.712087, "o", "u"]
+[26.758553, "o", "t"]
+[26.785702, "o", "e"]
+[26.820824, "o", "-"]
+[26.860112, "o", "f"]
+[26.903819, "o", "o"]
+[26.943936, "o", "r"]
+[26.974207, "o", "c"]
+[27.011004, "o", "e"]
+[27.216555, "o", "\r\n"]
+[27.358887, "o", "Problem: MaximumIndependentSet\r\nSolver: brute-force\r\nSolution: [0, 0, 1, 0, 1]\r\nEvaluation: Max(2)\r\n\r\nHint: use -o to save full solution details as JSON.\r\n"]
+[29.858887, "o", "$ "]
diff --git a/docs/src/static/cli-demo.html b/docs/src/static/cli-demo.html
new file mode 100644
index 000000000..f47b16c75
--- /dev/null
+++ b/docs/src/static/cli-demo.html
@@ -0,0 +1,2404 @@
+
+
+
+
+
+From a graph to a verified solution
+
+
+
+
+
+
+
+
+
From a graph to a verified solution
+
6 command(s) · 6 passed · 0 failed
+
+
+
+
+
+
+
diff --git a/docs/src/static/docs-theme.css b/docs/src/static/docs-theme.css
new file mode 100644
index 000000000..780566ba8
--- /dev/null
+++ b/docs/src/static/docs-theme.css
@@ -0,0 +1,362 @@
+@font-face {
+ font-family: "DM Sans";
+ src: url("../../../assets/fonts/dm-sans-regular.ttf") format("truetype");
+ font-style: normal;
+ font-weight: 400;
+ font-display: swap;
+}
+@font-face {
+ font-family: "DM Sans";
+ src: url("../../../assets/fonts/dm-sans-semibold.ttf") format("truetype");
+ font-style: normal;
+ font-weight: 600 800;
+ font-display: swap;
+}
+html[class] {
+ color-scheme: dark;
+ --bg: #101713;
+ --fg: #e8ede5;
+ --sidebar-bg: #131c17;
+ --sidebar-fg: #adb9af;
+ --sidebar-active: #c4dda6;
+ --sidebar-non-existant: #87968b;
+ --sidebar-width: 264px;
+ --links: #c4dda6;
+ --inline-code-color: #d5e7c5;
+ --theme-popup-bg: #19241d;
+ --theme-popup-border: #334337;
+ --quote-bg: #17221b;
+ --quote-border: #789566;
+ --table-border-color: #304034;
+ --table-header-bg: #19241d;
+ --table-alternate-bg: #131c17;
+ --searchbar-bg: #19241d;
+ --searchbar-fg: #e8ede5;
+ --searchbar-border-color: #4a614d;
+ --searchresults-header-fg: #e8ede5;
+ --searchresults-border-color: #304034;
+ --searchresults-li-bg: #19241d;
+ --icons: #b5c2b7;
+ --icons-hover: #e8ede5;
+ --content-max-width: 800px;
+}
+body {
+ font-family:
+ "DM Sans",
+ -apple-system,
+ BlinkMacSystemFont,
+ "Segoe UI",
+ sans-serif;
+ font-size: 15px;
+ line-height: 1.75;
+}
+.sidebar {
+ border-right: 1px solid #2a372d;
+ font-size: 13px;
+}
+.docs-brand {
+ display: flex;
+ align-items: center;
+ gap: 12px;
+ padding: 9px 18px;
+ color: var(--fg);
+ text-decoration: none;
+ font-weight: 600;
+ border-bottom: 1px solid #2a372d;
+}
+.docs-brand img {
+ width: 204px;
+ height: 59px;
+ object-fit: contain;
+}
+.sidebar .sidebar-scrollbox {
+ top: 78px;
+ padding: 14px 16px 28px;
+}
+.chapter {
+ line-height: 1.45;
+}
+.chapter li.chapter-item {
+ margin: 2px 0;
+}
+.chapter li a {
+ display: block;
+ padding: 7px 10px;
+ border-radius: 5px;
+ color: var(--sidebar-fg);
+}
+.chapter li a:hover {
+ color: var(--fg);
+ background: #1d2a20;
+ text-decoration: none;
+}
+.chapter li a.active {
+ color: #d4e9ba;
+ background: #263725;
+ font-weight: 600;
+}
+.chapter .section {
+ padding-left: 14px;
+}
+.chapter li.part-title {
+ margin: 23px 10px 7px;
+ color: #e2e9df;
+ font-size: 13px;
+ font-weight: 600;
+ text-transform: none;
+ letter-spacing: 0;
+}
+.chapter li.part-title:first-child {
+ margin-top: 9px;
+}
+.sidebar .on-this-page {
+ display: none;
+}
+.chapter li > a.toggle {
+ padding: 7px 3px;
+ width: 18px;
+}
+:is(#menu-bar, #mdbook-menu-bar) {
+ border-bottom: 1px solid #2a372d;
+ background: #101713;
+ padding: 0 24px;
+}
+.menu-title {
+ display: none;
+}
+.menu-bar .right-buttons {
+ margin-left: auto;
+}
+:is(#theme-toggle, #mdbook-theme-toggle) {
+ display: none;
+}
+.docs-tools {
+ display: flex;
+ align-items: center;
+ gap: 18px;
+ height: 50px;
+}
+.docs-tools a {
+ font-size: 13px;
+ font-weight: 600;
+ color: #b9c7bb;
+ text-decoration: none;
+}
+.docs-tools a:hover {
+ color: var(--links);
+}
+.content {
+ padding: 0 38px;
+}
+.content main {
+ padding: 42px 0 30px;
+}
+.content main > h1 {
+ font-size: 36px;
+ line-height: 1.2;
+ font-weight: 600;
+ letter-spacing: -1px;
+ margin: 0 0 22px;
+}
+.content h2 {
+ font-size: 21px;
+ font-weight: 600;
+ line-height: 1.4;
+ margin: 34px 0 12px;
+ letter-spacing: -0.25px;
+}
+.content h3 {
+ font-size: 17px;
+ font-weight: 600;
+ margin: 26px 0 10px;
+}
+.content p {
+ margin: 12px 0;
+}
+.content main > p:first-of-type {
+ font-size: 16px;
+ color: #c0ccc1;
+ line-height: 1.8;
+}
+.content a {
+ text-decoration: underline;
+ text-underline-offset: 3px;
+}
+.content .header {
+ text-decoration: none;
+}
+.content li {
+ margin: 6px 0;
+}
+.content strong {
+ font-weight: 600;
+}
+.content code {
+ font-size: 13px;
+ border-radius: 3px;
+}
+.content :not(pre) > code {
+ background: #213025;
+ padding: 2px 5px;
+ overflow-wrap: anywhere;
+}
+.content pre {
+ margin: 20px 0;
+ border: 1px solid #334437;
+ border-radius: 8px;
+ background: #162019;
+}
+.content pre > code {
+ display: block;
+ padding: 18px 20px;
+ background: #162019;
+ color: #dfe8dc;
+ line-height: 1.7;
+ tab-size: 4;
+}
+.content pre .buttons {
+ top: 6px;
+ right: 6px;
+}
+.content pre .buttons button {
+ background: #233429;
+ color: #d3dfcf;
+ border-radius: 4px;
+ padding: 7px;
+}
+.content table {
+ display: block;
+ width: 100%;
+ overflow-x: auto;
+ font-size: 14px;
+ margin: 18px 0;
+ border-collapse: collapse;
+}
+.content th {
+ font-weight: 600;
+ text-align: left;
+ color: #dfe8dc;
+}
+.content th,
+.content td {
+ padding: 12px 14px;
+ border: 0;
+ border-bottom: 1px solid #304034;
+}
+.content td {
+ vertical-align: top;
+}
+.content blockquote {
+ margin: 20px 0;
+ padding: 8px 18px;
+ border-radius: 0 6px 6px 0;
+}
+.content details {
+ border: 1px solid #304034;
+ border-radius: 6px;
+ padding: 12px 16px;
+ margin: 18px 0;
+}
+.content summary {
+ cursor: pointer;
+ font-weight: 600;
+ color: #c4dda6;
+}
+.content .header:link,
+.content .header:visited {
+ color: var(--fg);
+}
+.content .hljs-comment {
+ color: #9cac9b;
+ font-style: normal;
+}
+.content .hljs-keyword,
+.content .hljs-selector-tag {
+ color: #a9c9e8;
+}
+.content .hljs-string {
+ color: #c4dda6;
+}
+.content .hljs-number,
+.content .hljs-literal {
+ color: #ebc897;
+}
+.content .hljs-title {
+ color: #d8cfac;
+}
+.content .hljs-meta {
+ color: #a9c9e8;
+}
+.content :focus-visible,
+.docs-tools a:focus-visible,
+.sidebar a:focus-visible {
+ outline: 2px solid #c4dda6;
+ outline-offset: 4px;
+}
+.nav-chapters {
+ color: #b5c2b7;
+}
+.cli-cast {
+ display: block;
+ width: 100%;
+ height: 490px;
+ border: 1px solid #334437;
+ border-radius: 8px;
+ background: #0d0f12;
+ margin: 24px 0 16px;
+}
+:is(#searchbar, #mdbook-searchbar) {
+ padding: 13px 16px;
+ border-radius: 6px;
+}
+:is(#search-wrapper, #mdbook-search-wrapper) {
+ margin: 25px 0 0;
+}
+@media (min-width: 1200px) {
+ .content {
+ padding-left: 56px;
+ padding-right: 56px;
+ }
+}
+@media (max-width: 700px) {
+ .content {
+ padding: 0 22px;
+ }
+ .content main {
+ padding-top: 30px;
+ }
+ .content main > h1 {
+ font-size: 30px;
+ }
+ :is(#menu-bar, #mdbook-menu-bar) {
+ padding: 0 12px;
+ }
+ .docs-tools {
+ gap: 14px;
+ }
+ .docs-tools a {
+ font-size: 12px;
+ }
+ .cli-cast {
+ height: 345px;
+ }
+ .content th,
+ .content td {
+ padding: 9px 10px;
+ }
+}
+@media (max-width: 380px) {
+ .docs-tools a:last-child {
+ display: none;
+ }
+ .cli-cast {
+ height: 285px;
+ }
+}
+@media print {
+ .docs-tools,
+ .docs-brand,
+ .cli-cast {
+ display: none;
+ }
+}
diff --git a/docs/src/static/docs-theme.js b/docs/src/static/docs-theme.js
new file mode 100644
index 000000000..3c11dccb7
--- /dev/null
+++ b/docs/src/static/docs-theme.js
@@ -0,0 +1,125 @@
+/* Small additions to mdBook's native navigation; content remains usable without JS. */
+(() => {
+ const root = window.path_to_root || "";
+ // mdBook 0.5 uses a label for this control; expose its button behavior to keyboards.
+ const toggle = document.querySelector("label#mdbook-sidebar-toggle");
+ if (toggle) {
+ toggle.setAttribute("role", "button");
+ toggle.tabIndex = 0;
+ toggle.addEventListener("keydown", (event) => {
+ if (event.key === "Enter" || event.key === " ") {
+ event.preventDefault();
+ toggle.click();
+ }
+ });
+ }
+ const page = location.pathname.split("/").pop() || "introduction.html";
+ const legacy = {
+ "cli.html": {
+ installation: "install.html",
+ "ilp-backend": "install.html#optional-features",
+ "quick-start": "cli.html",
+ "global-flags": "cli-automation.html",
+ commands: "cli-catalog.html",
+ "shell-completions": "cli-completions.html",
+ "json-output": "cli-automation.html",
+ "problem-name-aliases": "cli-variants.html",
+ "pred-list--list-all-problem-types": "cli-catalog.html",
+ "pred-show--inspect-a-problem": "cli-catalog.html",
+ "pred-to--explore-incoming-neighbors": "cli-paths.html",
+ "pred-from--explore-outgoing-neighbors": "cli-paths.html",
+ "pred-path--find-a-reduction-path": "cli-paths.html",
+ "pred-export-graph--export-the-reduction-graph":
+ "cli-automation.html#registry-exports",
+ "pred-create--create-a-problem-instance": "cli-create.html",
+ "pred-evaluate--evaluate-a-configuration": "cli-inspect.html",
+ "pred-inspect--inspect-a-problem-file": "cli-inspect.html",
+ "pred-reduce--reduce-a-problem": "cli-reduce.html",
+ "pred-solve--solve-a-problem": "cli-solve.html",
+ },
+ "introduction.html": {
+ "reduction-graph": "reduction-graph.html",
+ "our-vision": "introduction.html#research-scope",
+ "call-for-contributions": "contributing.html",
+ authorship: "contributing.html#authorship-and-license",
+ },
+ "design.html": {
+ "module-architecture": "design.html#module-map",
+ "problem-model": "design-problem.html",
+ "variant-system": "design-variants.html",
+ "reduction-rules": "design-reductions.html",
+ "reduction-graph": "design-paths.html",
+ "path-finding": "design-paths.html",
+ "executable-paths": "rust-paths.html",
+ solvers: "rust-solvers.html",
+ "json-serialization": "design-serialization.html",
+ contributing: "contributing.html",
+ },
+ "getting-started.html": {
+ installation: "getting-started.html",
+ solvers: "rust-solvers.html",
+ "the-reduction-workflow": "rust-reduction.html",
+ "json-resources": "cli-automation.html#registry-exports",
+ "example-1-direct-reduction--set-packing-to-ilp": "rust-reduction.html",
+ "example-2-reduction-path-search--integer-factoring-to-spin-glass":
+ "rust-paths.html",
+ },
+ "mcp.html": {
+ setup: "mcp.html#install-with-mcp-support",
+ walkthrough: "mcp-walkthrough.html",
+ "available-tools": "mcp-tools.html",
+ "graph-query-tools": "mcp-tools.html#graph-queries",
+ "instance-tools": "mcp-tools.html#instances",
+ "available-prompts": "mcp-tools.html#prompt-templates",
+ },
+ };
+ const redirect = legacy[page]?.[location.hash.slice(1)];
+ if (redirect) {
+ location.replace(root + redirect);
+ return;
+ }
+ const sidebar = document.querySelector(".sidebar");
+ if (sidebar) {
+ const brand = document.createElement("a");
+ brand.className = "docs-brand";
+ brand.href = root + "introduction.html";
+ const logo = document.createElement("img");
+ logo.src = root + "assets/logo.svg";
+ logo.alt = "Problem Reductions";
+ brand.setAttribute("aria-label", "Documentation home");
+ brand.append(logo);
+ sidebar.prepend(brand);
+ }
+ for (const frame of document.querySelectorAll(".cli-cast")) {
+ frame.addEventListener("load", () => {
+ const content = frame.contentDocument.querySelector(".wrap");
+ if (!content) return;
+ const resize = () => {
+ frame.style.height = `${Math.ceil(content.getBoundingClientRect().height) + 2}px`;
+ };
+ new ResizeObserver(resize).observe(content);
+ resize();
+ });
+ }
+ const menu = document.querySelector(".menu-bar .right-buttons");
+ if (menu && page !== "print.html") {
+ const nav = document.createElement("nav");
+ nav.className = "docs-tools";
+ nav.setAttribute("aria-label", "Documentation resources");
+ const links = [
+ ["Markdown", "markdown/" + page.replace(/\.html$/, ".md")],
+ ["All pages", "markdown/index.md"],
+ ["Open atlas ↗", "index.html#atlas"],
+ ];
+ for (const [label, href] of links) {
+ const link = document.createElement("a");
+ link.textContent = label;
+ link.href = root + href;
+ nav.append(link);
+ }
+ menu.prepend(nav);
+ // Resource links replace duplicate repository, edit, and print icon shortcuts.
+ for (const child of [...menu.children])
+ if (child !== nav) child.hidden = true;
+ }
+})();
diff --git a/docs/website/README.md b/docs/website/README.md
new file mode 100644
index 000000000..ed2ef0f6e
--- /dev/null
+++ b/docs/website/README.md
@@ -0,0 +1,115 @@
+# Research website
+
+The public entry point presents Problem Reductions as infrastructure for autonomous
+research. It includes a searchable problem atlas, pages for every registered
+problem variant and reduction, and an interactive vertex-cover / independent-set
+example. Current implementation capabilities and future research ambitions are
+explicitly distinguished.
+
+## Build and preview
+
+```sh
+make website
+python3 -m http.server 3001 --bind 127.0.0.1 --directory book
+```
+
+Open . `make doc` also builds Rust API documentation.
+The deployment workflow builds the PDF and API and combines everything in `book/`.
+The fast `make website` preview includes the guide; API/PDF links require those
+additional builds, as in deployment.
+
+For CSS/JavaScript iteration after the registry exports have been generated:
+
+```sh
+python3 scripts/build_website.py
+```
+
+The builder overlays the website's `index.html` and `assets/` onto mdBook's output.
+Existing documentation URLs, `introduction.html`, the paper, and Rust API paths
+stay available. Running `mdbook build` by itself restores mdBook's homepage; run
+the website builder afterward. The GitHub Pages workflow does this automatically.
+
+## Design and data
+
+- Deep forest surfaces, warm ivory text, and pale lime form the dark visual palette.
+- The header, footer, and favicon use the original `docs/logo.svg` artwork, recolored
+ at build time to match the dark palette. The canonical source logo stays unchanged.
+- Self-hosted DM Sans and Instrument Serif include their OFL licenses in `assets/fonts/`.
+- The graph is a generated SVG based on actual registry edges. Its homepage view
+ groups variants by problem family and does not imply that arbitrary paths compose.
+- Detail pages use exact variants. URLs encode problem names and variant keys,
+ rather than transient registry indices.
+- Counts, schemas, capabilities, and overhead expressions come from the same
+ generated JSON used by the documentation and paper. Nothing is manually counted.
+- The five-vertex example is illustrative; research activity, novelty, and live test
+ results are never fabricated. A reduction's registration does not imply formal proof.
+- Navigation, filters, search, clipboard actions, and the example are keyboard
+ accessible. Layouts adapt to mobile; motion respects reduced-motion preferences.
+- No frontend framework, third-party runtime, or external font request is required.
+
+The static website does not yet provide agent execution, an experiment database,
+or live research telemetry. The research section describes the intended loop and
+links to the existing agent workflows.
+
+## Browser checks
+
+Build the full documentation with `make doc` so API link checks have their targets,
+then run these commands with the preview server running:
+
+```sh
+uv run --no-project --with playwright python -m playwright install chromium
+uv run --no-project --with playwright python scripts/test_website.py
+```
+
+Set `WEBSITE_BROWSER_CHANNEL=chrome` to use an installed Chrome instead, or
+`WEBSITE_BASE_URL=http://localhost:3001/` to change the preview address. The suite
+exercises search, filters, exact variants, deep links, keyboard navigation,
+clipboard actions, the mathematical example, legacy docs, and mobile overflow.
+
+## Documentation
+
+The guide uses short task pages grouped in `docs/src/SUMMARY.md`: start here,
+agent workflows, CLI reference, Rust library, and internals. Keep one task or
+contract per page and link prerequisites and next steps. Agent prompts name the
+actual repository skill file; instructions distinguish implemented capabilities
+from the research goal.
+
+`docs/src/static/docs-theme.css` supplies the restrained dark reading theme;
+`docs-theme.js` adds Markdown access and redirects old section links. Native
+mdBook search, code copying, and sidebar navigation remain available. Both
+mdBook 0.4.37 (deployment) and 0.5.2 are supported.
+
+The website builder emits `book/markdown/` from the same source pages, expanding
+Rust and generated-output includes. The Markdown index is the entry point for
+agents. The builder preserves the Markdown index URL after mdBook’s HTML link rewriting.
+
+To check the complete assembled documentation, build the API and PDF first:
+
+```sh
+make doc
+make paper
+cp docs/paper/reductions.pdf book/reductions.pdf
+uv run --no-project --with playwright python scripts/test_documentation.py
+```
+
+The checks cover task navigation, search, clipboard, Markdown links and includes,
+legacy section redirects, mobile layout, offline playback, and replaying the
+recorded CLI workflow against its expected optimum.
+
+## CLI recording
+
+`docs/src/static/cli-demo.cast` contains real PTY output from six successful
+commands against the current CLI. `cli-demo.html` embeds that cast and
+asciinema-player 3.8.0 for offline playback, with autoplay disabled. The bundled
+player is Apache-2.0 licensed; its license is alongside the recording.
+
+To refresh the recording, use the `how-to-demo-cli` skill from
+[qude-software-skills](https://github.com/QudeLeap/qude-software-skills/tree/main/skills/how-to-demo-cli).
+Build the CLI, create an isolated temporary directory, and place a `pred` symlink
+to the new executable there. Record the commands in `docs/src/cli-demo.md`, using
+`./pred` in that directory, at 88 columns × 22 rows with `--theme nord`,
+`--typing-speed 35`, `--step-pause 2.5`, and `--no-autoplay`.
+
+Retain real output and exit codes; never substitute a simulated successful run.
+The checked-in HTML adds the documentation palette and a compact embedded mode
+to the skill's generated wrapper. Preserve those wrapper styles when refreshing.
diff --git a/docs/website/assets/fonts/DM-Sans-OFL.txt b/docs/website/assets/fonts/DM-Sans-OFL.txt
new file mode 100644
index 000000000..a0eedfbf0
--- /dev/null
+++ b/docs/website/assets/fonts/DM-Sans-OFL.txt
@@ -0,0 +1,93 @@
+Copyright 2014 The DM Sans Project Authors (https://github.com/googlefonts/dm-fonts)
+
+This Font Software is licensed under the SIL Open Font License, Version 1.1.
+This license is copied below, and is also available with a FAQ at:
+https://scripts.sil.org/OFL
+
+
+-----------------------------------------------------------
+SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
+-----------------------------------------------------------
+
+PREAMBLE
+The goals of the Open Font License (OFL) are to stimulate worldwide
+development of collaborative font projects, to support the font creation
+efforts of academic and linguistic communities, and to provide a free and
+open framework in which fonts may be shared and improved in partnership
+with others.
+
+The OFL allows the licensed fonts to be used, studied, modified and
+redistributed freely as long as they are not sold by themselves. The
+fonts, including any derivative works, can be bundled, embedded,
+redistributed and/or sold with any software provided that any reserved
+names are not used by derivative works. The fonts and derivatives,
+however, cannot be released under any other type of license. The
+requirement for fonts to remain under this license does not apply
+to any document created using the fonts or their derivatives.
+
+DEFINITIONS
+"Font Software" refers to the set of files released by the Copyright
+Holder(s) under this license and clearly marked as such. This may
+include source files, build scripts and documentation.
+
+"Reserved Font Name" refers to any names specified as such after the
+copyright statement(s).
+
+"Original Version" refers to the collection of Font Software components as
+distributed by the Copyright Holder(s).
+
+"Modified Version" refers to any derivative made by adding to, deleting,
+or substituting -- in part or in whole -- any of the components of the
+Original Version, by changing formats or by porting the Font Software to a
+new environment.
+
+"Author" refers to any designer, engineer, programmer, technical
+writer or other person who contributed to the Font Software.
+
+PERMISSION & CONDITIONS
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of the Font Software, to use, study, copy, merge, embed, modify,
+redistribute, and sell modified and unmodified copies of the Font
+Software, subject to the following conditions:
+
+1) Neither the Font Software nor any of its individual components,
+in Original or Modified Versions, may be sold by itself.
+
+2) Original or Modified Versions of the Font Software may be bundled,
+redistributed and/or sold with any software, provided that each copy
+contains the above copyright notice and this license. These can be
+included either as stand-alone text files, human-readable headers or
+in the appropriate machine-readable metadata fields within text or
+binary files as long as those fields can be easily viewed by the user.
+
+3) No Modified Version of the Font Software may use the Reserved Font
+Name(s) unless explicit written permission is granted by the corresponding
+Copyright Holder. This restriction only applies to the primary font name as
+presented to the users.
+
+4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
+Software shall not be used to promote, endorse or advertise any
+Modified Version, except to acknowledge the contribution(s) of the
+Copyright Holder(s) and the Author(s) or with their explicit written
+permission.
+
+5) The Font Software, modified or unmodified, in part or in whole,
+must be distributed entirely under this license, and must not be
+distributed under any other license. The requirement for fonts to
+remain under this license does not apply to any document created
+using the Font Software.
+
+TERMINATION
+This license becomes null and void if any of the above conditions are
+not met.
+
+DISCLAIMER
+THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
+OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
+COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
+DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
+OTHER DEALINGS IN THE FONT SOFTWARE.
diff --git a/docs/website/assets/fonts/Instrument-Serif-OFL.txt b/docs/website/assets/fonts/Instrument-Serif-OFL.txt
new file mode 100644
index 000000000..e1801b959
--- /dev/null
+++ b/docs/website/assets/fonts/Instrument-Serif-OFL.txt
@@ -0,0 +1,93 @@
+Copyright 2022 The Instrument Serif Project Authors (https://github.com/Instrument/instrument-serif)
+
+This Font Software is licensed under the SIL Open Font License, Version 1.1.
+This license is copied below, and is also available with a FAQ at:
+https://scripts.sil.org/OFL
+
+
+-----------------------------------------------------------
+SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
+-----------------------------------------------------------
+
+PREAMBLE
+The goals of the Open Font License (OFL) are to stimulate worldwide
+development of collaborative font projects, to support the font creation
+efforts of academic and linguistic communities, and to provide a free and
+open framework in which fonts may be shared and improved in partnership
+with others.
+
+The OFL allows the licensed fonts to be used, studied, modified and
+redistributed freely as long as they are not sold by themselves. The
+fonts, including any derivative works, can be bundled, embedded,
+redistributed and/or sold with any software provided that any reserved
+names are not used by derivative works. The fonts and derivatives,
+however, cannot be released under any other type of license. The
+requirement for fonts to remain under this license does not apply
+to any document created using the fonts or their derivatives.
+
+DEFINITIONS
+"Font Software" refers to the set of files released by the Copyright
+Holder(s) under this license and clearly marked as such. This may
+include source files, build scripts and documentation.
+
+"Reserved Font Name" refers to any names specified as such after the
+copyright statement(s).
+
+"Original Version" refers to the collection of Font Software components as
+distributed by the Copyright Holder(s).
+
+"Modified Version" refers to any derivative made by adding to, deleting,
+or substituting -- in part or in whole -- any of the components of the
+Original Version, by changing formats or by porting the Font Software to a
+new environment.
+
+"Author" refers to any designer, engineer, programmer, technical
+writer or other person who contributed to the Font Software.
+
+PERMISSION & CONDITIONS
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of the Font Software, to use, study, copy, merge, embed, modify,
+redistribute, and sell modified and unmodified copies of the Font
+Software, subject to the following conditions:
+
+1) Neither the Font Software nor any of its individual components,
+in Original or Modified Versions, may be sold by itself.
+
+2) Original or Modified Versions of the Font Software may be bundled,
+redistributed and/or sold with any software, provided that each copy
+contains the above copyright notice and this license. These can be
+included either as stand-alone text files, human-readable headers or
+in the appropriate machine-readable metadata fields within text or
+binary files as long as those fields can be easily viewed by the user.
+
+3) No Modified Version of the Font Software may use the Reserved Font
+Name(s) unless explicit written permission is granted by the corresponding
+Copyright Holder. This restriction only applies to the primary font name as
+presented to the users.
+
+4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
+Software shall not be used to promote, endorse or advertise any
+Modified Version, except to acknowledge the contribution(s) of the
+Copyright Holder(s) and the Author(s) or with their explicit written
+permission.
+
+5) The Font Software, modified or unmodified, in part or in whole,
+must be distributed entirely under this license, and must not be
+distributed under any other license. The requirement for fonts to
+remain under this license does not apply to any document created
+using the Font Software.
+
+TERMINATION
+This license becomes null and void if any of the above conditions are
+not met.
+
+DISCLAIMER
+THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
+OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
+COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
+DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
+OTHER DEALINGS IN THE FONT SOFTWARE.
diff --git a/docs/website/assets/fonts/dm-sans-regular.ttf b/docs/website/assets/fonts/dm-sans-regular.ttf
new file mode 100644
index 000000000..6c789eadb
Binary files /dev/null and b/docs/website/assets/fonts/dm-sans-regular.ttf differ
diff --git a/docs/website/assets/fonts/dm-sans-semibold.ttf b/docs/website/assets/fonts/dm-sans-semibold.ttf
new file mode 100644
index 000000000..ec5dcf3e2
Binary files /dev/null and b/docs/website/assets/fonts/dm-sans-semibold.ttf differ
diff --git a/docs/website/assets/fonts/instrument-serif-italic.ttf b/docs/website/assets/fonts/instrument-serif-italic.ttf
new file mode 100644
index 000000000..25d2a8219
Binary files /dev/null and b/docs/website/assets/fonts/instrument-serif-italic.ttf differ
diff --git a/docs/website/assets/fonts/instrument-serif.ttf b/docs/website/assets/fonts/instrument-serif.ttf
new file mode 100644
index 000000000..8794c6950
Binary files /dev/null and b/docs/website/assets/fonts/instrument-serif.ttf differ
diff --git a/docs/website/assets/site.css b/docs/website/assets/site.css
new file mode 100644
index 000000000..62442056f
--- /dev/null
+++ b/docs/website/assets/site.css
@@ -0,0 +1,1728 @@
+@font-face {
+ font-family: DM Sans;
+ src: url("./fonts/dm-sans-regular.ttf") format("truetype");
+ font-weight: 400;
+ font-style: normal;
+ font-display: swap;
+}
+@font-face {
+ font-family: DM Sans;
+ src: url("./fonts/dm-sans-semibold.ttf") format("truetype");
+ font-weight: 500 800;
+ font-style: normal;
+ font-display: swap;
+}
+@font-face {
+ font-family: Instrument Serif;
+ src: url("./fonts/instrument-serif.ttf") format("truetype");
+ font-weight: 400;
+ font-style: normal;
+ font-display: swap;
+}
+@font-face {
+ font-family: Instrument Serif;
+ src: url("./fonts/instrument-serif-italic.ttf") format("truetype");
+ font-weight: 400;
+ font-style: italic;
+ font-display: swap;
+}
+:root {
+ color-scheme: dark;
+ --surface: #162119;
+ --on-accent: #142016;
+ --graph-node: #83a570;
+ --diagram-selected: #c4dda6;
+ --diagram-line: #88a079;
+ --diagram-label: #c4d5b4;
+ --paper: #101713;
+ --ink: #e8ede5;
+ --muted: #a4b0a5;
+ --green: #c4dda6;
+ --line: #2c3b30;
+ --lime: #d5e9a7;
+ --pale: #1a271e;
+ --serif: "Instrument Serif", Georgia, serif;
+ --sans: "DM Sans", Arial, sans-serif;
+ --mono: ui-monospace, SFMono-Regular, Consolas, monospace;
+}
+* {
+ box-sizing: border-box;
+}
+html {
+ scroll-behavior: smooth;
+ scroll-padding-top: 100px;
+}
+body {
+ margin: 0;
+ background: var(--paper);
+ color: var(--ink);
+ font-family: var(--sans);
+ font-size: 15px;
+ line-height: 1.65;
+ -webkit-font-smoothing: antialiased;
+}
+/* Route changes focus the content container; controls retain visible focus rings. */
+#main:focus {
+ outline: none;
+}
+a {
+ color: inherit;
+ text-decoration: none;
+}
+button,
+input,
+select {
+ font: inherit;
+}
+button,
+a,
+input,
+select {
+ -webkit-tap-highlight-color: transparent;
+}
+button {
+ cursor: pointer;
+}
+button:disabled {
+ cursor: default;
+}
+button:focus-visible,
+a:focus-visible,
+input:focus-visible,
+select:focus-visible,
+summary:focus-visible {
+ outline: 3px solid var(--green);
+ outline-offset: 5px;
+}
+::selection {
+ background: var(--lime);
+ color: var(--on-accent);
+}
+button {
+ color: inherit;
+}
+img,
+svg {
+ max-width: 100%;
+}
+h1,
+h2,
+h3,
+p {
+ margin: 0;
+}
+h1,
+h2,
+h3 {
+ font-weight: 500;
+}
+h1,
+h2 {
+ letter-spacing: -0.055em;
+ line-height: 1.03;
+}
+h1 em,
+h2 em {
+ font-family: var(--serif);
+ font-weight: 400;
+ letter-spacing: -0.025em;
+}
+h2 {
+ font-size: clamp(38px, 4.1vw, 57px);
+}
+h3 {
+ font-size: 21px;
+ letter-spacing: -0.025em;
+ line-height: 1.3;
+}
+p {
+ color: var(--muted);
+}
+.wrap {
+ width: min(1280px, calc(100% - 112px));
+ margin-inline: auto;
+}
+.context-label {
+ font-family: var(--sans);
+ font-size: 12px;
+ font-weight: 400;
+ line-height: 1.5;
+}
+.site-header {
+ position: sticky;
+ top: 0;
+ z-index: 30;
+ background: rgba(16, 23, 19, 0.96);
+ border-bottom: 1px solid var(--line);
+ backdrop-filter: blur(16px);
+}
+.header-inner {
+ width: min(1392px, calc(100% - 64px));
+ height: 84px;
+ margin: auto;
+ display: flex;
+ align-items: center;
+ justify-content: space-between;
+ gap: 24px;
+}
+.wordmark {
+ display: inline-flex;
+ align-items: center;
+ gap: 10px;
+ white-space: nowrap;
+ font-size: 20px;
+ font-weight: 600;
+ letter-spacing: -1px;
+}
+.project-logo {
+ display: block;
+ width: 252px;
+ height: auto;
+}
+.site-footer .project-logo {
+ width: 224px;
+}
+.brand-period {
+ color: var(--green);
+}
+.site-header nav {
+ display: flex;
+ gap: 32px;
+ align-items: center;
+ font-size: 13px;
+}
+.site-header nav a {
+ color: var(--muted);
+ transition: color 0.2s;
+}
+.site-header nav a:hover,
+.site-header nav a[aria-current] {
+ color: var(--green);
+}
+.site-header nav a[aria-current] {
+ text-decoration: underline;
+ text-underline-offset: 9px;
+}
+.docs-nav span {
+ font-size: 12px;
+ margin-left: 3px;
+}
+.search-trigger {
+ display: flex;
+ align-items: center;
+ gap: 9px;
+ background: transparent;
+ border: 1px solid var(--line);
+ border-radius: 6px;
+ padding: 8px 10px;
+ color: var(--muted);
+ font-size: 12px;
+}
+.search-trigger kbd {
+ font-size: 10px;
+ color: var(--muted);
+ margin-left: 20px;
+}
+.hero {
+ display: grid;
+ grid-template-columns: 1fr 1.15fr;
+ gap: 40px;
+ align-items: center;
+ min-height: 700px;
+ padding-block: 74px 76px;
+}
+.hero-copy {
+ position: relative;
+ z-index: 2;
+}
+.status-dot {
+ width: 6px;
+ height: 6px;
+ display: inline-block;
+ background: #a3c879;
+ border-radius: 50%;
+ flex-shrink: 0;
+ box-shadow: 0 0 0 4px rgba(122, 153, 86, 0.09);
+}
+.hero h1 {
+ font-size: clamp(60px, 6vw, 84px);
+ line-height: 0.99;
+}
+.hero h1 em {
+ color: var(--green);
+}
+.hero-description {
+ margin-top: 26px;
+ font-size: 15px;
+ line-height: 1.75;
+ max-width: 430px;
+}
+.hero-actions {
+ display: flex;
+ align-items: center;
+ gap: 25px;
+ margin-top: 29px;
+ flex-wrap: wrap;
+}
+.button {
+ display: inline-flex;
+ justify-content: center;
+ align-items: center;
+ gap: 23px;
+ min-height: 46px;
+ padding: 12px 20px;
+ border: 1px solid var(--green);
+ border-radius: 5px;
+ font-size: 13px;
+ transition:
+ background 0.2s,
+ transform 0.2s;
+}
+.primary {
+ background: var(--green);
+ color: var(--on-accent);
+}
+.primary:hover {
+ background: #d7edbd;
+ transform: translateY(-2px);
+}
+.secondary {
+ background: transparent;
+}
+.secondary:hover {
+ background: var(--pale);
+}
+.text-link {
+ display: inline-flex;
+ align-items: center;
+ gap: 15px;
+ font-size: 13px;
+ font-weight: 500;
+}
+.text-link:hover {
+ color: #dfedce;
+}
+.hero-footnote {
+ display: flex;
+ align-items: center;
+ gap: 8px;
+ margin-top: 25px;
+ font-size: 10px;
+ color: var(--muted);
+}
+.tiny-node {
+ height: 7px;
+ width: 7px;
+ border: 1px solid #96aa8b;
+ border-radius: 2px;
+}
+.atlas-visual {
+ position: relative;
+ min-width: 0;
+ padding: 0 0 68px;
+ margin-right: -15px;
+}
+.visual-toolbar {
+ display: flex;
+ align-items: center;
+ justify-content: space-between;
+ padding: 15px 0;
+ border-top: 1px solid var(--line);
+ color: var(--muted);
+}
+.map-scale {
+ font-size: 11px;
+}
+.hero-graph {
+ height: 427px;
+ position: relative;
+ background-image: radial-gradient(#30432d 0.75px, transparent 0.75px);
+ background-size: 18px 18px;
+}
+.hero-graph svg {
+ width: 100%;
+ height: 100%;
+ overflow: visible;
+}
+.network-edge {
+ stroke: #698b5c;
+ stroke-width: 0.85;
+ opacity: 0.47;
+}
+.network-edge.featured-edge {
+ stroke: #c2de9b;
+ stroke-width: 2.4;
+ opacity: 1;
+}
+.network-node {
+ transition: opacity 0.2s;
+}
+.network-node circle {
+ fill: var(--graph-node);
+ stroke: var(--paper);
+ stroke-width: 2;
+ transition:
+ r 0.2s,
+ fill 0.2s;
+}
+.network-node:hover circle,
+.network-node:focus-visible circle {
+ fill: #d7edbd;
+ r: 8;
+}
+.network-node text {
+ font-size: 11px;
+ font-family: var(--sans);
+ fill: var(--diagram-label);
+ paint-order: stroke;
+ stroke: var(--paper);
+ stroke-width: 6px;
+ stroke-linejoin: round;
+ pointer-events: none;
+}
+.network-node.major circle {
+ fill: #b3d191;
+}
+.network-node.major text {
+ font-size: 12px;
+ fill: var(--diagram-label);
+}
+.network-node.focus circle {
+ fill: #d4eab6;
+ stroke: #446239;
+ stroke-width: 7;
+}
+.network-node.focus text {
+ font-weight: 600;
+ fill: #d4eab6;
+}
+.graph-caption {
+ font-size: 9px;
+ color: var(--muted);
+ display: flex;
+ justify-content: space-between;
+ align-items: center;
+ padding: 14px 0;
+ border-top: 1px solid var(--line);
+}
+.graph-caption > span {
+ display: flex;
+ align-items: center;
+ gap: 6px;
+}
+.legend-dot {
+ width: 5px;
+ height: 5px;
+ background: var(--green);
+ border-radius: 50%;
+ display: inline-block;
+}
+.graph-feature {
+ position: absolute;
+ left: 11%;
+ right: 3%;
+ bottom: 0;
+ display: flex;
+ align-items: center;
+ gap: 14px;
+ padding: 16px 19px;
+ background: var(--surface);
+ border: 1px solid var(--line);
+ border-radius: 6px;
+ box-shadow: 0 12px 35px #00000024;
+ transition: transform 0.2s;
+}
+.graph-feature:hover {
+ transform: translateY(-3px);
+}
+.feature-icon {
+ font-size: 25px;
+ color: var(--green);
+ width: 37px;
+ height: 37px;
+ text-align: center;
+ background: var(--pale);
+ border-radius: 4px;
+}
+.graph-feature strong {
+ font-size: 12px;
+ font-weight: 500;
+ display: block;
+}
+.graph-feature strong span {
+ margin-inline: 6px;
+ color: var(--muted);
+}
+.graph-feature > span:last-child {
+ margin-left: auto;
+}
+.stats-bar {
+ display: grid;
+ grid-template-columns: 1.4fr 1fr 1fr 1fr 1.1fr;
+ border-top: 1px solid var(--line);
+ border-bottom: 1px solid var(--line);
+ padding-block: 27px;
+ align-items: center;
+}
+.stats-bar > p {
+ font-size: 12px;
+ line-height: 1.6;
+}
+.stats-bar > p strong {
+ font-weight: 500;
+ color: var(--ink);
+}
+.stats-bar > div {
+ border-left: 1px solid var(--line);
+ padding-left: 32px;
+ display: flex;
+ flex-direction: column;
+}
+.stats-bar > div strong {
+ font-size: 32px;
+ letter-spacing: -1.6px;
+ line-height: 1.25;
+ font-weight: 400;
+}
+.stats-bar > div span {
+ font-size: 10px;
+ color: var(--muted);
+ margin-top: 5px;
+}
+.stats-bar > a {
+ font-size: 11px;
+ line-height: 1.7;
+ padding-left: 26px;
+ border-left: 1px solid var(--line);
+}
+.stats-bar > a span {
+ margin-left: 16px;
+}
+.section {
+ padding-block: 98px;
+}
+.section-heading {
+ display: grid;
+ grid-template-columns: 1.2fr 1fr;
+ gap: 80px;
+ align-items: end;
+ margin-bottom: 44px;
+}
+.section-heading > p,
+.section-heading > div > p {
+ max-width: 405px;
+ font-size: 14px;
+ line-height: 1.85;
+}
+.problem-showcase {
+ display: grid;
+ grid-template-columns: repeat(3, 1fr);
+ border: 1px solid var(--line);
+ border-radius: 7px;
+ overflow: hidden;
+}
+.problem-card {
+ display: block;
+ padding: 29px 28px 25px;
+ position: relative;
+ transition: background 0.2s;
+}
+.problem-card + .problem-card {
+ border-left: 1px solid var(--line);
+}
+.problem-card:hover {
+ background: var(--pale);
+}
+.problem-card .context-label {
+ font-size: 12px;
+ color: var(--muted);
+}
+.problem-card h3 {
+ font-size: 23px;
+ margin-top: 17px;
+ margin-bottom: 11px;
+}
+.problem-card p {
+ font-size: 12px;
+ line-height: 1.8;
+ min-height: 44px;
+ max-width: 290px;
+}
+.problem-card .mini-art {
+ height: 112px;
+ margin-block: 18px;
+}
+.problem-card .mini-art svg {
+ width: 100%;
+ height: 100%;
+}
+.card-bottom {
+ border-top: 1px solid var(--line);
+ padding-top: 17px;
+ margin-top: 22px;
+ display: flex;
+ justify-content: space-between;
+ align-items: center;
+ font-size: 10px;
+ color: var(--muted);
+}
+.card-bottom span:last-child {
+ font-size: 20px;
+ color: var(--green);
+}
+.section-bottom {
+ display: flex;
+ justify-content: space-between;
+ gap: 25px;
+ margin-top: 24px;
+ color: var(--muted);
+ font-size: 11px;
+}
+.research-section {
+ background: #1a3023;
+ color: var(--ink);
+ padding-block: 85px;
+}
+.research-section h2 em {
+ color: var(--lime);
+}
+.research-section p {
+ color: #b5c5b2;
+}
+.research-cycle {
+ display: grid;
+ grid-template-columns: repeat(4, 1fr);
+ border-top: 1px solid #3a513d;
+ border-bottom: 1px solid #3a513d;
+ margin-top: 55px;
+}
+.research-cycle article {
+ padding: 29px 25px 27px 0;
+}
+.research-cycle article + article {
+ padding-left: 25px;
+ border-left: 1px solid #3a513d;
+}
+.research-cycle h3 {
+ font-size: 18px;
+ margin-bottom: 14px;
+}
+.research-cycle p {
+ font-size: 12px;
+ line-height: 1.85;
+}
+.research-note {
+ display: flex;
+ align-items: baseline;
+ gap: 12px;
+ padding-top: 25px;
+}
+.research-note p {
+ font-size: 10px;
+ max-width: 690px;
+}
+.research-note strong {
+ font-weight: 500;
+ color: var(--ink);
+}
+.research-note a {
+ font-size: 10px;
+ white-space: nowrap;
+ margin-left: auto;
+}
+.featured-result {
+ display: grid;
+ grid-template-columns: 1fr 1.2fr;
+ background: var(--pale);
+ border: 1px solid var(--line);
+ border-radius: 8px;
+ overflow: hidden;
+ transition: border-color 0.2s;
+}
+.featured-result:hover {
+ border-color: #7e9e65;
+}
+.featured-copy {
+ padding: 41px;
+}
+.pill {
+ display: inline-block;
+ border: 1px solid #4b6240;
+ color: #c6dcae;
+ background: #22331f;
+ padding: 5px 8px;
+ border-radius: 4px;
+ font-size: 11px;
+}
+.featured-copy h3 {
+ font-size: 33px;
+ line-height: 1.18;
+ letter-spacing: -1.2px;
+ margin: 23px 0 17px;
+}
+.featured-copy p {
+ font-size: 12px;
+ max-width: 335px;
+ line-height: 1.85;
+}
+.featured-copy .text-link {
+ margin-top: 25px;
+}
+.complement-art {
+ display: flex;
+ align-items: center;
+ justify-content: center;
+ border-left: 1px solid var(--line);
+ padding: 25px;
+}
+.complement-art svg {
+ width: 100%;
+}
+.infrastructure-section {
+ padding-block: 40px 104px;
+ display: grid;
+ grid-template-columns: 1fr 1fr;
+ gap: 70px;
+ align-items: center;
+}
+.infrastructure-section p {
+ font-size: 13px;
+ line-height: 1.9;
+ margin-top: 23px;
+}
+.terminal {
+ background: var(--surface);
+ border: 1px solid var(--line);
+ border-radius: 7px;
+ overflow: hidden;
+ box-shadow: 0 10px 25px #00000024;
+}
+.terminal-header {
+ display: flex;
+ justify-content: space-between;
+ align-items: center;
+ gap: 10px;
+ padding: 14px 20px;
+ border-bottom: 1px solid var(--line);
+ font-family: var(--mono);
+ font-size: 8px;
+ color: var(--muted);
+}
+.terminal-header > span:first-child {
+ display: flex;
+ gap: 5px;
+}
+.terminal-header i {
+ width: 6px;
+ height: 6px;
+ border-radius: 50%;
+ background: #556e4c;
+}
+.code-panel .terminal-header {
+ justify-content: flex-end;
+}
+.copy-button {
+ border: 0;
+ background: transparent;
+ color: var(--green);
+ font-size: 10px;
+ padding: 4px 7px;
+}
+.copy-button:hover {
+ background: var(--pale);
+}
+pre {
+ white-space: pre-wrap;
+ overflow-wrap: anywhere;
+ font-family: var(--mono);
+ line-height: 1.85;
+ font-size: 12px;
+ margin: 0;
+}
+.terminal pre {
+ padding: 26px;
+ color: #c0d7ad;
+ font-size: 11px;
+}
+.terminal-comment {
+ color: var(--muted);
+}
+.terminal-prompt {
+ color: #a1bd87;
+}
+.terminal > a {
+ display: flex;
+ justify-content: space-between;
+ padding: 13px 22px;
+ border-top: 1px solid var(--line);
+ font-size: 10px;
+ background: #19271d;
+}
+.site-footer {
+ border-top: 1px solid var(--line);
+ padding-block: 36px;
+ display: flex;
+ justify-content: space-between;
+ gap: 30px;
+ align-items: center;
+}
+.site-footer .wordmark {
+ font-size: 16px;
+}
+.site-footer p {
+ font-size: 10px;
+ margin-top: 8px;
+}
+.site-footer > div:last-child {
+ display: flex;
+ gap: 24px;
+ font-size: 10px;
+}
+.site-footer > div:last-child > span {
+ color: var(--muted);
+}
+.skip-link {
+ position: fixed;
+ top: -70px;
+ left: 20px;
+ z-index: 99;
+ background: var(--green);
+ color: var(--on-accent);
+ padding: 10px 20px;
+}
+.skip-link:focus {
+ top: 10px;
+}
+.toast {
+ position: fixed;
+ bottom: 24px;
+ left: 50%;
+ transform: translate(-50%, 20px);
+ background: var(--green);
+ color: var(--on-accent);
+ padding: 10px 20px;
+ font-size: 13px;
+ border-radius: 5px;
+ opacity: 0;
+ pointer-events: none;
+ transition:
+ opacity 0.2s,
+ transform 0.2s;
+ z-index: 50;
+}
+.toast.visible {
+ opacity: 1;
+ transform: translate(-50%, 0);
+}
+/* Atlas and scientific reading views share the same spacing and type system. */
+.page-header {
+ padding-top: 65px;
+ padding-bottom: 40px;
+}
+.breadcrumbs {
+ display: flex;
+ flex-wrap: wrap;
+ gap: 10px;
+ font-size: 11px;
+ color: var(--muted);
+ margin-bottom: 29px;
+}
+.breadcrumbs a:hover {
+ text-decoration: underline;
+}
+.page-header .pill {
+ margin-bottom: 20px;
+}
+.page-header h1 {
+ font-size: clamp(42px, 5vw, 65px);
+ max-width: 960px;
+ overflow-wrap: anywhere;
+}
+.page-header > p {
+ font-size: 15px;
+ max-width: 680px;
+ line-height: 1.8;
+ margin-top: 20px;
+}
+.atlas-controls {
+ display: flex;
+ align-items: center;
+ justify-content: space-between;
+ gap: 20px;
+ margin-top: 33px;
+}
+.atlas-search {
+ display: flex;
+ align-items: center;
+ gap: 12px;
+ border: 1px solid #42573b;
+ border-radius: 5px;
+ background: var(--surface);
+ padding: 12px 17px;
+ width: 420px;
+}
+.atlas-search input {
+ min-width: 0;
+ width: 100%;
+ border: 0;
+ background: transparent;
+ outline: none;
+ font-size: 13px;
+}
+.atlas-search:focus-within {
+ outline: 2px solid var(--green);
+ outline-offset: 2px;
+}
+.atlas-search input:focus-visible {
+ outline: none;
+}
+.result-count {
+ font-family: var(--mono);
+ font-size: 10px;
+ color: var(--muted);
+}
+.atlas-layout {
+ display: grid;
+ grid-template-columns: 180px 1fr;
+ gap: 40px;
+ padding-bottom: 80px;
+}
+.filters {
+ border-top: 1px solid var(--line);
+ padding-top: 21px;
+ align-self: start;
+ position: sticky;
+ top: 110px;
+}
+.filters .context-label {
+ margin-bottom: 13px;
+ color: var(--muted);
+}
+.filter-button {
+ display: flex;
+ justify-content: space-between;
+ align-items: center;
+ gap: 10px;
+ width: 100%;
+ padding: 10px 12px;
+ border: 0;
+ border-radius: 4px;
+ text-align: left;
+ background: transparent;
+ color: var(--muted);
+ font-size: 12px;
+ margin-block: 3px;
+}
+.filter-button[aria-pressed="true"] {
+ background: #2a3e26;
+ color: var(--green);
+}
+.filter-button:hover {
+ background: var(--pale);
+}
+.filter-button span:last-child {
+ font-family: var(--mono);
+ font-size: 9px;
+}
+.atlas-results {
+ border-top: 1px solid var(--line);
+}
+.atlas-row {
+ display: grid;
+ grid-template-columns: 1fr auto;
+ gap: 24px;
+ padding: 25px 20px;
+ border-bottom: 1px solid var(--line);
+ transition: background 0.2s;
+}
+.atlas-row:hover {
+ background: var(--pale);
+}
+.atlas-row h2 {
+ font-size: 21px;
+ letter-spacing: -0.04em;
+ line-height: 1.35;
+ overflow-wrap: anywhere;
+}
+.atlas-row p {
+ font-size: 12px;
+ margin-top: 8px;
+ max-width: 650px;
+}
+.atlas-row-meta {
+ display: flex;
+ gap: 15px;
+ margin-top: 13px;
+ font-family: var(--mono);
+ font-size: 9px;
+ color: var(--muted);
+}
+.atlas-row > span {
+ align-self: center;
+ font-size: 24px;
+}
+.empty-state {
+ padding: 60px 20px;
+}
+.empty-state h2 {
+ font-size: 30px;
+ margin-bottom: 14px;
+}
+.empty-state p {
+ font-size: 13px;
+}
+.empty-state button {
+ margin-top: 22px;
+}
+.reading-layout {
+ display: grid;
+ grid-template-columns: minmax(0, 1fr) 290px;
+ gap: 70px;
+ padding-bottom: 90px;
+}
+.reading-content {
+ min-width: 0;
+}
+.reading-section {
+ padding-block: 32px;
+ border-top: 1px solid var(--line);
+}
+.reading-section h2 {
+ font-size: 27px;
+ letter-spacing: -0.035em;
+ line-height: 1.2;
+ margin-bottom: 17px;
+}
+.reading-section > p {
+ font-size: 14px;
+ line-height: 1.85;
+ margin-block: 15px;
+ max-width: 730px;
+}
+.reading-section h3 {
+ font-size: 18px;
+ margin: 25px 0 13px;
+}
+.formula {
+ background: var(--pale);
+ padding: 27px;
+ border-left: 2px solid var(--green);
+ font-family: var(--serif);
+ font-size: 27px;
+ color: var(--green);
+ line-height: 1.5;
+ margin-block: 23px;
+}
+.formula small {
+ display: block;
+ font-family: var(--sans);
+ font-size: 11px;
+ color: var(--muted);
+ margin-top: 8px;
+}
+.reading-aside {
+ align-self: start;
+ position: sticky;
+ top: 112px;
+ background: var(--pale);
+ border: 1px solid var(--line);
+ border-radius: 6px;
+ padding: 25px;
+}
+.metadata {
+ margin: 21px 0 24px;
+}
+.metadata > div {
+ padding-block: 13px;
+ border-bottom: 1px solid var(--line);
+}
+.metadata dt {
+ font-size: 10px;
+ color: var(--muted);
+ margin-bottom: 4px;
+}
+.metadata dd {
+ margin: 0;
+ font-size: 12px;
+ overflow-wrap: anywhere;
+}
+.reading-aside > a {
+ display: flex;
+ justify-content: space-between;
+ font-size: 12px;
+ margin-top: 15px;
+}
+.reading-aside > a:hover {
+ text-decoration: underline;
+}
+.reading-aside p {
+ font-size: 10px;
+ margin-top: 20px;
+ line-height: 1.8;
+}
+.variant-control {
+ display: flex;
+ flex-wrap: wrap;
+ gap: 13px;
+ align-items: center;
+ margin-top: 25px;
+ font-size: 11px;
+ color: var(--muted);
+}
+.variant-control select {
+ max-width: 100%;
+ padding: 10px;
+ border: 1px solid var(--line);
+ border-radius: 4px;
+ background: var(--surface);
+ color: var(--ink);
+ font-size: 11px;
+}
+.variant-tags {
+ display: flex;
+ flex-wrap: wrap;
+ gap: 6px;
+ margin-top: 18px;
+}
+.variant-tag {
+ border: 1px solid var(--line);
+ border-radius: 3px;
+ padding: 4px 8px;
+ font-family: var(--mono);
+ font-size: 9px;
+ color: var(--muted);
+}
+.relation-link {
+ display: block;
+ border: 1px solid var(--line);
+ border-radius: 5px;
+ padding: 17px;
+ margin-bottom: 10px;
+ background: var(--surface);
+ transition: border-color 0.2s;
+}
+.relation-link:hover {
+ border-color: #89a76e;
+}
+.relation-title {
+ display: flex;
+ align-items: center;
+ justify-content: space-between;
+ gap: 15px;
+ font-size: 13px;
+ font-weight: 500;
+}
+.relation-link p {
+ font-family: var(--mono);
+ font-size: 9px;
+ margin-top: 7px;
+ overflow-wrap: anywhere;
+}
+.relation-link .capability {
+ font-family: var(--sans);
+ font-size: 10px;
+}
+.schema-table {
+ width: 100%;
+ border-collapse: collapse;
+ font-size: 12px;
+}
+.schema-table th {
+ text-align: left;
+ font-size: 10px;
+ color: var(--muted);
+ font-weight: 400;
+ padding: 10px 10px 10px 0;
+ border-bottom: 1px solid var(--line);
+}
+.schema-table td {
+ padding: 13px 10px 13px 0;
+ vertical-align: top;
+ border-bottom: 1px solid var(--line);
+ overflow-wrap: anywhere;
+}
+.schema-table code {
+ font-size: 11px;
+ word-break: break-word;
+}
+.table-scroll {
+ overflow: auto;
+}
+.code-panel {
+ border: 1px solid var(--line);
+ background: var(--surface);
+ border-radius: 5px;
+ overflow: hidden;
+ margin-top: 20px;
+}
+.code-panel pre {
+ padding: 22px;
+}
+.evidence-grid {
+ display: grid;
+ grid-template-columns: 1fr 1fr;
+ gap: 12px;
+ margin-top: 25px;
+}
+.evidence-item {
+ border: 1px solid var(--line);
+ border-radius: 5px;
+ padding: 20px;
+}
+.evidence-item h3 {
+ font-size: 14px;
+ margin: 12px 0 7px;
+}
+.evidence-item p {
+ font-size: 11px;
+ line-height: 1.8;
+}
+.evidence-item .context-label {
+ font-size: 12px;
+}
+.evidence-item a {
+ display: inline-block;
+ font-size: 11px;
+ margin-top: 12px;
+ text-decoration: underline;
+ text-underline-offset: 4px;
+}
+.demo-panel {
+ border: 1px solid var(--line);
+ background: var(--pale);
+ border-radius: 6px;
+ overflow: hidden;
+ margin-top: 25px;
+}
+.demo-toolbar {
+ padding: 16px 20px;
+ display: flex;
+ justify-content: space-between;
+ align-items: center;
+ gap: 15px;
+ border-bottom: 1px solid var(--line);
+ font-size: 11px;
+}
+.segmented {
+ display: flex;
+ background: #111c14;
+ padding: 3px;
+ border-radius: 5px;
+}
+.segmented button {
+ border: 0;
+ background: transparent;
+ border-radius: 3px;
+ padding: 7px 12px;
+ font-size: 10px;
+}
+.segmented button[aria-pressed="true"] {
+ background: var(--green);
+ color: var(--on-accent);
+ box-shadow: 0 1px 4px #00000020;
+}
+.demo-panel svg {
+ display: block;
+ max-height: 290px;
+ width: 100%;
+ padding: 20px;
+}
+.demo-caption {
+ display: flex;
+ justify-content: space-between;
+ align-items: center;
+ gap: 15px;
+ padding: 16px 20px;
+ border-top: 1px solid var(--line);
+ font-size: 11px;
+ color: var(--muted);
+}
+.demo-caption strong {
+ color: var(--green);
+ font-weight: 500;
+}
+.notice {
+ font-size: 11px;
+ line-height: 1.85;
+ color: var(--muted);
+ border-left: 2px solid #799461;
+ padding-left: 15px;
+ margin-top: 24px;
+}
+.reading-content details {
+ border-bottom: 1px solid var(--line);
+ padding-block: 15px;
+}
+.reading-content summary {
+ cursor: pointer;
+ font-size: 13px;
+ font-weight: 500;
+}
+.reading-content details p {
+ font-size: 12px;
+ line-height: 1.9;
+ padding-block: 15px;
+}
+.page-enter {
+ animation: page-enter 0.3s ease-out;
+}
+@keyframes page-enter {
+ from {
+ opacity: 0.5;
+ transform: translateY(6px);
+ }
+ to {
+ opacity: 1;
+ transform: translateY(0);
+ }
+}
+@media (min-width: 1600px) {
+ .hero {
+ min-height: 770px;
+ }
+ .hero h1 {
+ font-size: 91px;
+ }
+ .hero-graph {
+ height: 465px;
+ }
+}
+@media (max-width: 1100px) {
+ .wrap {
+ width: calc(100% - 64px);
+ }
+ .header-inner {
+ height: 74px;
+ }
+ .site-header nav {
+ gap: 20px;
+ }
+ .wordmark {
+ font-size: 17px;
+ }
+ .search-trigger kbd {
+ margin-left: 4px;
+ }
+ .hero {
+ gap: 18px;
+ min-height: 620px;
+ padding-block: 60px;
+ }
+ .hero h1 {
+ font-size: 66px;
+ }
+ .hero-graph {
+ height: 380px;
+ }
+ .hero-description {
+ font-size: 14px;
+ }
+ .hero-footnote {
+ font-size: 9px;
+ }
+ .hero-actions {
+ gap: 18px;
+ }
+ .graph-feature {
+ left: 2%;
+ right: 0;
+ padding: 14px;
+ }
+ .graph-feature strong {
+ font-size: 10px;
+ }
+ .section-heading {
+ gap: 50px;
+ }
+ .reading-layout {
+ gap: 35px;
+ grid-template-columns: minmax(0, 1fr) 260px;
+ }
+ .infrastructure-section {
+ gap: 35px;
+ }
+ .site-footer > div:last-child {
+ gap: 15px;
+ }
+}
+@media (max-width: 800px) {
+ .header-inner {
+ width: calc(100% - 40px);
+ gap: 14px;
+ flex-wrap: wrap;
+ height: auto;
+ min-height: 108px;
+ padding-block: 16px;
+ row-gap: 15px;
+ }
+ .site-header nav {
+ order: 3;
+ width: 100%;
+ justify-content: center;
+ gap: 35px;
+ font-size: 12px;
+ }
+ .search-trigger {
+ margin-left: auto;
+ }
+ .search-trigger kbd {
+ display: none;
+ }
+ .wrap {
+ width: calc(100% - 48px);
+ }
+ .hero {
+ grid-template-columns: 1fr;
+ padding-block: 50px 40px;
+ gap: 50px;
+ }
+ .hero h1 {
+ font-size: 74px;
+ }
+ .hero h1 br.desktop-break {
+ display: none;
+ }
+ .hero-description {
+ font-size: 15px;
+ }
+ .hero-copy {
+ max-width: 600px;
+ }
+ .hero-footnote {
+ font-size: 10px;
+ }
+ .atlas-visual {
+ margin: 0;
+ max-width: 600px;
+ width: 100%;
+ justify-self: center;
+ }
+ .hero-graph {
+ height: 360px;
+ }
+ .graph-feature {
+ left: 15%;
+ right: 0;
+ }
+ .stats-bar {
+ grid-template-columns: repeat(3, 1fr);
+ gap: 20px 0;
+ }
+ .stats-bar > p {
+ grid-column: 1/-1;
+ display: flex;
+ gap: 5px;
+ }
+ .stats-bar > p br {
+ display: none;
+ }
+ .stats-bar > div {
+ padding-left: 20px;
+ }
+ .stats-bar > div:nth-child(2) {
+ border: 0;
+ padding-left: 0;
+ }
+ .stats-bar > a {
+ display: none;
+ }
+ .section {
+ padding-block: 65px;
+ }
+ .section-heading {
+ grid-template-columns: 1fr;
+ gap: 25px;
+ margin-bottom: 30px;
+ }
+ .section-heading > p,
+ .section-heading > div > p {
+ max-width: 550px;
+ }
+ .problem-showcase {
+ grid-template-columns: 1fr;
+ }
+ .problem-card + .problem-card {
+ border-left: 0;
+ border-top: 1px solid var(--line);
+ }
+ .problem-card {
+ padding: 25px;
+ display: grid;
+ grid-template-columns: 1fr 130px;
+ gap: 0 15px;
+ }
+ .problem-card .context-label,
+ .problem-card h3,
+ .problem-card p {
+ grid-column: 1;
+ }
+ .problem-card h3 {
+ font-size: 23px;
+ margin-top: 12px;
+ }
+ .problem-card .mini-art {
+ grid-column: 2;
+ grid-row: 1/4;
+ height: 120px;
+ align-self: center;
+ margin: 0;
+ }
+ .problem-card p {
+ min-height: 0;
+ }
+ .card-bottom {
+ grid-column: 1/-1;
+ margin-top: 20px;
+ }
+ .research-section {
+ padding-block: 65px;
+ }
+ .research-cycle {
+ grid-template-columns: 1fr 1fr;
+ margin-top: 35px;
+ }
+ .research-cycle article {
+ padding: 24px !important;
+ }
+ .research-cycle article:nth-child(odd) {
+ padding-left: 0 !important;
+ border-left: 0;
+ }
+ .research-cycle article:nth-child(n + 3) {
+ border-top: 1px solid #3a513d;
+ }
+ .research-note {
+ flex-wrap: wrap;
+ }
+ .research-note p {
+ flex: 1;
+ font-size: 11px;
+ }
+ .research-note a {
+ width: 100%;
+ margin-left: 18px;
+ }
+ .featured-result {
+ grid-template-columns: 1fr;
+ }
+ .featured-copy {
+ padding: 30px;
+ }
+ .featured-copy p {
+ max-width: 480px;
+ }
+ .complement-art {
+ border-left: 0;
+ border-top: 1px solid var(--line);
+ min-height: 230px;
+ }
+ .complement-art svg {
+ max-width: 550px;
+ }
+ .infrastructure-section {
+ grid-template-columns: 1fr;
+ gap: 35px;
+ padding-block: 15px 65px;
+ }
+ .terminal {
+ max-width: 600px;
+ }
+ .site-footer {
+ flex-direction: column;
+ align-items: flex-start;
+ }
+ .site-footer > div:last-child {
+ flex-wrap: wrap;
+ gap: 22px;
+ }
+ .atlas-layout {
+ grid-template-columns: 1fr;
+ gap: 20px;
+ }
+ .filters {
+ position: static;
+ display: flex;
+ flex-wrap: wrap;
+ gap: 6px;
+ }
+ .filters .context-label {
+ width: 100%;
+ margin-bottom: 5px;
+ }
+ .filter-button {
+ width: auto;
+ gap: 15px;
+ font-size: 11px;
+ border: 1px solid var(--line);
+ }
+ .reading-layout {
+ grid-template-columns: 1fr;
+ }
+ .reading-aside {
+ position: static;
+ order: -1;
+ padding: 20px;
+ }
+ .metadata {
+ display: flex;
+ flex-wrap: wrap;
+ gap: 12px 30px;
+ margin: 10px 0;
+ }
+ .metadata > div {
+ border: 0;
+ padding-block: 4px;
+ }
+ .reading-aside > a {
+ display: inline-flex;
+ gap: 20px;
+ margin: 10px 20px 0 0;
+ }
+ .reading-aside p {
+ margin-top: 12px;
+ }
+ .page-header {
+ padding-top: 40px;
+ }
+ .page-header h1 {
+ font-size: 48px;
+ }
+ .page-header > p {
+ font-size: 14px;
+ }
+ .atlas-controls {
+ align-items: flex-start;
+ flex-direction: column;
+ gap: 12px;
+ }
+ .atlas-search {
+ width: 100%;
+ }
+ .atlas-row {
+ padding-inline: 5px;
+ }
+ .section-bottom {
+ font-size: 10px;
+ }
+ .section-bottom .text-link {
+ font-size: 11px;
+ }
+ .desktop-break {
+ display: none;
+ }
+ html {
+ scroll-padding-top: 135px;
+ }
+}
+@media (max-width: 420px) {
+ .wrap {
+ width: calc(100% - 36px);
+ }
+ .header-inner {
+ width: calc(100% - 32px);
+ }
+ .wordmark {
+ font-size: 16px;
+ gap: 7px;
+ }
+ .wordmark .project-logo {
+ width: 208px;
+ }
+ .site-header nav {
+ gap: 25px;
+ font-size: 11px;
+ }
+ .search-trigger {
+ padding: 7px;
+ }
+ .search-trigger > span {
+ display: none;
+ }
+ .hero h1 {
+ font-size: 61px;
+ }
+ .hero-description {
+ font-size: 14px;
+ }
+ .hero-actions {
+ gap: 20px;
+ }
+ .button {
+ padding: 11px 16px;
+ font-size: 12px;
+ }
+ .hero-actions .text-link {
+ font-size: 12px;
+ }
+ .hero-footnote {
+ font-size: 8px;
+ }
+ .hero-graph {
+ height: 310px;
+ }
+ .graph-feature {
+ left: 0;
+ }
+ .stats-bar > div strong {
+ font-size: 28px;
+ }
+ .stats-bar > div span {
+ font-size: 9px;
+ }
+ .problem-card {
+ grid-template-columns: 1fr 85px;
+ padding: 22px;
+ }
+ .problem-card h3 {
+ font-size: 21px;
+ }
+ .problem-card p {
+ font-size: 11px;
+ }
+ .research-cycle article {
+ padding: 22px 16px !important;
+ }
+ .research-cycle h3 {
+ font-size: 16px;
+ }
+ .research-cycle p {
+ font-size: 11px;
+ }
+ .evidence-grid {
+ grid-template-columns: 1fr;
+ }
+ .demo-toolbar {
+ flex-direction: column;
+ align-items: flex-start;
+ }
+ .demo-caption {
+ align-items: flex-start;
+ flex-direction: column;
+ gap: 4px;
+ }
+ .section-bottom {
+ flex-direction: column;
+ gap: 10px;
+ }
+ .page-header h1 {
+ font-size: 40px;
+ }
+ .variant-control select {
+ width: 100%;
+ }
+ .formula {
+ font-size: 23px;
+ padding: 20px;
+ }
+}
+@media (prefers-reduced-motion: reduce) {
+ html {
+ scroll-behavior: auto;
+ }
+ *,
+ *::before,
+ *::after {
+ animation: none !important;
+ transition: none !important;
+ }
+}
diff --git a/docs/website/assets/site.js b/docs/website/assets/site.js
new file mode 100644
index 000000000..651bd079e
--- /dev/null
+++ b/docs/website/assets/site.js
@@ -0,0 +1,708 @@
+/* The site is a static client of the same registry exports as the book and paper. */
+(() => {
+ "use strict";
+ const data = window.REDUCTIONS;
+ const main = document.querySelector("main");
+ const homeHTML = main.innerHTML;
+ const baseTitle = "Problem Reductions";
+ const repo = "https://github.com/CodingThrust/problem-reductions";
+ const categories = {
+ graph: "Graph theory",
+ formula: "Logic & formulas",
+ set: "Set systems",
+ algebraic: "Algebra",
+ misc: "Other structures",
+ };
+ const aliases = {
+ MIS: "MaximumIndependentSet",
+ MVC: "MinimumVertexCover",
+ SAT: "Satisfiability",
+ "3SAT": "KSatisfiability",
+ "3-SAT": "KSatisfiability",
+ };
+ let filter = "all";
+ let query = "";
+ let toastTimer;
+ let focusSearchAfterNavigation = false;
+ const escape = (value) =>
+ String(value ?? "").replace(
+ /[&<>"']/g,
+ (c) =>
+ ({
+ "&": "&",
+ "<": "<",
+ ">": ">",
+ '"': """,
+ "'": "'",
+ })[c],
+ );
+ const nameOf = (name) =>
+ data.schemas.find((s) => s.name === name)?.display_name ||
+ name
+ .replace(/([a-z0-9])([A-Z])/g, "$1 $2")
+ .replace(/([A-Z])([A-Z][a-z])/g, "$1 $2");
+ const variantKey = (node) =>
+ Object.entries(node.variant)
+ .sort(([a], [b]) => a.localeCompare(b))
+ .map(([k, v]) => `${k}=${v}`)
+ .join(",");
+ const variantLabel = (node) =>
+ Object.entries(node.variant)
+ .map(([k, v]) => `${k}: ${v}`)
+ .join(" · ") || "Default variant";
+ const problemHref = (name, node) =>
+ `#problem/${encodeURIComponent(name)}${node ? `?variant=${encodeURIComponent(variantKey(node))}` : ""}`;
+ const ruleHref = (edge) =>
+ `#reduction/${encodeURIComponent(data.nodes[edge.source].name)}/${encodeURIComponent(data.nodes[edge.target].name)}?from=${encodeURIComponent(variantKey(data.nodes[edge.source]))}&to=${encodeURIComponent(variantKey(data.nodes[edge.target]))}`;
+ const schemaOf = (name) => data.schemas.find((s) => s.name === name);
+ const description = (name) =>
+ schemaOf(name)?.description ||
+ "Explore the registered variants, reduction contracts, and implementation of this computational problem.";
+ const apiHref = (path) => `./api/problemreductions/${path}`;
+ const moduleName = (edge) => edge.doc_path.split("/").at(-2);
+ const sourceHref = (edge) => `${repo}/blob/main/${edge.source_path}`;
+ const families = [...new Set(data.nodes.map((n) => n.name))].sort();
+ const variantsOf = (name) =>
+ data.nodes
+ .map((n, i) => ({ ...n, index: i }))
+ .filter((n) => n.name === name);
+ const edgesOf = (name) =>
+ data.edges.filter(
+ (e) =>
+ data.nodes[e.source].name === name ||
+ data.nodes[e.target].name === name,
+ );
+ const featuredEdge = data.edges.find(
+ (e) =>
+ data.nodes[e.source].name === "MinimumVertexCover" &&
+ data.nodes[e.target].name === "MaximumIndependentSet",
+ );
+
+ function notify(message) {
+ const toast = document.querySelector(".toast");
+ toast.textContent = message;
+ toast.classList.add("visible");
+ clearTimeout(toastTimer);
+ toastTimer = setTimeout(() => toast.classList.remove("visible"), 2800);
+ }
+
+ function graphArt() {
+ const width = 630,
+ height = 430;
+ const highlights = {
+ MaximumIndependentSet: [310, 242, "Independent Set"],
+ MinimumVertexCover: [452, 155, "Vertex Cover"],
+ Satisfiability: [145, 162, "Satisfiability"],
+ KSatisfiability: [220, 74, "k-SAT"],
+ MaximumSetPacking: [449, 314, "Set Packing"],
+ QUBO: [158, 335, "QUBO"],
+ ILP: [330, 370, "ILP"],
+ Coloring: [92, 249, "Coloring"],
+ };
+ const positions = {};
+ families.forEach((name, i) => {
+ const angle = i * 2.39996323;
+ const radius = Math.sqrt((i + 1) / families.length);
+ positions[name] = highlights[name] || [
+ 315 + Math.cos(angle) * radius * 287,
+ 218 + Math.sin(angle) * radius * 191,
+ ];
+ });
+ const seen = new Set();
+ const lines = data.edges
+ .map((e) => {
+ const from = data.nodes[e.source].name,
+ to = data.nodes[e.target].name;
+ if (from === to) return "";
+ const key = [from, to].sort().join("/");
+ if (seen.has(key)) return "";
+ seen.add(key);
+ const [x1, y1] = positions[from],
+ [x2, y2] = positions[to];
+ const featured =
+ [from, to].includes("MinimumVertexCover") &&
+ [from, to].includes("MaximumIndependentSet");
+ return ``;
+ })
+ .join("");
+ const nodes = [...families]
+ .sort((a, b) => Number(!!highlights[a]) - Number(!!highlights[b]))
+ .map((name) => {
+ const [x, y] = positions[name];
+ const isFocus = [
+ "MaximumIndependentSet",
+ "MinimumVertexCover",
+ ].includes(name);
+ const label = highlights[name]?.[2];
+ if (!label)
+ return ``;
+ return `${escape(nameOf(name))}${label ? `${escape(label)}` : ""}`;
+ })
+ .join("");
+ return ``;
+ }
+
+ const cyclePoints = [
+ [150, 35],
+ [231, 94],
+ [200, 190],
+ [100, 190],
+ [69, 94],
+ ];
+ function cycleSVG(mode = "independent", labels = false) {
+ const selected = mode === "independent" ? [0, 2] : [1, 3, 4];
+ return ``;
+ }
+
+ function complementArt() {
+ const graph = (offset, selected) =>
+ `${cyclePoints.map(([x, y], i) => ``).join("")}${cyclePoints.map(([x, y], i) => ``).join("")}`;
+ return ``;
+ }
+
+ function miniArt(name) {
+ if (name === "MaximumIndependentSet") return cycleSVG();
+ if (name === "Satisfiability")
+ return '';
+ return '';
+ }
+
+ function hydrateHome() {
+ document.querySelector("#hero-graph").innerHTML = graphArt();
+ document.querySelector("#problem-showcase").innerHTML = [
+ "MaximumIndependentSet",
+ "Satisfiability",
+ "QUBO",
+ ]
+ .filter((name) => families.includes(name))
+ .map((name) => {
+ const variants = variantsOf(name);
+ return `${escape(categories[variants[0].category] || "Computational problem")}
+ Explore ${families.length} problem families and their implemented
+ reductions. Every connection has explicit variants, size bounds, and
+ code you can inspect.
+
+ ${mis ? "A simple question. A rich search space." : "The problem"}
+
+ ${mis ? '
Given a graph G = (V, E), choose a set of vertices such that no two chosen vertices are adjacent. Maximize the total weight of the chosen vertices. With unit weights, this is the largest independent set.
maximize ∑ wᵥ xᵥsubject to xᵤ + xᵥ ≤ 1 for every edge (u, v), with xᵥ ∈ {0, 1}.
' : `
${escape(description(name))}. The fields below define the instance accepted by the implementation. Consult the paper for its mathematical definition and the API for its full contract.
No incoming reduction is registered for this exact variant.
'}
+
+
+
Instance structure
+ ${schema?.fields?.length ? `
Field
Type
Meaning
${schema.fields.map((f) => `
${escape(f.name)}
${escape(f.type_name)}
${escape(f.description)}
`).join("")}
` : "
See the API reference for the instance schema.
"}
+
+
+
Explore from your terminal
+ ${codePanel(`pred show ${name}`)}
+
+ Install the CLI with
+ cargo install problemreductions-cli. The command
+ shows the problem catalog; reduction availability depends on the
+ selected variant.
+
+ ${complement ? "Keep the graph. Complement the solution. A foundational connection between two views of the same combinatorial structure." : "An executable construction connecting two concrete problem variants, with explicit size bounds and a recoverable contract."}
+
+
+
+
+
+
The construction
+ ${complement ? `
The target uses the same graph and vertex weights. ${vcToMis ? "Solve Maximum Independent Set on that graph, then take the complement of its vertex selection to recover a minimum vertex cover." : "Solve Minimum Vertex Cover on that graph, then take the complement of its vertex selection to recover a maximum independent set."}
S ↔ V ∖ SA set is independent exactly when its complement is a vertex cover.
For weighted instances, the two objective values sum to the total vertex weight. Maximizing the independent-set weight therefore minimizes the complementary cover weight.
+ Registry overheads are asymptotic upper bounds. Read the
+ constructor for exact instance
+ sizes.${complement ? " This construction preserves the number of vertices and edges exactly." : ""}
+
+
+
+
Follow the evidence
+
+ Implementation, mathematical reasoning, and test evidence are
+ distinct parts of the record.
+
+
+
+
Executable Rust construction
+
+ Inspect the transformation and its extraction contract
+ directly.
+
+ ${complement ? "Established mathematical result" : "Implemented in the library"}
+
+
+ ${complement ? "This is a classical reduction, presented as an example of an inspectable result." : "Registration establishes implementation availability. It does not establish research novelty."}
+ Formal verification is not asserted.
+
+
+
+ ${complement ? "Why does complementation preserve optimality?
If S is independent, no edge has both endpoints in S, so every edge has an endpoint in V ∖ S. Conversely, if V ∖ S covers every edge, no edge can have both endpoints in S. Since w(S) + w(V ∖ S) = w(V), maximizing one objective minimizes the other.
" : ""}
+
+
+
Reproduce the implementation checks
+
From a checkout of the repository:
+ ${codePanel(testCommand)}
+
+ ${edge.test_path ? "The command filters library tests by the rule module." : "This rule uses shared test coverage; the command runs the library suite."}
+ Check the reported test count and results. Tests support the
+ implementation; they do not replace a general proof.
+
+ A different formulation can unlock a different solver. Explore the
+ connections, understand their cost, and follow the construction all
+ the way to code.
+
+ Our ambition is a continuous research loop: agents choose useful
+ questions, construct reductions, search for counterexamples, and
+ turn surviving ideas into reusable mathematics.
+
+
+
+
+
+
Find the frontier
+
+ Identify missing solver access, costly constructions, and
+ opportunities to improve the atlas.
+
+
+
+
Build a hypothesis
+
+ Explore the literature. Propose a mapping, its assumptions, and
+ the claims it must satisfy.
+
+
+
+
Try to break it
+
+ Challenge the construction with independent implementations and
+ adversarial examples.
+
+
+
+
Grow the atlas
+
+ Review the evidence. Integrate useful results and use what was
+ learned to guide the next question.
+
+
+
+
+
+
+ Built today: agent-assisted implementation and
+ review workflows. Next frontier: autonomous
+ question selection and persistent experiment records.
+
# Install the research toolkit
+$ cargo install problemreductions-cli
+
+# Explore a problem
+$ pred show MIS
+
+# Search for a route to a solver
+$ pred path MIS ILP