Merge pull request #651 from CodingThrust/fixture-based-example-db

perf: store example DB as fixtures, 850x faster export

Author: GiggleLiu

.claude/CLAUDE.md

@@ -41,15 +41,14 @@ make fmt-check      # Check code formatting
 make clippy         # Run clippy lints
 make doc            # Build mdBook documentation (includes reduction graph export)
 make mdbook         # Build and serve mdBook with live reload
-make paper          # Build Typst paper (runs examples + exports first)
+make paper          # Build Typst paper from checked-in example fixtures
 make coverage       # Generate coverage report (>95% required)
 make check          # Quick pre-commit check (fmt + clippy + test)
 make rust-export    # Generate Julia parity test data (mapping stages)
 make export-schemas # Regenerate problem schemas JSON
 make qubo-testdata  # Regenerate QUBO ground truth JSON
 make clean          # Clean build artifacts
 make diagrams      # Generate SVG diagrams from Typst (light + dark)
-make examples      # Generate example JSON for paper
 make compare       # Generate and compare Rust mapping exports
 make jl-testdata   # Regenerate Julia parity test data (requires julia)
 make cli           # Build the pred CLI tool (without MCP, fast)

.claude/skills/add-rule/SKILL.md

@@ -155,18 +155,17 @@ Step-by-step walkthrough with concrete numbers from JSON data. Required steps:
 1. Show source instance (dimensions, structure, graph visualization if applicable)
 2. Walk through construction with intermediate values
 3. Verify a concrete solution end-to-end
-4. Solution count: `#src_tgt.solutions.len()` with combinatorial justification
+4. Witness semantics: state that the fixture stores one canonical witness; if multiplicity matters mathematically, explain it from the construction rather than from `solutions.len()`
 
 Use `graph-colors`, `g-node()`, `g-edge()` for graph visualization — see reference examples.
 
 ### 5d. Build and verify
 
 ```bash
-make examples  # Regenerate example JSON
 make paper     # Must compile without errors
 ```
 
-Checklist: notation self-contained, complexity cited, overhead consistent, example uses JSON data (not hardcoded), solution verified end-to-end, solution count stated, paper compiles.
+Checklist: notation self-contained, complexity cited, overhead consistent, example uses JSON data (not hardcoded), solution verified end-to-end, witness semantics respected, paper compiles.
 
 ## Step 6: Regenerate exports and verify
 

.claude/skills/final-review/SKILL.md

@@ -197,10 +197,10 @@ Verify the PR includes all required components. Check:
 
 **Paper-example consistency check (both Model and Rule PRs):**
 
-The paper example must use data from the generated JSON (`docs/paper/examples/generated/`), not hand-written data. To verify:
-1. Run `make examples` on the PR branch to regenerate `docs/paper/examples/generated/models.json` and `rules.json`.
-2. For **[Rule] PRs**: the paper's `reduction-rule` entry must call `load-example(source, target)` (defined in `reductions.typ`) to load the canonical example from `rules.json`, and derive all concrete values from the loaded data using Typst array operations — no hand-written instance data.
-3. For **[Model] PRs**: read the problem's entry in `models.json` and compare its `instance` field against the paper's `problem-def` example. The paper example must use the same instance (allowing 0-indexed JSON vs 1-indexed math notation). If they differ, flag: "Paper example does not match `example_db` canonical instance in `models.json`."
+The paper example must use data from the canonical fixture JSON (`src/example_db/fixtures/examples.json`), not hand-written data. To verify:
+1. If the PR changes example builders/specs, run `make regenerate-fixtures` on the PR branch.
+2. For **[Rule] PRs**: the paper's `reduction-rule` entry must call `load-example(source, target, ...)` (defined in `reductions.typ`) to load the canonical example from `examples.json`, and derive all concrete values from the loaded data using Typst array operations — no hand-written instance data.
+3. For **[Model] PRs**: read the problem's entry in `examples.json` under `models` and compare its `instance` field against the paper's `problem-def` example. The paper example must use the same instance (allowing 0-indexed JSON vs 1-indexed math notation). If they differ, flag: "Paper example does not match `example_db` canonical instance in `examples.json`."
 
 **Issue–test round-trip consistency check (both Model and Rule PRs):**
 

.claude/skills/write-model-in-paper/SKILL.md

@@ -126,16 +126,16 @@ achieves $O^*(2^n)$ @bjorklund2009.
 
 ### 3c. Example with Visualization
 
-A concrete small instance that illustrates the problem. **The example must use data from the generated `models.json`**, not an independently invented instance.
+A concrete small instance that illustrates the problem. **The example must use data from the checked-in canonical fixture DB**, not an independently invented instance.
 
 #### Sourcing example data
 
-1. Run `make examples` to ensure `docs/paper/examples/generated/models.json` is up to date.
-2. Find the problem's entry in `models.json` — it contains the canonical `instance`, `samples`, and `optimal` fields.
+1. If you changed example builders/specs, run `make regenerate-fixtures` to refresh `src/example_db/fixtures/examples.json`.
+2. Find the problem's entry in `src/example_db/fixtures/examples.json` under `models` — it contains the canonical `instance`, `samples`, and `optimal` fields.
 3. Use the values from `instance` in the paper example (translating 0-indexed code values to 1-indexed math notation where conventional, e.g., vertices {0,...,n-1} → {1,...,n}).
 4. Use `optimal` configurations to show the solution.
 
-**Do not invent a different instance.** If the canonical example is too large or not pedagogically ideal, fix it in `canonical_model_example_specs()` first, re-run `make examples`, then write the paper entry from the updated JSON.
+**Do not invent a different instance.** If the canonical example is too large or not pedagogically ideal, fix it in `canonical_model_example_specs()` first, re-run `make regenerate-fixtures`, then write the paper entry from the updated JSON.
 
 #### Requirements
 
@@ -147,7 +147,7 @@ A concrete small instance that illustrates the problem. **The example must use d
 #### Structure
 
 ```typst
-*Example.* Consider [instance description with concrete numbers from models.json].
+*Example.* Consider [instance description with concrete numbers from `examples.json`].
 [Describe the solution and why it's valid/optimal].
 
 #figure({
@@ -185,7 +185,7 @@ make paper
 - [ ] **Notation self-contained**: every symbol in `def` is defined before first use
 - [ ] **Background present**: historical context, applications, or structural properties
 - [ ] **Algorithms cited**: every complexity claim has `@citation` or footnote warning
-- [ ] **Example from JSON**: instance data matches `models.json` canonical example (not independently invented)
+- [ ] **Example from JSON**: instance data matches `src/example_db/fixtures/examples.json` canonical example (not independently invented)
 - [ ] **Evaluation shown**: objective/verifier computed on the example solution
 - [ ] **Diagram included**: figure with caption and label for graph/matrix/set visualization
 - [ ] **Paper compiles**: `make paper` succeeds without errors

.claude/skills/write-rule-in-paper/SKILL.md

@@ -18,7 +18,7 @@ Full authoring guide for writing a `reduction-rule` entry in `docs/paper/reducti
 Before using this skill, ensure:
 - The reduction is implemented and tested (`src/rules/<source>_<target>.rs`)
 - A canonical example exists in `src/example_db/rule_builders.rs`
-- Example JSON is generated (`make examples`)
+- If the canonical example changed, fixtures are regenerated (`make regenerate-fixtures`)
 - The reduction graph and schemas are up to date (`cargo run --example export_graph && cargo run --example export_schemas`)
 
 ## Step 1: Load Example Data
@@ -29,8 +29,8 @@ Before using this skill, ensure:
 ```
 
 Where:
-- `load-example(source, target)` looks up the canonical rule entry from the generated rule database
-- The returned record contains `source`, `target`, `overhead`, and `solutions`
+- `load-example(source, target, ...)` looks up the canonical rule entry from `src/example_db/fixtures/examples.json`
+- The returned record contains `source`, `target`, and `solutions`
 - Access fields: `src_tgt.source.instance`, `src_tgt.target.instance`, `src_tgt_sol.source_config`, `src_tgt_sol.target_config`
 
 ## Step 2: Write the Theorem Body (Rule Statement)
@@ -158,7 +158,7 @@ Detailed by default. Only use a brief example for trivially obvious reductions (
 
     *Step N -- Verify a solution.* [end-to-end verification]
 
-    *Count:* #src_tgt.solutions.len() optimal solutions ...
+    *Multiplicity:* The fixture stores one canonical witness. If total multiplicity matters, explain it from the construction.
   ],
 )
 ```
@@ -177,7 +177,7 @@ Each step should:
 | First | Show the source instance (dimensions, structure). Include graph visualization if applicable. |
 | Middle | Walk through the construction. Show intermediate values. Explicitly quantify overhead. |
 | Second-to-last | Verify a concrete solution end-to-end (source config → target config, check validity). |
-| Last | Solution count: `#src_tgt.solutions.len()` with brief combinatorial justification. |
+| Last | State that the fixture stores one canonical witness; if multiplicity matters, justify it mathematically from the construction. |
 
 ### 4d. Graph Visualization (if applicable)
 
@@ -202,8 +202,8 @@ Each step should:
 // Target configuration (e.g., binary encoding)
 #src_tgt_sol.target_config.map(str).join(", ")
 
-// Number of optimal solutions
-#src_tgt.solutions.len()
+// The canonical witness pair
+#src_tgt.solutions.at(0)
 
 // Source instance fields
 #src_tgt.source.instance.num_vertices
@@ -220,9 +220,6 @@ If this is a new problem not yet in the paper, add to the `display-name` diction
 ## Step 6: Build and Verify
 
 ```bash
-# Regenerate example JSON (if not already done)
-make examples
-
 # Build the paper
 make paper
 ```
@@ -234,7 +231,7 @@ make paper
 - [ ] **Overhead consistent**: prose dimensions match auto-derived overhead from JSON edge data
 - [ ] **Example uses JSON data**: concrete values come from `load-example`/`load-results`, not hardcoded
 - [ ] **Solution verified**: at least one solution checked end-to-end in the example
-- [ ] **Solution count**: `solutions.len()` stated with combinatorial explanation
+- [ ] **Witness semantics**: text treats `solutions.at(0)` as the canonical witness; any multiplicity claim is derived mathematically, not from fixture length
 - [ ] **Paper compiles**: `make paper` succeeds without errors
 - [ ] **Completeness check**: no new warnings about missing edges in the paper
 

.gitignore

@@ -84,6 +84,7 @@ claude-output.log
 .worktrees/
 .worktree/
 *.json
+!src/example_db/fixtures/*.json
 .claude/worktrees/
 docs/test-reports/
 docs/superpowers/

Cargo.toml

@@ -46,8 +46,8 @@ name = "solver_benchmarks"
 harness = false
 
 [[example]]
-name = "export_examples"
-path = "examples/export_examples.rs"
+name = "regenerate_fixtures"
+path = "examples/regenerate_fixtures.rs"
 required-features = ["example-db"]
 
 [profile.release]

Makefile

@@ -1,6 +1,6 @@
 # Makefile for problemreductions
 
-.PHONY: help build test mcp-test fmt clippy doc mdbook paper examples 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
+.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 regenerate-fixtures
 
 RUNNER ?= codex
 CLAUDE_MODEL ?= opus
@@ -18,13 +18,13 @@ 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 "  paper        - Build Typst paper (requires typst)"
+	@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"
 	@echo "  check        - Quick check (fmt + clippy + test)"
 	@echo "  rust-export  - Generate Rust mapping JSON exports"
 	@echo "  compare      - Generate and compare Rust mapping exports"
-	@echo "  examples     - Generate example JSON for paper"
+	@echo "  regenerate-fixtures - Recompute example DB fixtures (BruteForce/ILP, slow)"
 	@echo "  export-schemas - Export problem schemas to JSON"
 	@echo "  qubo-testdata - Regenerate QUBO test data (requires uv)"
 	@echo "  jl-testdata  - Regenerate Julia parity test data (requires julia)"
@@ -113,20 +113,20 @@ mdbook:
 	python3 -m http.server 3001 -d book &
 	@sleep 1 && (command -v xdg-open >/dev/null && xdg-open http://localhost:3001 || open http://localhost:3001)
 
-# Generate all example JSON files for the paper
-examples:
-	cargo run --features "ilp-highs example-db" --example export_examples
-	cargo run --features ilp-highs --example export_petersen_mapping
+# Regenerate example DB fixtures from code (runs BruteForce/ILP — slow)
+regenerate-fixtures:
+	cargo run --release --features "ilp-highs example-db" --example regenerate_fixtures
 
 # Export problem schemas to JSON
 export-schemas:
 	cargo run --example export_schemas
 
-# Build Typst paper (generates examples first)
-paper: examples
+# Build Typst paper (reads canonical examples directly from fixtures)
+paper:
+	cargo run --example export_petersen_mapping
 	cargo run --example export_graph
 	cargo run --example export_schemas
-	cd docs/paper && typst compile --root .. reductions.typ reductions.pdf
+	typst compile --root . docs/paper/reductions.typ docs/paper/reductions.pdf
 
 # Generate coverage report (requires: cargo install cargo-llvm-cov)
 coverage:

docs/agent-profiles/SKILLS.md

@@ -1,9 +1,10 @@
 # Skills
 
-Example generation now goes through the example catalog and dedicated exporter.
+Example generation now goes through the example catalog and checked-in fixture DB.
 When a workflow needs a paper/example instance, prefer the catalog path over ad hoc `examples/reduction_*.rs` binaries:
 
-- use `make examples` or `cargo run --features "ilp-highs example-db" --example export_examples`
+- use `src/example_db/fixtures/examples.json` directly for paper/example data
+- use `make regenerate-fixtures` when canonical examples change
 - use `pred create --example <PROBLEM_SPEC>` to materialize a canonical model example as normal problem JSON
 - use `pred create --example <SOURCE_SPEC> --to <TARGET_SPEC>` to materialize a canonical rule example as normal problem JSON
 - when adding new example coverage, register a catalog entry instead of creating a new standalone reduction example file