diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index 8256fe593..fc00a6f1f 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -41,7 +41,7 @@ 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)
@@ -49,7 +49,6 @@ 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)
diff --git a/.claude/skills/add-rule/SKILL.md b/.claude/skills/add-rule/SKILL.md
index c8ac7e7c6..894d11996 100644
--- a/.claude/skills/add-rule/SKILL.md
+++ b/.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
 
diff --git a/.claude/skills/final-review/SKILL.md b/.claude/skills/final-review/SKILL.md
index 4e7d96987..1eeb86df1 100644
--- a/.claude/skills/final-review/SKILL.md
+++ b/.claude/skills/final-review/SKILL.md
@@ -196,10 +196,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):**
 
diff --git a/.claude/skills/write-model-in-paper/SKILL.md b/.claude/skills/write-model-in-paper/SKILL.md
index c5b4e3ed4..03cc2dbc3 100644
--- a/.claude/skills/write-model-in-paper/SKILL.md
+++ b/.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
diff --git a/.claude/skills/write-rule-in-paper/SKILL.md b/.claude/skills/write-rule-in-paper/SKILL.md
index 3542875ef..1ddfa3aa9 100644
--- a/.claude/skills/write-rule-in-paper/SKILL.md
+++ b/.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
 
diff --git a/.gitignore b/.gitignore
index 79202a3bd..edd41945c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -84,6 +84,7 @@ claude-output.log
 .worktrees/
 .worktree/
 *.json
+!src/example_db/fixtures/*.json
 .claude/worktrees/
 docs/test-reports/
 docs/superpowers/
diff --git a/Cargo.toml b/Cargo.toml
index 9ee646cdc..45071c49c 100644
--- a/Cargo.toml
+++ b/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]
diff --git a/Makefile b/Makefile
index 53917dd42..fdc254914 100644
--- a/Makefile
+++ b/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:
diff --git a/docs/agent-profiles/SKILLS.md b/docs/agent-profiles/SKILLS.md
index d1d49b220..b7c7a6e3a 100644
--- a/docs/agent-profiles/SKILLS.md
+++ b/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
diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index f50c5ee53..b3a286b66 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -15,12 +15,16 @@
 #show: thmrules.with(qed-symbol: $square$)
 
 // === Example JSON helpers ===
-// Load canonical example databases generated by `make examples`.
-#let rule-db = json("examples/generated/rules.json")
-#let model-db = json("examples/generated/models.json")
-
-#let load-example(source, target) = {
-  let matches = rule-db.rules.filter(r => r.source.problem == source and r.target.problem == target)
+// Load canonical example database directly from the checked-in fixture file.
+#let example-db = json("../../src/example_db/fixtures/examples.json")
+
+#let load-example(source, target, source-variant: none, target-variant: none) = {
+  let matches = example-db.rules.filter(r =>
+    r.source.problem == source and
+    r.target.problem == target and
+    (source-variant == none or r.source.variant == source-variant) and
+    (target-variant == none or r.target.variant == target-variant)
+  )
   if matches.len() == 1 {
     matches.at(0)
   } else if matches.len() == 0 {
@@ -30,8 +34,11 @@
   }
 }
 
-#let load-model-example(name) = {
-  let matches = model-db.models.filter(m => m.problem == name)
+#let load-model-example(name, variant: none) = {
+  let matches = example-db.models.filter(m =>
+    m.problem == name and
+    (variant == none or m.variant == variant)
+  )
   if matches.len() == 1 {
     matches.at(0)
   } else if matches.len() == 0 {
@@ -275,6 +282,8 @@
 #let reduction-rule(
   source, target,
   example: false,
+  example-source-variant: none,
+  example-target-variant: none,
   example-caption: none,
   extra: none,
   theorem-body, proof-body,
@@ -301,7 +310,12 @@
   proof[#proof-body]
 
   if example {
-    let data = load-example(source, target)
+    let data = load-example(
+      source,
+      target,
+      source-variant: example-source-variant,
+      target-variant: example-target-variant,
+    )
     pad(left: 1.5em, reduction-example(data, caption: example-caption)[#extra])
   }
 }
@@ -376,8 +390,8 @@ The gray schema table shows the JSON field names used in the library's data stru
 In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| = n$ vertices and $|E|$ edges.
 
 #{
-  // MIS has two entries in models.json; select the unit-weight variant
-  let x = model-db.models.filter(m => m.problem == "MaximumIndependentSet" and m.variant.at("weight", default: "") == "One").at(0)
+  // MIS has two entries in examples.json; select the unit-weight variant
+  let x = load-model-example("MaximumIndependentSet", variant: (graph: "SimpleGraph", weight: "One"))
   let nv = graph-num-vertices(x.instance)
   let ne = graph-num-edges(x.instance)
   // Pick optimal[2] = {v1, v3, v5, v9} to match figure
@@ -1991,7 +2005,7 @@ Each reduction is presented as a *Rule* (with linked problem names and overhead
   extra: [
     Source: $n = #spin-num-spins(sg_qubo.source.instance)$ spins, $h_i = 0$, couplings $J_(i j) in {plus.minus 1}$ \
     Mapping: $s_i = 2x_i - 1$ converts spins ${-1, +1}$ to binary ${0, 1}$ \
-    Ground state ($#sg_qubo.solutions.len()$-fold degenerate): $bold(x) = (#sg_qubo_sol.target_config.map(str).join(", "))$ #sym.checkmark
+    Canonical ground-state witness: $bold(x) = (#sg_qubo_sol.target_config.map(str).join(", "))$ #sym.checkmark
   ],
 )[
   The Ising model and QUBO are both quadratic functions over finite domains: spins ${-1,+1}$ and binary variables ${0,1}$, respectively. The affine map $s_i = 2x_i - 1$ establishes a bijection between the two domains and preserves the quadratic structure. Substituting into the Ising Hamiltonian yields a QUBO objective that differs from the original energy by a constant, so ground states correspond exactly.
@@ -2039,7 +2053,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
 
     *Step 4 -- Verify a solution.* The first valid 3-coloring is $(c_0, ..., c_4) = (#kc_qubo_sol.source_config.map(str).join(", "))$, shown in the figure above. The one-hot encoding is $bold(x) = (#kc_qubo_sol.target_config.map(str).join(", "))$. Check: each 3-bit group has exactly one 1 (valid one-hot #sym.checkmark), and for every edge the two endpoints have different colors (e.g.\ edge $0 dash 1$: colors $#kc_qubo_sol.source_config.at(0), #kc_qubo_sol.source_config.at(1)$ #sym.checkmark).\
 
-    *Count:* #kc_qubo.solutions.len() valid colorings $= 3! times 3$. The triangle $2 dash 3 dash 4$ forces 3 distinct colors ($3! = 6$ permutations); for each, the base vertices $0, 1$ each have 3 compatible choices but share edge $0 dash 1$, leaving $3$ valid pairs.
+    *Multiplicity:* The fixture stores one canonical coloring witness. The house graph has $3! times 3 = 18$ valid colorings overall: the triangle $2 dash 3 dash 4$ forces 3 distinct colors ($3! = 6$ permutations), and for each, the base vertices $0, 1$ have exactly $3$ compatible ordered pairs.
   ],
 )[
   The $k$-coloring problem has two requirements: each vertex gets exactly one color, and adjacent vertices get different colors. Both can be expressed as quadratic penalties over binary variables. Introduce $n k$ binary variables $x_(v,c) in {0,1}$ (indexed by $v dot k + c$), where $x_(v,c) = 1$ means vertex $v$ receives color $c$. The first requirement becomes a _one-hot constraint_ penalizing vertices with zero or multiple colors; the second becomes an _edge conflict penalty_ penalizing same-color neighbors. The combined QUBO matrix $Q in RR^(n k times n k)$ encodes both penalties.
@@ -2173,7 +2187,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
 
     *Step 4 -- Verify a solution.* The QUBO ground state $bold(z) = (#ks_qubo_sol.target_config.map(str).join(", "))$ extracts to the knapsack choice $bold(x) = (#ks_qubo_sol.source_config.map(str).join(", "))$. This selects items $\{#ks_qubo_selected.map(str).join(", ")\}$ with total weight $#ks_qubo_selected.map(i => str(ks_qubo.source.instance.weights.at(i))).join(" + ") = #ks_qubo_sel_weight$ and total value $#ks_qubo_selected.map(i => str(ks_qubo.source.instance.values.at(i))).join(" + ") = #ks_qubo_sel_value$, so the slack bits are all zero and the penalty term vanishes #sym.checkmark.
 
-    *Count:* #ks_qubo.solutions.len() optimal QUBO solution. The source optimum is unique because items $\{#ks_qubo_selected.map(str).join(", ")\}$ are the only feasible selection achieving value #ks_qubo_sel_value.
+    *Uniqueness:* The fixture stores one canonical optimal witness. The source optimum is unique because items $\{#ks_qubo_selected.map(str).join(", ")\}$ are the only feasible selection achieving value #ks_qubo_sel_value.
   ],
 )[
   For a standard 0-1 Knapsack instance with nonnegative weights, nonnegative values, and nonnegative capacity, the inequality $sum_i w_i x_i lt.eq C$ is converted to equality using binary slack variables that encode the unused capacity. When $C > 0$, one can take $B = floor(log_2 C) + 1$ slack bits; when $C = 0$, a single slack bit also suffices. The penalty method (@sec:penalty-method) combines the negated value objective with a quadratic constraint penalty, producing a QUBO with $n + B$ binary variables.
@@ -2198,7 +2212,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   extra: [
     Source: $n = #qubo_ilp.source.instance.num_vars$ binary variables, 3 off-diagonal terms \
     Target: #qubo_ilp.target.instance.num_vars ILP variables ($#qubo_ilp.source.instance.num_vars$ original $+ #(qubo_ilp.target.instance.num_vars - qubo_ilp.source.instance.num_vars)$ auxiliary), #qubo_ilp.target.instance.constraints.len() McCormick constraints \
-    Optimal: $bold(x) = (#qubo_ilp_sol.source_config.map(str).join(", "))$ ($#qubo_ilp.solutions.len()$-fold degenerate) #sym.checkmark
+    Canonical optimal witness: $bold(x) = (#qubo_ilp_sol.source_config.map(str).join(", "))$ #sym.checkmark
   ],
 )[
   QUBO minimizes a quadratic form $bold(x)^top Q bold(x)$ over binary variables. Every quadratic term $Q_(i j) x_i x_j$ can be _linearized_ by introducing an auxiliary variable $y_(i j)$ constrained to equal the product $x_i x_j$ via three McCormick inequalities. Diagonal terms $Q_(i i) x_i^2 = Q_(i i) x_i$ are already linear for binary $x_i$. The result is a binary ILP with a linear objective and $3 m$ constraints (where $m$ is the number of non-zero off-diagonal entries), whose minimizer corresponds exactly to the QUBO minimizer.
@@ -2224,7 +2238,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   extra: [
     Circuit: #circuit-num-gates(cs_ilp.source.instance) gates (2 XOR, 2 AND, 1 OR), #circuit-num-variables(cs_ilp.source.instance) variables \
     Target: #cs_ilp.target.instance.num_vars ILP variables (circuit vars $+$ auxiliary), trivial objective \
-    #cs_ilp.solutions.len() feasible solutions ($= 2^3$ valid input combinations for the full adder) #sym.checkmark
+    Canonical feasible witness shown ($2^3$ valid input combinations exist for the full adder) #sym.checkmark
   ],
 )[
   Each boolean gate (AND, OR, NOT, XOR) has a truth table that can be captured exactly by a small set of linear inequalities over binary variables. By Tseitin-style flattening, each internal expression node gets an auxiliary ILP variable constrained to match its gate's output, so the conjunction of all gate constraints is feasible if and only if the circuit is satisfiable. The ILP has a trivial objective (minimize 0), making it a pure feasibility problem.
@@ -2278,7 +2292,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   extra: [
     SAT assignment: $(x_1, ..., x_5) = (#sat_kc_sol.source_config.map(str).join(", "))$ \
     Construction: 3 base + $2 times #sat_kc.source.instance.num_vars$ variable gadgets + OR-gadgets $arrow.r$ #graph-num-vertices(sat_kc.target.instance) vertices, #graph-num-edges(sat_kc.target.instance) edges \
-    #sat_kc.solutions.len() valid 3-colorings (color symmetry of satisfying assignments) #sym.checkmark
+    Canonical 3-coloring witness shown (the construction also has the expected color-symmetry multiplicity for satisfying assignments) #sym.checkmark
   ],
 )[
   @garey1979 A 3-coloring partitions vertices into three classes. The key insight is that three colors suffice to encode Boolean logic: one color represents TRUE, one FALSE, and a third (AUX) serves as a neutral ground. Variable gadgets force each variable's positive and negative literals to receive opposite truth colors, while clause gadgets use an OR-chain that can only receive the TRUE color when at least one input literal is TRUE-colored. Connecting the output of each clause gadget to the FALSE vertex forces it to be TRUE-colored, encoding the requirement that every clause is satisfied.
@@ -2365,7 +2379,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   extra: [
     Circuit: #circuit-num-gates(cs_sg.source.instance) gates (2 XOR, 2 AND, 1 OR), #circuit-num-variables(cs_sg.source.instance) variables \
     Target: #spin-num-spins(cs_sg.target.instance) spins (each gate allocates I/O + auxiliary spins) \
-    #cs_sg.solutions.len() ground states ($= 2^3$ valid input combinations for the full adder) #sym.checkmark
+    Canonical ground-state witness shown ($2^3$ valid input combinations exist for the full adder) #sym.checkmark
   ],
 )[
   @whitfield2012 @lucas2014 Each logic gate can be represented as an Ising gadget --- a small set of spins with couplings $J_(i j)$ and fields $h_i$ chosen so that the gadget's ground states correspond exactly to the gate's truth table rows. Composing gadgets for all gates in the circuit yields a spin glass whose ground states encode precisely the satisfying assignments of the circuit. The energy gap between valid and invalid I/O patterns ensures that any global ground state respects every gate's logic.
@@ -2400,18 +2414,17 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   let pow2 = (1, 2, 4, 8, 16, 32)
   range(count).fold(0, (acc, i) => acc + config.at(start + i) * pow2.at(i))
 }
+#let fact_cs_sol = fact_cs.solutions.at(0)
 #let fact-nbf = fact_cs.source.instance.m
 #let fact-nbs = fact_cs.source.instance.n
+#let fact-p = fact-decode(fact_cs_sol.source_config, 0, fact-nbf)
+#let fact-q = fact-decode(fact_cs_sol.source_config, fact-nbf, fact-nbs)
 #reduction-rule("Factoring", "CircuitSAT",
   example: true,
   example-caption: [Factor $N = #fact_cs.source.instance.target$],
   extra: [
     Circuit: $#fact-nbf times #fact-nbs$ array multiplier with #circuit-num-gates(fact_cs.target.instance) gates, #circuit-num-variables(fact_cs.target.instance) variables \
-    #fact_cs.solutions.len() solutions: #fact_cs.solutions.map(sol => {
-      let p = fact-decode(sol.source_config, 0, fact-nbf)
-      let q = fact-decode(sol.source_config, fact-nbf, fact-nbs)
-      $#p times #q = #fact_cs.source.instance.target$
-    }).join(" and ") #sym.checkmark
+    Canonical witness: $#fact-p times #fact-q = #fact_cs.source.instance.target$ #sym.checkmark
   ],
 )[
   Integer multiplication can be implemented as a boolean circuit: an $m times n$ array multiplier computes $p times q$ using only AND, XOR, and OR gates arranged in a grid of full adders. Constraining the output bits to match $N$ turns the circuit into a satisfiability problem --- the circuit is satisfiable iff $N = p times q$ for some $p, q$ within the given bit widths. _(Folklore; no canonical reference.)_
@@ -2438,7 +2451,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   extra: [
     Direct 1:1 mapping: vertices $arrow.r$ spins, $J_(i j) = w_(i j) = 1$, $h_i = 0$ \
     Partition: $S = {#mc_sg_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ vs $overline(S) = {#mc_sg_sol.source_config.enumerate().filter(((i, x)) => x == 0).map(((i, x)) => str(i)).join(", ")}$ \
-    Cut value $= #mc_sg_cut$ ($#mc_sg.solutions.len()$-fold degenerate) #sym.checkmark
+    Cut value $= #mc_sg_cut$ (canonical witness shown) #sym.checkmark
   ],
 )[
   @barahona1982 A maximum cut partitions vertices into two groups to maximize the total weight of edges crossing the partition. In the Ising model, two spins with opposite signs contribute $-J_(i j) s_i s_j = J_(i j)$ to the energy, while same-sign spins contribute $-J_(i j)$. Setting $J_(i j) = w_(i j)$ and $h_i = 0$ makes each cut edge lower the energy by $2 J_(i j)$ relative to an uncut edge, so the Ising ground state corresponds to the maximum cut.
@@ -2458,7 +2471,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   extra: [
     All $h_i = 0$: no ancilla needed, direct 1:1 vertex mapping \
     Edge weights $w_(i j) = J_(i j) in {plus.minus 1}$ (alternating couplings) \
-    Ground state ($#sg_mc.solutions.len()$-fold degenerate): partition $S = {#sg_mc_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ #sym.checkmark
+    Canonical ground-state witness: partition $S = {#sg_mc_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ #sym.checkmark
   ],
 )[
   @barahona1982 @lucas2014 The Ising Hamiltonian $H = -sum J_(i j) s_i s_j - sum h_i s_i$ has two types of terms. The pairwise couplings $J_(i j)$ map directly to MaxCut edge weights, since minimizing $-J_(i j) s_i s_j$ favors opposite spins (cut edges) when $J_(i j) > 0$. The local fields $h_i$ have no direct MaxCut analogue, but can be absorbed by introducing a single ancilla vertex connected to every spin with weight $h_i$: fixing the ancilla's partition side effectively creates a linear bias on each spin.
@@ -2627,7 +2640,7 @@ The following reductions to Integer Linear Programming are straightforward formu
 
     *Step 4 -- Verify a solution.* The QUBO ground state $bold(x) = (#tsp_qubo_sol.target_config.map(str).join(", "))$ encodes a valid tour. Reading the permutation: each 3-bit group has exactly one 1 (valid permutation #sym.checkmark). The tour cost equals $w_(01) + w_(02) + w_(12) = 1 + 2 + 3 = 6$.\
 
-    *Count:* #tsp_qubo.solutions.len() optimal QUBO solutions $= 3! = 6$. On $K_3$ with distinct edge weights $1, 2, 3$, every Hamiltonian cycle has cost $1 + 2 + 3 = 6$ (all edges used), and 3 cyclic tours $times$ 2 directions yield $6$ permutation matrices.
+    *Multiplicity:* The fixture stores one canonical optimal witness. On $K_3$ with distinct edge weights $1, 2, 3$, every Hamiltonian cycle has cost $1 + 2 + 3 = 6$ (all edges used), and 3 cyclic tours $times$ 2 directions yield $6$ permutation matrices overall.
   ],
 )[
   Position-based QUBO encoding @lucas2014 maps a Hamiltonian tour to $n^2$ binary variables $x_(v,p)$, where $x_(v,p) = 1$ iff city $v$ is visited at position $p$. The QUBO Hamiltonian $H = H_A + H_B + H_C$ combines permutation constraints with the distance objective ($n^2$ variables indexed by $v dot n + p$).
@@ -2767,22 +2780,31 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples
 
 == Resource Estimation from Examples
 
-The following table shows concrete variable overhead for example instances, generated from the reduction examples (`make examples`).
+The following table shows concrete variable overhead for example instances, taken directly from the canonical fixture examples.
 
 #let example-files = (
   (source: "MaximumIndependentSet", target: "MinimumVertexCover"),
   (source: "MinimumVertexCover", target: "MaximumIndependentSet"),
-  (source: "MaximumIndependentSet", target: "MaximumSetPacking"),
+  (
+    source: "MaximumIndependentSet",
+    target: "MaximumSetPacking",
+    source-variant: (graph: "SimpleGraph", weight: "One"),
+    target-variant: (weight: "One"),
+  ),
   (source: "MaximumMatching", target: "MaximumSetPacking"),
   (source: "MinimumVertexCover", target: "MinimumSetCovering"),
   (source: "MaxCut", target: "SpinGlass"),
   (source: "SpinGlass", target: "MaxCut"),
   (source: "SpinGlass", target: "QUBO"),
   (source: "QUBO", target: "SpinGlass"),
-  (source: "MaximumIndependentSet", target: "QUBO"),
   (source: "KColoring", target: "QUBO"),
   (source: "MaximumSetPacking", target: "QUBO"),
-  (source: "KSatisfiability", target: "QUBO"),
+  (
+    source: "KSatisfiability",
+    target: "QUBO",
+    source-variant: (k: "K3"),
+    target-variant: (weight: "f64"),
+  ),
   (source: "ILP", target: "QUBO"),
   (source: "Satisfiability", target: "MaximumIndependentSet"),
   (source: "Satisfiability", target: "KColoring"),
@@ -2801,7 +2823,12 @@ The following table shows concrete variable overhead for example instances, gene
 )
 
 #let examples = example-files.map(entry => {
-  let d = load-example(entry.source, entry.target)
+  let d = load-example(
+    entry.source,
+    entry.target,
+    source-variant: entry.at("source-variant", default: none),
+    target-variant: entry.at("target-variant", default: none),
+  )
   (name: example-name(entry.source, entry.target), data: d)
 })
 
diff --git a/examples/export_examples.rs b/examples/export_examples.rs
deleted file mode 100644
index af5ee8e02..000000000
--- a/examples/export_examples.rs
+++ /dev/null
@@ -1,23 +0,0 @@
-use problemreductions::example_db::{build_model_db, build_rule_db, default_generated_dir};
-use problemreductions::export::{write_model_db_to, write_rule_db_to};
-use std::fs;
-
-fn main() {
-    let output_dir = default_generated_dir();
-    if output_dir.exists() {
-        fs::remove_dir_all(&output_dir).expect("Failed to clear generated examples directory");
-    }
-    fs::create_dir_all(&output_dir).expect("Failed to create generated examples directory");
-
-    let rule_db = build_rule_db().expect("Failed to build canonical rule database");
-    let model_db = build_model_db().expect("Failed to build canonical model database");
-
-    write_rule_db_to(&output_dir, &rule_db);
-    write_model_db_to(&output_dir, &model_db);
-
-    println!(
-        "Exported {} rule examples and {} model examples",
-        rule_db.rules.len(),
-        model_db.models.len()
-    );
-}
diff --git a/examples/regenerate_fixtures.rs b/examples/regenerate_fixtures.rs
new file mode 100644
index 000000000..11d34670d
--- /dev/null
+++ b/examples/regenerate_fixtures.rs
@@ -0,0 +1,31 @@
+/// Regenerate example database fixture files from builder code.
+///
+/// This binary recomputes all model and rule examples using BruteForce/ILP
+/// and writes them to `src/example_db/fixtures/` as wrapped JSON objects. Run
+/// this in release mode after changing any model or rule to update the stored
+/// expected results:
+///
+/// ```
+/// cargo run --release --example regenerate_fixtures --features "ilp-highs example-db"
+/// ```
+use problemreductions::example_db::compute_example_db;
+use problemreductions::export::write_example_db_to;
+use std::fs;
+use std::path::Path;
+
+fn main() {
+    let fixtures_dir = Path::new(env!("CARGO_MANIFEST_DIR")).join("src/example_db/fixtures");
+    fs::create_dir_all(&fixtures_dir).expect("Failed to create fixtures directory");
+
+    let example_db = compute_example_db().expect("Failed to compute canonical example database");
+    let examples_path = fixtures_dir.join("examples.json");
+
+    write_example_db_to(&fixtures_dir, &example_db);
+
+    println!(
+        "Regenerated fixtures: {} rule examples, {} model examples",
+        example_db.rules.len(),
+        example_db.models.len()
+    );
+    println!("  Examples: {}", examples_path.display());
+}
diff --git a/src/example_db/fixtures/examples.json b/src/example_db/fixtures/examples.json
new file mode 100644
index 000000000..e48eef824
--- /dev/null
+++ b/src/example_db/fixtures/examples.json
@@ -0,0 +1,79 @@
+{
+  "models": [
+    {"problem":"BMF","variant":{},"instance":{"k":2,"m":3,"matrix":[[true,true,false],[true,true,true],[false,true,true]],"n":3},"samples":[{"config":[1,0,1,1,0,1,1,1,0,0,1,1],"metric":{"Valid":0}}],"optimal":[{"config":[0,1,1,1,1,0,0,1,1,1,1,0],"metric":{"Valid":0}},{"config":[1,0,1,1,0,1,1,1,0,0,1,1],"metric":{"Valid":0}}]},
+    {"problem":"BicliqueCover","variant":{},"instance":{"graph":{"edges":[[0,0],[0,1],[1,1],[1,2]],"left_size":2,"right_size":3},"k":2},"samples":[{"config":[1,0,0,1,1,0,1,1,0,1],"metric":{"Valid":6}}],"optimal":[{"config":[0,1,0,1,0,1,0,1,0,1],"metric":{"Valid":5}},{"config":[1,0,1,0,1,0,1,0,1,0],"metric":{"Valid":5}}]},
+    {"problem":"CircuitSAT","variant":{},"instance":{"circuit":{"assignments":[{"expr":{"op":{"And":[{"op":{"Var":"x1"}},{"op":{"Var":"x2"}}]}},"outputs":["a"]},{"expr":{"op":{"Or":[{"op":{"Var":"x1"}},{"op":{"Var":"x2"}}]}},"outputs":["b"]},{"expr":{"op":{"Xor":[{"op":{"Var":"a"}},{"op":{"Var":"b"}}]}},"outputs":["c"]}]},"variables":["a","b","c","x1","x2"]},"samples":[{"config":[0,1,1,0,1],"metric":true},{"config":[0,1,1,1,0],"metric":true}],"optimal":[{"config":[0,0,0,0,0],"metric":true},{"config":[0,1,1,0,1],"metric":true},{"config":[0,1,1,1,0],"metric":true},{"config":[1,1,0,1,1],"metric":true}]},
+    {"problem":"ClosestVectorProblem","variant":{"weight":"i32"},"instance":{"basis":[[2,0],[1,2]],"bounds":[{"lower":-2,"upper":4},{"lower":-2,"upper":4}],"target":[2.8,1.5]},"samples":[{"config":[3,3],"metric":{"Valid":0.5385164807134505}}],"optimal":[{"config":[3,3],"metric":{"Valid":0.5385164807134505}}]},
+    {"problem":"ExactCoverBy3Sets","variant":{},"instance":{"subsets":[[0,1,2],[0,2,4],[3,4,5],[3,5,7],[6,7,8],[1,4,6],[2,5,8]],"universe_size":9},"samples":[{"config":[1,0,1,0,1,0,0],"metric":true}],"optimal":[{"config":[1,0,1,0,1,0,0],"metric":true}]},
+    {"problem":"Factoring","variant":{},"instance":{"m":2,"n":3,"target":15},"samples":[{"config":[1,1,1,0,1],"metric":{"Valid":0}}],"optimal":[{"config":[1,1,1,0,1],"metric":{"Valid":0}}]},
+    {"problem":"HamiltonianPath","variant":{"graph":"SimpleGraph"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[3,4,null],[3,5,null],[4,2,null],[5,1,null]],"node_holes":[],"nodes":[null,null,null,null,null,null]}}},"samples":[{"config":[0,2,4,3,1,5],"metric":true}],"optimal":[{"config":[0,1,5,3,2,4],"metric":true},{"config":[0,1,5,3,4,2],"metric":true},{"config":[0,2,4,3,1,5],"metric":true},{"config":[0,2,4,3,5,1],"metric":true},{"config":[1,0,2,4,3,5],"metric":true},{"config":[1,5,3,4,2,0],"metric":true},{"config":[2,0,1,5,3,4],"metric":true},{"config":[2,4,3,5,1,0],"metric":true},{"config":[3,4,2,0,1,5],"metric":true},{"config":[3,5,1,0,2,4],"metric":true},{"config":[4,2,0,1,3,5],"metric":true},{"config":[4,2,0,1,5,3],"metric":true},{"config":[4,2,3,5,1,0],"metric":true},{"config":[4,3,2,0,1,5],"metric":true},{"config":[4,3,5,1,0,2],"metric":true},{"config":[5,1,0,2,3,4],"metric":true},{"config":[5,1,0,2,4,3],"metric":true},{"config":[5,1,3,4,2,0],"metric":true},{"config":[5,3,1,0,2,4],"metric":true},{"config":[5,3,4,2,0,1],"metric":true}]},
+    {"problem":"ILP","variant":{"variable":"i32"},"instance":{"constraints":[{"cmp":"Le","rhs":5.0,"terms":[[0,1.0],[1,1.0]]},{"cmp":"Le","rhs":28.0,"terms":[[0,4.0],[1,7.0]]}],"num_vars":2,"objective":[[0,-5.0],[1,-6.0]],"sense":"Minimize"},"samples":[{"config":[0,4],"metric":{"Valid":-24.0}}],"optimal":[{"config":[3,2],"metric":{"Valid":-27.0}}]},
+    {"problem":"IsomorphicSpanningTree","variant":{},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[0,3,null],[1,2,null],[1,3,null],[2,3,null]],"node_holes":[],"nodes":[null,null,null,null]}},"tree":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[0,3,null]],"node_holes":[],"nodes":[null,null,null,null]}}},"samples":[{"config":[0,1,2,3],"metric":true}],"optimal":[{"config":[0,1,2,3],"metric":true},{"config":[0,1,3,2],"metric":true},{"config":[0,2,1,3],"metric":true},{"config":[0,2,3,1],"metric":true},{"config":[0,3,1,2],"metric":true},{"config":[0,3,2,1],"metric":true},{"config":[1,0,2,3],"metric":true},{"config":[1,0,3,2],"metric":true},{"config":[1,2,0,3],"metric":true},{"config":[1,2,3,0],"metric":true},{"config":[1,3,0,2],"metric":true},{"config":[1,3,2,0],"metric":true},{"config":[2,0,1,3],"metric":true},{"config":[2,0,3,1],"metric":true},{"config":[2,1,0,3],"metric":true},{"config":[2,1,3,0],"metric":true},{"config":[2,3,0,1],"metric":true},{"config":[2,3,1,0],"metric":true},{"config":[3,0,1,2],"metric":true},{"config":[3,0,2,1],"metric":true},{"config":[3,1,0,2],"metric":true},{"config":[3,1,2,0],"metric":true},{"config":[3,2,0,1],"metric":true},{"config":[3,2,1,0],"metric":true}]},
+    {"problem":"KColoring","variant":{"graph":"SimpleGraph","k":"K3"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"num_colors":3},"samples":[{"config":[0,1,1,0,2],"metric":true}],"optimal":[{"config":[0,1,1,0,2],"metric":true},{"config":[0,1,1,2,0],"metric":true},{"config":[0,1,2,0,1],"metric":true},{"config":[0,2,1,0,2],"metric":true},{"config":[0,2,2,0,1],"metric":true},{"config":[0,2,2,1,0],"metric":true},{"config":[1,0,0,1,2],"metric":true},{"config":[1,0,0,2,1],"metric":true},{"config":[1,0,2,1,0],"metric":true},{"config":[1,2,0,1,2],"metric":true},{"config":[1,2,2,0,1],"metric":true},{"config":[1,2,2,1,0],"metric":true},{"config":[2,0,0,1,2],"metric":true},{"config":[2,0,0,2,1],"metric":true},{"config":[2,0,1,2,0],"metric":true},{"config":[2,1,0,2,1],"metric":true},{"config":[2,1,1,0,2],"metric":true},{"config":[2,1,1,2,0],"metric":true}]},
+    {"problem":"KSatisfiability","variant":{"k":"K3"},"instance":{"clauses":[{"literals":[1,2,3]},{"literals":[-1,-2,3]},{"literals":[1,-2,-3]}],"num_vars":3},"samples":[{"config":[1,0,1],"metric":true}],"optimal":[{"config":[0,0,1],"metric":true},{"config":[0,1,0],"metric":true},{"config":[1,0,0],"metric":true},{"config":[1,0,1],"metric":true},{"config":[1,1,1],"metric":true}]},
+    {"problem":"MaxCut","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,1,1,1,1,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}}},"samples":[{"config":[1,0,0,1,0],"metric":{"Valid":5}}],"optimal":[{"config":[0,1,1,0,0],"metric":{"Valid":5}},{"config":[0,1,1,0,1],"metric":{"Valid":5}},{"config":[1,0,0,1,0],"metric":{"Valid":5}},{"config":[1,0,0,1,1],"metric":{"Valid":5}}]},
+    {"problem":"MaximalIS","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[2,3,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]},"samples":[{"config":[0,1,0,1,0],"metric":{"Valid":2}},{"config":[1,0,1,0,1],"metric":{"Valid":3}}],"optimal":[{"config":[1,0,1,0,1],"metric":{"Valid":3}}]},
+    {"problem":"MaximumClique","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]},"samples":[{"config":[0,0,1,1,1],"metric":{"Valid":3}}],"optimal":[{"config":[0,0,1,1,1],"metric":{"Valid":3}}]},
+    {"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"One"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[2,3,null],[3,4,null],[4,0,null],[5,7,null],[7,9,null],[9,6,null],[6,8,null],[8,5,null],[0,5,null],[1,6,null],[2,7,null],[3,8,null],[4,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1]},"samples":[{"config":[0,1,0,1,0,1,0,0,0,1],"metric":{"Valid":4}}],"optimal":[{"config":[0,0,1,0,1,1,1,0,0,0],"metric":{"Valid":4}},{"config":[0,1,0,0,1,0,0,1,1,0],"metric":{"Valid":4}},{"config":[0,1,0,1,0,1,0,0,0,1],"metric":{"Valid":4}},{"config":[1,0,0,1,0,0,1,1,0,0],"metric":{"Valid":4}},{"config":[1,0,1,0,0,0,0,0,1,1],"metric":{"Valid":4}}]},
+    {"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[2,3,null],[3,4,null],[4,0,null],[5,7,null],[7,9,null],[9,6,null],[6,8,null],[8,5,null],[0,5,null],[1,6,null],[2,7,null],[3,8,null],[4,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}},"weights":[5,1,1,1,1,3,1,1,1,3]},"samples":[{"config":[1,0,1,0,0,0,0,0,1,1],"metric":{"Valid":10}}],"optimal":[{"config":[1,0,1,0,0,0,0,0,1,1],"metric":{"Valid":10}}]},
+    {"problem":"MaximumMatching","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,1,1,1,1,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}}},"samples":[{"config":[1,0,0,0,1,0],"metric":{"Valid":2}}],"optimal":[{"config":[0,0,1,0,1,0],"metric":{"Valid":2}},{"config":[0,1,0,0,0,1],"metric":{"Valid":2}},{"config":[0,1,1,0,0,0],"metric":{"Valid":2}},{"config":[1,0,0,0,0,1],"metric":{"Valid":2}},{"config":[1,0,0,0,1,0],"metric":{"Valid":2}},{"config":[1,0,0,1,0,0],"metric":{"Valid":2}}]},
+    {"problem":"MaximumSetPacking","variant":{"weight":"i32"},"instance":{"sets":[[0,1],[1,2],[2,3],[3,4]],"weights":[1,1,1,1]},"samples":[{"config":[1,0,1,0],"metric":{"Valid":2}}],"optimal":[{"config":[0,1,0,1],"metric":{"Valid":2}},{"config":[1,0,0,1],"metric":{"Valid":2}},{"config":[1,0,1,0],"metric":{"Valid":2}}]},
+    {"problem":"MinimumDominatingSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]},"samples":[{"config":[0,0,1,1,0],"metric":{"Valid":2}}],"optimal":[{"config":[0,0,1,1,0],"metric":{"Valid":2}},{"config":[0,1,0,0,1],"metric":{"Valid":2}},{"config":[0,1,0,1,0],"metric":{"Valid":2}},{"config":[0,1,1,0,0],"metric":{"Valid":2}},{"config":[1,0,0,0,1],"metric":{"Valid":2}},{"config":[1,0,0,1,0],"metric":{"Valid":2}},{"config":[1,0,1,0,0],"metric":{"Valid":2}}]},
+    {"problem":"MinimumFeedbackVertexSet","variant":{"weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"directed","edges":[[0,1,null],[1,2,null],[2,0,null],[0,3,null],[3,4,null],[4,1,null],[4,2,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]},"samples":[{"config":[1,0,0,0,0],"metric":{"Valid":1}}],"optimal":[{"config":[0,0,1,0,0],"metric":{"Valid":1}},{"config":[1,0,0,0,0],"metric":{"Valid":1}}]},
+    {"problem":"MinimumSetCovering","variant":{"weight":"i32"},"instance":{"sets":[[0,1,2],[1,3],[2,3,4]],"universe_size":5,"weights":[1,1,1]},"samples":[{"config":[1,0,1],"metric":{"Valid":2}}],"optimal":[{"config":[1,0,1],"metric":{"Valid":2}}]},
+    {"problem":"MinimumSumMulticenter","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_lengths":[1,1,1,1,1,1,1,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[2,3,null],[3,4,null],[4,5,null],[5,6,null],[0,6,null],[2,5,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null]}},"k":2,"vertex_weights":[1,1,1,1,1,1,1]},"samples":[{"config":[0,0,1,0,0,1,0],"metric":{"Valid":6}}],"optimal":[{"config":[0,0,0,1,0,0,1],"metric":{"Valid":6}},{"config":[0,0,1,0,0,0,1],"metric":{"Valid":6}},{"config":[0,0,1,0,0,1,0],"metric":{"Valid":6}},{"config":[0,1,0,0,0,1,0],"metric":{"Valid":6}},{"config":[0,1,0,0,1,0,0],"metric":{"Valid":6}},{"config":[1,0,0,0,0,1,0],"metric":{"Valid":6}},{"config":[1,0,0,0,1,0,0],"metric":{"Valid":6}},{"config":[1,0,0,1,0,0,0],"metric":{"Valid":6}},{"config":[1,0,1,0,0,0,0],"metric":{"Valid":6}}]},
+    {"problem":"MinimumTardinessSequencing","variant":{},"instance":{"deadlines":[2,3,1,4],"num_tasks":4,"precedences":[[0,2]]},"samples":[{"config":[0,0,0,0],"metric":{"Valid":1}}],"optimal":[{"config":[0,0,0,0],"metric":{"Valid":1}},{"config":[0,0,1,0],"metric":{"Valid":1}},{"config":[0,1,0,0],"metric":{"Valid":1}},{"config":[0,2,0,0],"metric":{"Valid":1}},{"config":[1,0,0,0],"metric":{"Valid":1}},{"config":[1,0,1,0],"metric":{"Valid":1}},{"config":[3,0,0,0],"metric":{"Valid":1}}]},
+    {"problem":"MinimumVertexCover","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]},"samples":[{"config":[1,0,0,1,1],"metric":{"Valid":3}}],"optimal":[{"config":[0,1,1,0,1],"metric":{"Valid":3}},{"config":[0,1,1,1,0],"metric":{"Valid":3}},{"config":[1,0,0,1,1],"metric":{"Valid":3}},{"config":[1,0,1,1,0],"metric":{"Valid":3}}]},
+    {"problem":"PaintShop","variant":{},"instance":{"car_labels":["A","B","C"],"is_first":[true,true,false,true,false,false],"num_cars":3,"sequence_indices":[0,1,0,2,1,2]},"samples":[{"config":[0,0,1],"metric":{"Valid":2}}],"optimal":[{"config":[0,0,1],"metric":{"Valid":2}},{"config":[0,1,1],"metric":{"Valid":2}},{"config":[1,0,0],"metric":{"Valid":2}},{"config":[1,1,0],"metric":{"Valid":2}}]},
+    {"problem":"PartitionIntoTriangles","variant":{"graph":"SimpleGraph"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,2,null],[3,4,null],[3,5,null],[4,5,null],[0,3,null]],"node_holes":[],"nodes":[null,null,null,null,null,null]}}},"samples":[{"config":[0,0,0,1,1,1],"metric":true}],"optimal":[{"config":[0,0,0,1,1,1],"metric":true},{"config":[1,1,1,0,0,0],"metric":true}]},
+    {"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-1.0,2.0,0.0],[0.0,-1.0,2.0],[0.0,0.0,-1.0]],"num_vars":3},"samples":[{"config":[1,0,1],"metric":{"Valid":-2.0}}],"optimal":[{"config":[1,0,1],"metric":{"Valid":-2.0}}]},
+    {"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1,2]},{"literals":[-1,3]},{"literals":[-2,-3]}],"num_vars":3},"samples":[{"config":[1,0,1],"metric":true}],"optimal":[{"config":[0,1,0],"metric":true},{"config":[1,0,1],"metric":true}]},
+    {"problem":"ShortestCommonSupersequence","variant":{},"instance":{"alphabet_size":3,"bound":4,"strings":[[0,1,2],[1,0,2]]},"samples":[{"config":[1,0,1,2],"metric":true}],"optimal":[{"config":[0,1,0,2],"metric":true},{"config":[1,0,1,2],"metric":true}]},
+    {"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"couplings":[1,1,1,1,1,1,1],"fields":[0,0,0,0,0],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[3,4,null],[0,3,null],[1,3,null],[1,4,null],[2,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}}},"samples":[{"config":[1,0,1,1,0],"metric":{"Valid":-3}}],"optimal":[{"config":[0,0,1,1,0],"metric":{"Valid":-3}},{"config":[0,1,0,0,1],"metric":{"Valid":-3}},{"config":[0,1,0,1,0],"metric":{"Valid":-3}},{"config":[0,1,1,1,0],"metric":{"Valid":-3}},{"config":[1,0,0,0,1],"metric":{"Valid":-3}},{"config":[1,0,1,0,1],"metric":{"Valid":-3}},{"config":[1,0,1,1,0],"metric":{"Valid":-3}},{"config":[1,1,0,0,1],"metric":{"Valid":-3}}]},
+    {"problem":"TravelingSalesman","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,3,2,2,3,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[0,3,null],[1,2,null],[1,3,null],[2,3,null]],"node_holes":[],"nodes":[null,null,null,null]}}},"samples":[{"config":[1,0,1,1,0,1],"metric":{"Valid":6}}],"optimal":[{"config":[1,0,1,1,0,1],"metric":{"Valid":6}}]}
+  ],
+  "rules": [
+    {"source":{"problem":"BinPacking","variant":{"weight":"i32"},"instance":{"capacity":10,"sizes":[6,5,5,4,3]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Eq","rhs":1.0,"terms":[[0,1.0],[1,1.0],[2,1.0],[3,1.0],[4,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[5,1.0],[6,1.0],[7,1.0],[8,1.0],[9,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[10,1.0],[11,1.0],[12,1.0],[13,1.0],[14,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[15,1.0],[16,1.0],[17,1.0],[18,1.0],[19,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[20,1.0],[21,1.0],[22,1.0],[23,1.0],[24,1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[0,6.0],[5,5.0],[10,5.0],[15,4.0],[20,3.0],[25,-10.0]]},{"cmp":"Le","rhs":0.0,"terms":[[1,6.0],[6,5.0],[11,5.0],[16,4.0],[21,3.0],[26,-10.0]]},{"cmp":"Le","rhs":0.0,"terms":[[2,6.0],[7,5.0],[12,5.0],[17,4.0],[22,3.0],[27,-10.0]]},{"cmp":"Le","rhs":0.0,"terms":[[3,6.0],[8,5.0],[13,5.0],[18,4.0],[23,3.0],[28,-10.0]]},{"cmp":"Le","rhs":0.0,"terms":[[4,6.0],[9,5.0],[14,5.0],[19,4.0],[24,3.0],[29,-10.0]]}],"num_vars":30,"objective":[[25,1.0],[26,1.0],[27,1.0],[28,1.0],[29,1.0]],"sense":"Minimize"}},"solutions":[{"source_config":[2,1,0,0,2],"target_config":[0,0,1,0,0,0,1,0,0,0,1,0,0,0,0,1,0,0,0,0,0,0,1,0,0,1,1,1,0,0]}]},
+    {"source":{"problem":"CircuitSAT","variant":{},"instance":{"circuit":{"assignments":[{"expr":{"op":{"Xor":[{"op":{"Var":"a"}},{"op":{"Var":"b"}}]}},"outputs":["t"]},{"expr":{"op":{"Xor":[{"op":{"Var":"t"}},{"op":{"Var":"cin"}}]}},"outputs":["sum"]},{"expr":{"op":{"And":[{"op":{"Var":"a"}},{"op":{"Var":"b"}}]}},"outputs":["ab"]},{"expr":{"op":{"And":[{"op":{"Var":"cin"}},{"op":{"Var":"t"}}]}},"outputs":["cin_t"]},{"expr":{"op":{"Or":[{"op":{"Var":"ab"}},{"op":{"Var":"cin_t"}}]}},"outputs":["cout"]}]},"variables":["a","ab","b","cin","cin_t","cout","sum","t"]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":0.0,"terms":[[8,1.0],[0,-1.0],[2,-1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[8,1.0],[0,-1.0],[2,1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[8,1.0],[0,1.0],[2,-1.0]]},{"cmp":"Le","rhs":2.0,"terms":[[8,1.0],[0,1.0],[2,1.0]]},{"cmp":"Eq","rhs":0.0,"terms":[[7,1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[9,1.0],[7,-1.0],[3,-1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[9,1.0],[7,-1.0],[3,1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[9,1.0],[7,1.0],[3,-1.0]]},{"cmp":"Le","rhs":2.0,"terms":[[9,1.0],[7,1.0],[3,1.0]]},{"cmp":"Eq","rhs":0.0,"terms":[[6,1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[10,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[10,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[10,1.0],[0,-1.0],[2,-1.0]]},{"cmp":"Eq","rhs":0.0,"terms":[[1,1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[11,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[11,1.0],[7,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[11,1.0],[3,-1.0],[7,-1.0]]},{"cmp":"Eq","rhs":0.0,"terms":[[4,1.0],[11,-1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[12,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[12,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[12,1.0],[1,-1.0],[4,-1.0]]},{"cmp":"Eq","rhs":0.0,"terms":[[5,1.0],[12,-1.0]]}],"num_vars":13,"objective":[],"sense":"Minimize"}},"solutions":[{"source_config":[0,0,0,0,0,0,0,0],"target_config":[0,0,0,0,0,0,0,0,0,0,0,0,0]}]},
+    {"source":{"problem":"CircuitSAT","variant":{},"instance":{"circuit":{"assignments":[{"expr":{"op":{"Xor":[{"op":{"Var":"a"}},{"op":{"Var":"b"}}]}},"outputs":["t"]},{"expr":{"op":{"Xor":[{"op":{"Var":"t"}},{"op":{"Var":"cin"}}]}},"outputs":["sum"]},{"expr":{"op":{"And":[{"op":{"Var":"a"}},{"op":{"Var":"b"}}]}},"outputs":["ab"]},{"expr":{"op":{"And":[{"op":{"Var":"cin"}},{"op":{"Var":"t"}}]}},"outputs":["cin_t"]},{"expr":{"op":{"Or":[{"op":{"Var":"ab"}},{"op":{"Var":"cin_t"}}]}},"outputs":["cout"]}]},"variables":["a","ab","b","cin","cin_t","cout","sum","t"]}},"target":{"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"couplings":[2,-1,-2,-2,-1,-2,-2,2,-4,2,-1,-2,-2,-1,-2,-2,2,-4,-4,1,-2,-4,-2,-4],"fields":[-2,-2,1,2,-2,-2,1,2,0,2,1,2,1,-2,0],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[0,3,null],[0,9,null],[1,2,null],[1,3,null],[1,9,null],[2,3,null],[2,4,null],[4,5,null],[4,6,null],[4,7,null],[4,11,null],[5,6,null],[5,7,null],[5,11,null],[6,7,null],[6,8,null],[9,10,null],[10,12,null],[10,13,null],[11,12,null],[12,13,null],[13,14,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null,null,null,null,null,null]}}}},"solutions":[{"source_config":[0,0,0,0,0,0,0,0],"target_config":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]}]},
+    {"source":{"problem":"Factoring","variant":{},"instance":{"m":3,"n":3,"target":35}},"target":{"problem":"CircuitSAT","variant":{},"instance":{"circuit":{"assignments":[{"expr":{"op":{"And":[{"op":{"Var":"p1"}},{"op":{"Var":"q1"}}]}},"outputs":["a_1_1"]},{"expr":{"op":{"Xor":[{"op":{"Var":"a_1_1"}},{"op":{"Const":false}}]}},"outputs":["axs_1_1"]},{"expr":{"op":{"Xor":[{"op":{"Var":"axs_1_1"}},{"op":{"Const":false}}]}},"outputs":["s1_1"]},{"expr":{"op":{"And":[{"op":{"Var":"axs_1_1"}},{"op":{"Const":false}}]}},"outputs":["axsc_1_1"]},{"expr":{"op":{"And":[{"op":{"Var":"a_1_1"}},{"op":{"Const":false}}]}},"outputs":["as_1_1"]},{"expr":{"op":{"Or":[{"op":{"Var":"axsc_1_1"}},{"op":{"Var":"as_1_1"}}]}},"outputs":["c1_1"]},{"expr":{"op":{"And":[{"op":{"Var":"p1"}},{"op":{"Var":"q2"}}]}},"outputs":["a_1_2"]},{"expr":{"op":{"Xor":[{"op":{"Var":"a_1_2"}},{"op":{"Const":false}}]}},"outputs":["axs_1_2"]},{"expr":{"op":{"Xor":[{"op":{"Var":"axs_1_2"}},{"op":{"Var":"c1_1"}}]}},"outputs":["s1_2"]},{"expr":{"op":{"And":[{"op":{"Var":"axs_1_2"}},{"op":{"Var":"c1_1"}}]}},"outputs":["axsc_1_2"]},{"expr":{"op":{"And":[{"op":{"Var":"a_1_2"}},{"op":{"Const":false}}]}},"outputs":["as_1_2"]},{"expr":{"op":{"Or":[{"op":{"Var":"axsc_1_2"}},{"op":{"Var":"as_1_2"}}]}},"outputs":["c1_2"]},{"expr":{"op":{"And":[{"op":{"Var":"p1"}},{"op":{"Var":"q3"}}]}},"outputs":["a_1_3"]},{"expr":{"op":{"Xor":[{"op":{"Var":"a_1_3"}},{"op":{"Const":false}}]}},"outputs":["axs_1_3"]},{"expr":{"op":{"Xor":[{"op":{"Var":"axs_1_3"}},{"op":{"Var":"c1_2"}}]}},"outputs":["s1_3"]},{"expr":{"op":{"And":[{"op":{"Var":"axs_1_3"}},{"op":{"Var":"c1_2"}}]}},"outputs":["axsc_1_3"]},{"expr":{"op":{"And":[{"op":{"Var":"a_1_3"}},{"op":{"Const":false}}]}},"outputs":["as_1_3"]},{"expr":{"op":{"Or":[{"op":{"Var":"axsc_1_3"}},{"op":{"Var":"as_1_3"}}]}},"outputs":["c1_3"]},{"expr":{"op":{"And":[{"op":{"Var":"p2"}},{"op":{"Var":"q1"}}]}},"outputs":["a_2_1"]},{"expr":{"op":{"Xor":[{"op":{"Var":"a_2_1"}},{"op":{"Var":"s1_2"}}]}},"outputs":["axs_2_1"]},{"expr":{"op":{"Xor":[{"op":{"Var":"axs_2_1"}},{"op":{"Const":false}}]}},"outputs":["s2_1"]},{"expr":{"op":{"And":[{"op":{"Var":"axs_2_1"}},{"op":{"Const":false}}]}},"outputs":["axsc_2_1"]},{"expr":{"op":{"And":[{"op":{"Var":"a_2_1"}},{"op":{"Var":"s1_2"}}]}},"outputs":["as_2_1"]},{"expr":{"op":{"Or":[{"op":{"Var":"axsc_2_1"}},{"op":{"Var":"as_2_1"}}]}},"outputs":["c2_1"]},{"expr":{"op":{"And":[{"op":{"Var":"p2"}},{"op":{"Var":"q2"}}]}},"outputs":["a_2_2"]},{"expr":{"op":{"Xor":[{"op":{"Var":"a_2_2"}},{"op":{"Var":"s1_3"}}]}},"outputs":["axs_2_2"]},{"expr":{"op":{"Xor":[{"op":{"Var":"axs_2_2"}},{"op":{"Var":"c2_1"}}]}},"outputs":["s2_2"]},{"expr":{"op":{"And":[{"op":{"Var":"axs_2_2"}},{"op":{"Var":"c2_1"}}]}},"outputs":["axsc_2_2"]},{"expr":{"op":{"And":[{"op":{"Var":"a_2_2"}},{"op":{"Var":"s1_3"}}]}},"outputs":["as_2_2"]},{"expr":{"op":{"Or":[{"op":{"Var":"axsc_2_2"}},{"op":{"Var":"as_2_2"}}]}},"outputs":["c2_2"]},{"expr":{"op":{"And":[{"op":{"Var":"p2"}},{"op":{"Var":"q3"}}]}},"outputs":["a_2_3"]},{"expr":{"op":{"Xor":[{"op":{"Var":"a_2_3"}},{"op":{"Var":"c1_3"}}]}},"outputs":["axs_2_3"]},{"expr":{"op":{"Xor":[{"op":{"Var":"axs_2_3"}},{"op":{"Var":"c2_2"}}]}},"outputs":["s2_3"]},{"expr":{"op":{"And":[{"op":{"Var":"axs_2_3"}},{"op":{"Var":"c2_2"}}]}},"outputs":["axsc_2_3"]},{"expr":{"op":{"And":[{"op":{"Var":"a_2_3"}},{"op":{"Var":"c1_3"}}]}},"outputs":["as_2_3"]},{"expr":{"op":{"Or":[{"op":{"Var":"axsc_2_3"}},{"op":{"Var":"as_2_3"}}]}},"outputs":["c2_3"]},{"expr":{"op":{"And":[{"op":{"Var":"p3"}},{"op":{"Var":"q1"}}]}},"outputs":["a_3_1"]},{"expr":{"op":{"Xor":[{"op":{"Var":"a_3_1"}},{"op":{"Var":"s2_2"}}]}},"outputs":["axs_3_1"]},{"expr":{"op":{"Xor":[{"op":{"Var":"axs_3_1"}},{"op":{"Const":false}}]}},"outputs":["s3_1"]},{"expr":{"op":{"And":[{"op":{"Var":"axs_3_1"}},{"op":{"Const":false}}]}},"outputs":["axsc_3_1"]},{"expr":{"op":{"And":[{"op":{"Var":"a_3_1"}},{"op":{"Var":"s2_2"}}]}},"outputs":["as_3_1"]},{"expr":{"op":{"Or":[{"op":{"Var":"axsc_3_1"}},{"op":{"Var":"as_3_1"}}]}},"outputs":["c3_1"]},{"expr":{"op":{"And":[{"op":{"Var":"p3"}},{"op":{"Var":"q2"}}]}},"outputs":["a_3_2"]},{"expr":{"op":{"Xor":[{"op":{"Var":"a_3_2"}},{"op":{"Var":"s2_3"}}]}},"outputs":["axs_3_2"]},{"expr":{"op":{"Xor":[{"op":{"Var":"axs_3_2"}},{"op":{"Var":"c3_1"}}]}},"outputs":["s3_2"]},{"expr":{"op":{"And":[{"op":{"Var":"axs_3_2"}},{"op":{"Var":"c3_1"}}]}},"outputs":["axsc_3_2"]},{"expr":{"op":{"And":[{"op":{"Var":"a_3_2"}},{"op":{"Var":"s2_3"}}]}},"outputs":["as_3_2"]},{"expr":{"op":{"Or":[{"op":{"Var":"axsc_3_2"}},{"op":{"Var":"as_3_2"}}]}},"outputs":["c3_2"]},{"expr":{"op":{"And":[{"op":{"Var":"p3"}},{"op":{"Var":"q3"}}]}},"outputs":["a_3_3"]},{"expr":{"op":{"Xor":[{"op":{"Var":"a_3_3"}},{"op":{"Var":"c2_3"}}]}},"outputs":["axs_3_3"]},{"expr":{"op":{"Xor":[{"op":{"Var":"axs_3_3"}},{"op":{"Var":"c3_2"}}]}},"outputs":["s3_3"]},{"expr":{"op":{"And":[{"op":{"Var":"axs_3_3"}},{"op":{"Var":"c3_2"}}]}},"outputs":["axsc_3_3"]},{"expr":{"op":{"And":[{"op":{"Var":"a_3_3"}},{"op":{"Var":"c2_3"}}]}},"outputs":["as_3_3"]},{"expr":{"op":{"Or":[{"op":{"Var":"axsc_3_3"}},{"op":{"Var":"as_3_3"}}]}},"outputs":["c3_3"]},{"expr":{"op":{"Const":true}},"outputs":["s1_1"]},{"expr":{"op":{"Const":true}},"outputs":["s2_1"]},{"expr":{"op":{"Const":false}},"outputs":["s3_1"]},{"expr":{"op":{"Const":false}},"outputs":["s3_2"]},{"expr":{"op":{"Const":false}},"outputs":["s3_3"]},{"expr":{"op":{"Const":true}},"outputs":["c3_3"]}]},"variables":["a_1_1","a_1_2","a_1_3","a_2_1","a_2_2","a_2_3","a_3_1","a_3_2","a_3_3","as_1_1","as_1_2","as_1_3","as_2_1","as_2_2","as_2_3","as_3_1","as_3_2","as_3_3","axs_1_1","axs_1_2","axs_1_3","axs_2_1","axs_2_2","axs_2_3","axs_3_1","axs_3_2","axs_3_3","axsc_1_1","axsc_1_2","axsc_1_3","axsc_2_1","axsc_2_2","axsc_2_3","axsc_3_1","axsc_3_2","axsc_3_3","c1_1","c1_2","c1_3","c2_1","c2_2","c2_3","c3_1","c3_2","c3_3","p1","p2","p3","q1","q2","q3","s1_1","s1_2","s1_3","s2_1","s2_2","s2_3","s3_1","s3_2","s3_3"]}},"solutions":[{"source_config":[1,0,1,1,1,1],"target_config":[1,1,1,0,0,0,1,1,1,0,0,0,0,0,0,1,0,0,1,1,1,1,1,0,0,1,1,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,1,1,1,1,0,1,1,1,1,1,1,1,1,1,0,0,0,0]}]},
+    {"source":{"problem":"Factoring","variant":{},"instance":{"m":3,"n":3,"target":35}},"target":{"problem":"ILP","variant":{"variable":"i32"},"instance":{"constraints":[{"cmp":"Le","rhs":0.0,"terms":[[6,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[6,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[6,1.0],[0,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[7,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[7,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[7,1.0],[0,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[8,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[8,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[8,1.0],[0,-1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[9,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[9,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[9,1.0],[1,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[10,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[10,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[10,1.0],[1,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[11,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[11,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[11,1.0],[1,-1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[12,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[12,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[12,1.0],[2,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[13,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[13,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[13,1.0],[2,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[14,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[14,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[14,1.0],[2,-1.0],[5,-1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[6,1.0],[15,-2.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[7,1.0],[9,1.0],[15,1.0],[16,-2.0]]},{"cmp":"Eq","rhs":0.0,"terms":[[8,1.0],[10,1.0],[12,1.0],[16,1.0],[17,-2.0]]},{"cmp":"Eq","rhs":0.0,"terms":[[11,1.0],[13,1.0],[17,1.0],[18,-2.0]]},{"cmp":"Eq","rhs":0.0,"terms":[[14,1.0],[18,1.0],[19,-2.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[19,1.0],[20,-2.0]]},{"cmp":"Eq","rhs":0.0,"terms":[[20,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[3,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[15,1.0]]},{"cmp":"Le","rhs":3.0,"terms":[[15,1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[16,1.0]]},{"cmp":"Le","rhs":3.0,"terms":[[16,1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[17,1.0]]},{"cmp":"Le","rhs":3.0,"terms":[[17,1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[18,1.0]]},{"cmp":"Le","rhs":3.0,"terms":[[18,1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[19,1.0]]},{"cmp":"Le","rhs":3.0,"terms":[[19,1.0]]},{"cmp":"Ge","rhs":0.0,"terms":[[20,1.0]]},{"cmp":"Le","rhs":3.0,"terms":[[20,1.0]]}],"num_vars":21,"objective":[],"sense":"Minimize"}},"solutions":[{"source_config":[1,0,1,1,1,1],"target_config":[1,0,1,1,1,1,1,1,1,0,0,0,1,1,1,0,0,1,1,1,0]}]},
+    {"source":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":10.0,"terms":[[0,3.0],[1,2.0],[2,5.0],[3,4.0],[4,2.0],[5,3.0]]},{"cmp":"Le","rhs":2.0,"terms":[[0,1.0],[1,1.0],[2,1.0]]},{"cmp":"Le","rhs":2.0,"terms":[[3,1.0],[4,1.0],[5,1.0]]}],"num_vars":6,"objective":[[0,10.0],[1,7.0],[2,12.0],[3,8.0],[4,6.0],[5,9.0]],"sense":"Maximize"}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-3628.0,938.0,2144.0,1608.0,804.0,1206.0,402.0,804.0,1608.0,3216.0,134.0,268.0,0.0,0.0],[0.0,-2620.0,1474.0,1072.0,536.0,804.0,268.0,536.0,1072.0,2144.0,134.0,268.0,0.0,0.0],[0.0,0.0,-5238.0,2680.0,1340.0,2010.0,670.0,1340.0,2680.0,5360.0,134.0,268.0,0.0,0.0],[0.0,0.0,0.0,-4497.0,1206.0,1742.0,536.0,1072.0,2144.0,4288.0,0.0,0.0,134.0,268.0],[0.0,0.0,0.0,0.0,-2619.0,938.0,268.0,536.0,1072.0,2144.0,0.0,0.0,134.0,268.0],[0.0,0.0,0.0,0.0,0.0,-3627.0,402.0,804.0,1608.0,3216.0,0.0,0.0,134.0,268.0],[0.0,0.0,0.0,0.0,0.0,0.0,-1273.0,268.0,536.0,1072.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,-2412.0,1072.0,2144.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-4288.0,4288.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6432.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-201.0,268.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-268.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-201.0,268.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-268.0]],"num_vars":14}},"solutions":[{"source_config":[1,1,0,0,1,1],"target_config":[1,1,0,0,1,1,0,0,0,0,0,0,0,0]}]},
+    {"source":{"problem":"KColoring","variant":{"graph":"SimpleGraph","k":"KN"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}},"num_colors":3}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Eq","rhs":1.0,"terms":[[0,1.0],[1,1.0],[2,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[3,1.0],[4,1.0],[5,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[6,1.0],[7,1.0],[8,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[9,1.0],[10,1.0],[11,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[12,1.0],[13,1.0],[14,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[15,1.0],[16,1.0],[17,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[18,1.0],[19,1.0],[20,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[21,1.0],[22,1.0],[23,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[24,1.0],[25,1.0],[26,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[27,1.0],[28,1.0],[29,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[3,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[12,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[13,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[14,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[15,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[16,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[17,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[3,1.0],[6,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[4,1.0],[7,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0],[8,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[3,1.0],[18,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[4,1.0],[19,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0],[20,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[6,1.0],[9,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[7,1.0],[10,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[8,1.0],[11,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[6,1.0],[21,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[7,1.0],[22,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[8,1.0],[23,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[9,1.0],[12,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[10,1.0],[13,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[11,1.0],[14,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[9,1.0],[24,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[10,1.0],[25,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[11,1.0],[26,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[12,1.0],[27,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[13,1.0],[28,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[14,1.0],[29,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[15,1.0],[21,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[16,1.0],[22,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[17,1.0],[23,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[15,1.0],[24,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[16,1.0],[25,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[17,1.0],[26,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[18,1.0],[24,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[19,1.0],[25,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[20,1.0],[26,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[18,1.0],[27,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[19,1.0],[28,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[20,1.0],[29,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[21,1.0],[27,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[22,1.0],[28,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[23,1.0],[29,1.0]]}],"num_vars":30,"objective":[],"sense":"Minimize"}},"solutions":[{"source_config":[0,2,0,1,2,1,1,2,0,0],"target_config":[1,0,0,0,0,1,1,0,0,0,1,0,0,0,1,0,1,0,0,1,0,0,0,1,1,0,0,1,0,0]}]},
+    {"source":{"problem":"KColoring","variant":{"graph":"SimpleGraph","k":"KN"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,3,null],[2,3,null],[2,4,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"num_colors":3}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-6.0,12.0,12.0,3.0,0.0,0.0,3.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0],[0.0,-6.0,12.0,0.0,3.0,0.0,0.0,3.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0],[0.0,0.0,-6.0,0.0,0.0,3.0,0.0,0.0,3.0,0.0,0.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,-6.0,12.0,12.0,0.0,0.0,0.0,3.0,0.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,-6.0,12.0,0.0,0.0,0.0,0.0,3.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,-6.0,0.0,0.0,0.0,0.0,0.0,3.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,-6.0,12.0,12.0,3.0,0.0,0.0,3.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6.0,12.0,0.0,3.0,0.0,0.0,3.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6.0,0.0,0.0,3.0,0.0,0.0,3.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6.0,12.0,12.0,3.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6.0,12.0,0.0,3.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6.0,0.0,0.0,3.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6.0,12.0,12.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6.0,12.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6.0]],"num_vars":15}},"solutions":[{"source_config":[1,2,2,1,0],"target_config":[0,1,0,0,0,1,0,0,1,0,1,0,1,0,0]}]},
+    {"source":{"problem":"KSatisfiability","variant":{"k":"K2"},"instance":{"clauses":[{"literals":[1,2]},{"literals":[-1,3]},{"literals":[-2,4]},{"literals":[-3,-4]}],"num_vars":4}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[0.0,1.0,-1.0,0.0],[0.0,0.0,0.0,-1.0],[0.0,0.0,0.0,1.0],[0.0,0.0,0.0,0.0]],"num_vars":4}},"solutions":[{"source_config":[0,1,0,1],"target_config":[0,1,0,1]}]},
+    {"source":{"problem":"KSatisfiability","variant":{"k":"K3"},"instance":{"clauses":[{"literals":[1,2,-3]},{"literals":[-1,3,4]},{"literals":[2,-4,5]},{"literals":[-2,3,-5]},{"literals":[1,-3,5]},{"literals":[-1,-2,4]},{"literals":[3,-4,-5]}],"num_vars":5}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[0.0,4.0,-4.0,0.0,0.0,4.0,-4.0,0.0,0.0,4.0,-4.0,0.0],[0.0,0.0,-2.0,-2.0,0.0,4.0,0.0,4.0,-4.0,0.0,-4.0,0.0],[0.0,0.0,2.0,-2.0,0.0,1.0,4.0,0.0,4.0,-4.0,0.0,4.0],[0.0,0.0,0.0,4.0,0.0,0.0,-1.0,-4.0,0.0,0.0,-1.0,-4.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,-1.0,1.0,-1.0,0.0,1.0],[0.0,0.0,0.0,0.0,0.0,-2.0,0.0,0.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,3.0,0.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,3.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,2.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,3.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,7.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,2.0]],"num_vars":12}},"solutions":[{"source_config":[1,1,1,1,1],"target_config":[1,1,1,1,1,0,0,0,0,0,1,0]}]},
+    {"source":{"problem":"KSatisfiability","variant":{"k":"K3"},"instance":{"clauses":[{"literals":[1,2,3]},{"literals":[-1,-2,3]}],"num_vars":3}},"target":{"problem":"SubsetSum","variant":{},"instance":{"sizes":["10010","10001","1010","1001","111","100","10","20","1","2"],"target":"11144"}},"solutions":[{"source_config":[0,0,1],"target_config":[0,1,0,1,1,0,1,1,1,0]}]},
+    {"source":{"problem":"KSatisfiability","variant":{"k":"KN"},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,3,4]},{"literals":[2,-3,-4]}],"num_vars":4}},"target":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,3,4]},{"literals":[2,-3,-4]}],"num_vars":4}},"solutions":[{"source_config":[1,1,1,0],"target_config":[1,1,1,0]}]},
+    {"source":{"problem":"Knapsack","variant":{},"instance":{"capacity":7,"values":[3,4,5,7],"weights":[2,3,4,5]}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-483.0,240.0,320.0,400.0,80.0,160.0,320.0],[0.0,-664.0,480.0,600.0,120.0,240.0,480.0],[0.0,0.0,-805.0,800.0,160.0,320.0,640.0],[0.0,0.0,0.0,-907.0,200.0,400.0,800.0],[0.0,0.0,0.0,0.0,-260.0,80.0,160.0],[0.0,0.0,0.0,0.0,0.0,-480.0,320.0],[0.0,0.0,0.0,0.0,0.0,0.0,-800.0]],"num_vars":7}},"solutions":[{"source_config":[1,0,0,1],"target_config":[1,0,0,1,0,0,0]}]},
+    {"source":{"problem":"LongestCommonSubsequence","variant":{},"instance":{"strings":[[65,66,65,67],[66,65,67,65]]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[1,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[3,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[3,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[3,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[4,1.0],[5,1.0]]}],"num_vars":6,"objective":[[0,1.0],[1,1.0],[2,1.0],[3,1.0],[4,1.0],[5,1.0]],"sense":"Maximize"}},"solutions":[{"source_config":[0,1,1,1],"target_config":[0,0,1,1,0,1]}]},
+    {"source":{"problem":"MaxCut","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"target":{"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"couplings":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],"fields":[0,0,0,0,0,0,0,0,0,0],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"solutions":[{"source_config":[1,0,1,0,0,0,0,0,1,1],"target_config":[1,0,1,0,0,0,0,0,1,1]}]},
+    {"source":{"problem":"MaximumClique","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[0,3,null],[0,4,null],[1,2,null],[1,3,null],[1,5,null],[2,4,null],[2,5,null],[3,4,null],[3,5,null],[4,5,null]],"node_holes":[],"nodes":[null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[3,1.0]]}],"num_vars":6,"objective":[[0,1.0],[1,1.0],[2,1.0],[3,1.0],[4,1.0],[5,1.0]],"sense":"Maximize"}},"solutions":[{"source_config":[1,1,1,0,0,0],"target_config":[1,1,1,0,0,0]}]},
+    {"source":{"problem":"MaximumClique","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[2,3,null]],"node_holes":[],"nodes":[null,null,null,null]}},"weights":[1,1,1,1]}},"target":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,2,null],[0,3,null],[1,3,null]],"node_holes":[],"nodes":[null,null,null,null]}},"weights":[1,1,1,1]}},"solutions":[{"source_config":[0,1,1,0],"target_config":[0,1,1,0]}]},
+    {"source":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"One"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MaximumSetPacking","variant":{"weight":"One"},"instance":{"sets":[[0,1,2],[0,3,4],[3,5,6],[5,7,8],[1,7,9],[2,10,11],[4,12,13],[6,10,14],[8,11,12],[9,13,14]],"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[1,0,1,0,0,0,0,0,1,1],"target_config":[1,0,1,0,0,0,0,0,1,1]}]},
+    {"source":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[2,3,null],[3,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]}},"target":{"problem":"MaximumClique","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,2,null],[0,3,null],[0,4,null],[1,3,null],[1,4,null],[2,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]}},"solutions":[{"source_config":[1,0,1,0,1],"target_config":[1,0,1,0,1]}]},
+    {"source":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MaximumSetPacking","variant":{"weight":"i32"},"instance":{"sets":[[0,1,2],[0,3,4],[3,5,6],[5,7,8],[1,7,9],[2,10,11],[4,12,13],[6,10,14],[8,11,12],[9,13,14]],"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[1,0,1,0,0,0,0,0,1,1],"target_config":[1,0,1,0,0,0,0,0,1,1]}]},
+    {"source":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MinimumVertexCover","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[1,0,1,0,0,0,0,0,1,1],"target_config":[0,1,0,1,1,1,1,1,0,0]}]},
+    {"source":{"problem":"MaximumMatching","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[1,1.0],[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[3,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[3,1.0],[5,1.0],[6,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0],[7,1.0],[8,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[7,1.0],[9,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[10,1.0],[11,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[4,1.0],[12,1.0],[13,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[6,1.0],[10,1.0],[14,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[8,1.0],[11,1.0],[12,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[9,1.0],[13,1.0],[14,1.0]]}],"num_vars":15,"objective":[[0,1.0],[1,1.0],[2,1.0],[3,1.0],[4,1.0],[5,1.0],[6,1.0],[7,1.0],[8,1.0],[9,1.0],[10,1.0],[11,1.0],[12,1.0],[13,1.0],[14,1.0]],"sense":"Maximize"}},"solutions":[{"source_config":[0,0,1,1,0,0,0,1,0,0,0,0,1,0,1],"target_config":[0,0,1,1,0,0,0,1,0,0,0,0,1,0,1]}]},
+    {"source":{"problem":"MaximumMatching","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"target":{"problem":"MaximumSetPacking","variant":{"weight":"i32"},"instance":{"sets":[[0,1],[0,4],[0,5],[1,2],[1,6],[2,3],[2,7],[3,4],[3,8],[4,9],[5,7],[5,8],[6,8],[6,9],[7,9]],"weights":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[0,0,1,1,0,0,0,1,0,0,0,0,1,0,1],"target_config":[0,0,1,1,0,0,0,1,0,0,0,0,1,0,1]}]},
+    {"source":{"problem":"MaximumSetPacking","variant":{"weight":"One"},"instance":{"sets":[[0,1,2],[2,3],[4,5,6],[1,5,7],[3,6]],"weights":[1,1,1,1,1]}},"target":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"One"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,3,null],[1,4,null],[2,3,null],[2,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]}},"solutions":[{"source_config":[1,0,0,0,1],"target_config":[1,0,0,0,1]}]},
+    {"source":{"problem":"MaximumSetPacking","variant":{"weight":"f64"},"instance":{"sets":[[0,1,2],[2,3,4],[4,5,6],[6,7,0],[1,3,5],[0,4,7]],"weights":[1.0,1.0,1.0,1.0,1.0,1.0]}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-1.0,7.0,0.0,7.0,7.0,7.0],[0.0,-1.0,7.0,0.0,7.0,7.0],[0.0,0.0,-1.0,7.0,7.0,7.0],[0.0,0.0,0.0,-1.0,0.0,7.0],[0.0,0.0,0.0,0.0,-1.0,0.0],[0.0,0.0,0.0,0.0,0.0,-1.0]],"num_vars":6}},"solutions":[{"source_config":[0,0,0,1,1,0],"target_config":[0,0,0,1,1,0]}]},
+    {"source":{"problem":"MaximumSetPacking","variant":{"weight":"i32"},"instance":{"sets":[[0,1,2],[2,3,4],[4,5,6],[6,7,0],[1,3,5],[0,4,7]],"weights":[1,1,1,1,1,1]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[3,1.0],[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[1,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[2,1.0],[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0],[3,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[3,1.0],[5,1.0]]}],"num_vars":6,"objective":[[0,1.0],[1,1.0],[2,1.0],[3,1.0],[4,1.0],[5,1.0]],"sense":"Maximize"}},"solutions":[{"source_config":[0,0,0,1,1,0],"target_config":[0,0,0,1,1,0]}]},
+    {"source":{"problem":"MaximumSetPacking","variant":{"weight":"i32"},"instance":{"sets":[[0,1,2],[2,3],[4,5,6],[1,5,7],[3,6]],"weights":[1,1,1,1,1]}},"target":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,3,null],[1,4,null],[2,3,null],[2,4,null]],"node_holes":[],"nodes":[null,null,null,null,null]}},"weights":[1,1,1,1,1]}},"solutions":[{"source_config":[1,0,0,0,1],"target_config":[1,0,0,0,1]}]},
+    {"source":{"problem":"MinimumDominatingSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Ge","rhs":1.0,"terms":[[0,1.0],[5,1.0],[4,1.0],[1,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[1,1.0],[6,1.0],[2,1.0],[0,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[2,1.0],[7,1.0],[3,1.0],[1,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[3,1.0],[8,1.0],[4,1.0],[2,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[4,1.0],[9,1.0],[3,1.0],[0,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[5,1.0],[8,1.0],[7,1.0],[0,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[6,1.0],[9,1.0],[8,1.0],[1,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[7,1.0],[9,1.0],[5,1.0],[2,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[8,1.0],[6,1.0],[5,1.0],[3,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[9,1.0],[7,1.0],[6,1.0],[4,1.0]]}],"num_vars":10,"objective":[[0,1.0],[1,1.0],[2,1.0],[3,1.0],[4,1.0],[5,1.0],[6,1.0],[7,1.0],[8,1.0],[9,1.0]],"sense":"Minimize"}},"solutions":[{"source_config":[0,0,1,0,0,1,0,0,0,1],"target_config":[0,0,1,0,0,1,0,0,0,1]}]},
+    {"source":{"problem":"MinimumSetCovering","variant":{"weight":"i32"},"instance":{"sets":[[0,1,2],[2,3,4],[4,5,6],[6,7,0],[1,3,5],[0,4,7]],"universe_size":8,"weights":[1,1,1,1,1,1]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Ge","rhs":1.0,"terms":[[0,1.0],[3,1.0],[5,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[0,1.0],[4,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[0,1.0],[1,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[1,1.0],[4,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[1,1.0],[2,1.0],[5,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[2,1.0],[4,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[2,1.0],[3,1.0]]},{"cmp":"Ge","rhs":1.0,"terms":[[3,1.0],[5,1.0]]}],"num_vars":6,"objective":[[0,1.0],[1,1.0],[2,1.0],[3,1.0],[4,1.0],[5,1.0]],"sense":"Minimize"}},"solutions":[{"source_config":[0,1,0,1,1,0],"target_config":[0,1,0,1,1,0]}]},
+    {"source":{"problem":"MinimumVertexCover","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[0,1,0,1,1,1,1,1,0,0],"target_config":[1,0,1,0,0,0,0,0,1,1]}]},
+    {"source":{"problem":"MinimumVertexCover","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1]}},"target":{"problem":"MinimumSetCovering","variant":{"weight":"i32"},"instance":{"sets":[[0,1,2],[0,3,4],[3,5,6],[5,7,8],[1,7,9],[2,10,11],[4,12,13],[6,10,14],[8,11,12],[9,13,14]],"universe_size":15,"weights":[1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[0,1,0,1,1,1,1,1,0,0],"target_config":[0,1,0,1,1,1,1,1,0,0]}]},
+    {"source":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-2.0,1.0,0.0,0.0],[0.0,-3.0,2.0,0.0],[0.0,0.0,-1.0,-1.0],[0.0,0.0,0.0,-4.0]],"num_vars":4}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":0.0,"terms":[[4,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[4,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[4,1.0],[0,-1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[5,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[5,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[5,1.0],[1,-1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[6,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[6,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[6,1.0],[2,-1.0],[3,-1.0]]}],"num_vars":7,"objective":[[0,-2.0],[1,-3.0],[2,-1.0],[3,-4.0],[4,1.0],[5,2.0],[6,-1.0]],"sense":"Minimize"}},"solutions":[{"source_config":[1,1,1,1],"target_config":[1,1,1,1,1,1,1]}]},
+    {"source":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-1.0,2.0,0.0,0.0,-1.5,2.0,0.0,0.0,0.0,0.0],[0.0,-0.8,-1.5,0.0,0.0,0.0,2.0,0.0,0.0,0.0],[0.0,0.0,-0.6,-1.5,0.0,0.0,0.0,2.0,0.0,0.0],[0.0,0.0,0.0,-0.3999999999999999,-1.5,0.0,0.0,0.0,2.0,0.0],[0.0,0.0,0.0,0.0,-0.19999999999999996,0.0,0.0,0.0,0.0,-1.5],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,2.0,-1.5,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.20000000000000018,0.0,2.0,-1.5],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.40000000000000013,0.0,2.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.6000000000000001,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.8]],"num_vars":10}},"target":{"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"f64"},"instance":{"couplings":[0.5,-0.375,0.5,-0.375,0.5,-0.375,0.5,-0.375,0.5,-0.375,0.5,-0.375,0.5,-0.375,0.5],"fields":[0.125,0.22499999999999998,-0.55,-0.44999999999999996,-1.225,0.625,0.7250000000000001,1.7000000000000002,0.925,0.15000000000000002],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"solutions":[{"source_config":[1,0,1,1,1,0,1,0,0,1],"target_config":[1,0,1,1,1,0,1,0,0,1]}]},
+    {"source":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,2]},{"literals":[2,3]}],"num_vars":3}},"target":{"problem":"CircuitSAT","variant":{},"instance":{"circuit":{"assignments":[{"expr":{"op":{"Or":[{"op":{"Var":"x1"}},{"op":{"Not":{"op":{"Var":"x2"}}}},{"op":{"Var":"x3"}}]}},"outputs":["__clause_0"]},{"expr":{"op":{"Or":[{"op":{"Not":{"op":{"Var":"x1"}}}},{"op":{"Var":"x2"}}]}},"outputs":["__clause_1"]},{"expr":{"op":{"Or":[{"op":{"Var":"x2"}},{"op":{"Var":"x3"}}]}},"outputs":["__clause_2"]},{"expr":{"op":{"And":[{"op":{"Var":"__clause_0"}},{"op":{"Var":"__clause_1"}},{"op":{"Var":"__clause_2"}}]}},"outputs":["__out"]},{"expr":{"op":{"Const":true}},"outputs":["__out"]}]},"variables":["__clause_0","__clause_1","__clause_2","__out","x1","x2","x3"]}},"solutions":[{"source_config":[1,1,1],"target_config":[1,1,1,1,1,1,1]}]},
+    {"source":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1]},{"literals":[-3]},{"literals":[5]}],"num_vars":5}},"target":{"problem":"KColoring","variant":{"graph":"SimpleGraph","k":"K3"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,2,null],[3,2,null],[8,2,null],[3,8,null],[4,2,null],[9,2,null],[4,9,null],[5,2,null],[10,2,null],[5,10,null],[6,2,null],[11,2,null],[6,11,null],[7,2,null],[12,2,null],[7,12,null],[3,2,null],[3,1,null],[10,2,null],[10,1,null],[7,2,null],[7,1,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null,null,null,null]}},"num_colors":3}},"solutions":[{"source_config":[1,1,0,1,1],"target_config":[2,1,0,2,2,1,2,2,1,1,2,1,1]}]},
+    {"source":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1]},{"literals":[2,-3]},{"literals":[-1,3,4]},{"literals":[2,-4,5]},{"literals":[1,-2,3,-5]},{"literals":[-1,2,-3,4,5]}],"num_vars":5}},"target":{"problem":"KSatisfiability","variant":{"k":"K3"},"instance":{"clauses":[{"literals":[1,6,7]},{"literals":[1,6,-7]},{"literals":[1,-6,8]},{"literals":[1,-6,-8]},{"literals":[2,-3,9]},{"literals":[2,-3,-9]},{"literals":[-1,3,4]},{"literals":[2,-4,5]},{"literals":[1,-2,10]},{"literals":[-10,3,-5]},{"literals":[-1,2,11]},{"literals":[-11,-3,12]},{"literals":[-12,4,5]}],"num_vars":12}},"solutions":[{"source_config":[1,0,0,1,1],"target_config":[1,0,0,1,1,0,0,0,0,0,1,1]}]},
+    {"source":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1,2,-3]},{"literals":[-1,3,4]},{"literals":[2,-4,5]},{"literals":[-2,3,-5]},{"literals":[1,-3,5]},{"literals":[-1,-2,4]},{"literals":[3,-4,-5]}],"num_vars":5}},"target":{"problem":"MaximumIndependentSet","variant":{"graph":"SimpleGraph","weight":"One"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,2,null],[3,4,null],[3,5,null],[4,5,null],[6,7,null],[6,8,null],[7,8,null],[9,10,null],[9,11,null],[10,11,null],[12,13,null],[12,14,null],[13,14,null],[15,16,null],[15,17,null],[16,17,null],[18,19,null],[18,20,null],[19,20,null],[0,3,null],[0,15,null],[1,9,null],[1,16,null],[2,4,null],[2,10,null],[2,18,null],[3,12,null],[4,13,null],[5,7,null],[5,19,null],[6,9,null],[6,16,null],[7,17,null],[8,11,null],[8,20,null],[10,13,null],[11,14,null],[12,15,null],[13,18,null],[14,20,null],[17,19,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[1,1,1,1,0],"target_config":[1,0,0,0,1,0,1,0,0,0,0,1,1,0,0,0,0,1,1,0,0]}]},
+    {"source":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1,2,-3]},{"literals":[-1,3,4]},{"literals":[2,-4,5]},{"literals":[-2,3,-5]},{"literals":[1,-3,5]},{"literals":[-1,-2,4]},{"literals":[3,-4,-5]}],"num_vars":5}},"target":{"problem":"MinimumDominatingSet","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,2,null],[3,4,null],[3,5,null],[4,5,null],[6,7,null],[6,8,null],[7,8,null],[9,10,null],[9,11,null],[10,11,null],[12,13,null],[12,14,null],[13,14,null],[0,15,null],[3,15,null],[7,15,null],[1,16,null],[6,16,null],[9,16,null],[3,17,null],[10,17,null],[12,17,null],[4,18,null],[6,18,null],[13,18,null],[0,19,null],[7,19,null],[12,19,null],[1,20,null],[4,20,null],[9,20,null],[6,21,null],[10,21,null],[13,21,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null]}},"weights":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]}},"solutions":[{"source_config":[1,0,1,1,1],"target_config":[1,0,0,0,1,0,1,0,0,1,0,0,1,0,0,0,0,0,0,0,0,0]}]},
+    {"source":{"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"f64"},"instance":{"couplings":[1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0,-1.0,1.0],"fields":[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-2.0,4.0,0.0,0.0,-4.0,4.0,0.0,0.0,0.0,0.0],[0.0,-2.0,-4.0,0.0,0.0,0.0,4.0,0.0,0.0,0.0],[0.0,0.0,2.0,-4.0,0.0,0.0,0.0,4.0,0.0,0.0],[0.0,0.0,0.0,2.0,-4.0,0.0,0.0,0.0,4.0,0.0],[0.0,0.0,0.0,0.0,6.0,0.0,0.0,0.0,0.0,-4.0],[0.0,0.0,0.0,0.0,0.0,-2.0,0.0,4.0,-4.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,-2.0,0.0,4.0,-4.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,-6.0,0.0,4.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-2.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,2.0]],"num_vars":10}},"solutions":[{"source_config":[0,1,1,0,0,1,0,0,1,0],"target_config":[0,1,1,0,0,1,0,0,1,0]}]},
+    {"source":{"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"couplings":[1,-1,1,-1,1,-1,1,-1,1,-1,1,-1,1,-1,1],"fields":[0,0,0,0,0,0,0,0,0,0],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"target":{"problem":"MaxCut","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,-1,1,-1,1,-1,1,-1,1,-1,1,-1,1,-1,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"solutions":[{"source_config":[0,1,1,0,0,1,0,0,1,0],"target_config":[0,1,1,0,0,1,0,0,1,0]}]},
+    {"source":{"problem":"TravelingSalesman","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[10,15,20,35,25,30],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[0,3,null],[1,2,null],[1,3,null],[2,3,null]],"node_holes":[],"nodes":[null,null,null,null]}}}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Eq","rhs":1.0,"terms":[[0,1.0],[1,1.0],[2,1.0],[3,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[4,1.0],[5,1.0],[6,1.0],[7,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[8,1.0],[9,1.0],[10,1.0],[11,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[12,1.0],[13,1.0],[14,1.0],[15,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[0,1.0],[4,1.0],[8,1.0],[12,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[1,1.0],[5,1.0],[9,1.0],[13,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[2,1.0],[6,1.0],[10,1.0],[14,1.0]]},{"cmp":"Eq","rhs":1.0,"terms":[[3,1.0],[7,1.0],[11,1.0],[15,1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[16,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[16,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[16,1.0],[0,-1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[17,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[17,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[17,1.0],[4,-1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[18,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[18,1.0],[6,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[18,1.0],[1,-1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[19,1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[19,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[19,1.0],[5,-1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[20,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[20,1.0],[7,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[20,1.0],[2,-1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[21,1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[21,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[21,1.0],[6,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[22,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[22,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[22,1.0],[3,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[23,1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[23,1.0],[0,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[23,1.0],[7,-1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[24,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[24,1.0],[9,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[24,1.0],[0,-1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[25,1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[25,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[25,1.0],[8,-1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[26,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[26,1.0],[10,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[26,1.0],[1,-1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[27,1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[27,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[27,1.0],[9,-1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[28,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[28,1.0],[11,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[28,1.0],[2,-1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[29,1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[29,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[29,1.0],[10,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[30,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[30,1.0],[8,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[30,1.0],[3,-1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[31,1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[31,1.0],[0,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[31,1.0],[11,-1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[32,1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[32,1.0],[13,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[32,1.0],[0,-1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[33,1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[33,1.0],[1,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[33,1.0],[12,-1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[34,1.0],[1,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[34,1.0],[14,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[34,1.0],[1,-1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[35,1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[35,1.0],[2,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[35,1.0],[13,-1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[36,1.0],[2,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[36,1.0],[15,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[36,1.0],[2,-1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[37,1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[37,1.0],[3,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[37,1.0],[14,-1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[38,1.0],[3,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[38,1.0],[12,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[38,1.0],[3,-1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[39,1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[39,1.0],[0,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[39,1.0],[15,-1.0],[0,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[40,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[40,1.0],[9,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[40,1.0],[4,-1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[41,1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[41,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[41,1.0],[8,-1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[42,1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[42,1.0],[10,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[42,1.0],[5,-1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[43,1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[43,1.0],[6,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[43,1.0],[9,-1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[44,1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[44,1.0],[11,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[44,1.0],[6,-1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[45,1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[45,1.0],[7,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[45,1.0],[10,-1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[46,1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[46,1.0],[8,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[46,1.0],[7,-1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[47,1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[47,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[47,1.0],[11,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[48,1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[48,1.0],[13,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[48,1.0],[4,-1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[49,1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[49,1.0],[5,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[49,1.0],[12,-1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[50,1.0],[5,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[50,1.0],[14,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[50,1.0],[5,-1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[51,1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[51,1.0],[6,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[51,1.0],[13,-1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[52,1.0],[6,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[52,1.0],[15,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[52,1.0],[6,-1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[53,1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[53,1.0],[7,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[53,1.0],[14,-1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[54,1.0],[7,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[54,1.0],[12,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[54,1.0],[7,-1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[55,1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[55,1.0],[4,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[55,1.0],[15,-1.0],[4,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[56,1.0],[8,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[56,1.0],[13,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[56,1.0],[8,-1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[57,1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[57,1.0],[9,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[57,1.0],[12,-1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[58,1.0],[9,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[58,1.0],[14,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[58,1.0],[9,-1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[59,1.0],[13,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[59,1.0],[10,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[59,1.0],[13,-1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[60,1.0],[10,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[60,1.0],[15,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[60,1.0],[10,-1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[61,1.0],[14,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[61,1.0],[11,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[61,1.0],[14,-1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[62,1.0],[11,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[62,1.0],[12,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[62,1.0],[11,-1.0],[12,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[63,1.0],[15,-1.0]]},{"cmp":"Le","rhs":0.0,"terms":[[63,1.0],[8,-1.0]]},{"cmp":"Ge","rhs":-1.0,"terms":[[63,1.0],[15,-1.0],[8,-1.0]]}],"num_vars":64,"objective":[[16,10.0],[17,10.0],[18,10.0],[19,10.0],[20,10.0],[21,10.0],[22,10.0],[23,10.0],[24,15.0],[25,15.0],[26,15.0],[27,15.0],[28,15.0],[29,15.0],[30,15.0],[31,15.0],[32,20.0],[33,20.0],[34,20.0],[35,20.0],[36,20.0],[37,20.0],[38,20.0],[39,20.0],[40,35.0],[41,35.0],[42,35.0],[43,35.0],[44,35.0],[45,35.0],[46,35.0],[47,35.0],[48,25.0],[49,25.0],[50,25.0],[51,25.0],[52,25.0],[53,25.0],[54,25.0],[55,25.0],[56,30.0],[57,30.0],[58,30.0],[59,30.0],[60,30.0],[61,30.0],[62,30.0],[63,30.0]],"sense":"Minimize"}},"solutions":[{"source_config":[1,1,0,0,1,1],"target_config":[0,1,0,0,1,0,0,0,0,0,1,0,0,0,0,1,0,1,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,1,0,0,0]}]},
+    {"source":{"problem":"TravelingSalesman","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,2,3],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,2,null],[1,2,null]],"node_holes":[],"nodes":[null,null,null]}}}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-14.0,14.0,14.0,14.0,1.0,1.0,14.0,2.0,2.0],[0.0,-14.0,14.0,1.0,14.0,1.0,2.0,14.0,2.0],[0.0,0.0,-14.0,1.0,1.0,14.0,2.0,2.0,14.0],[0.0,0.0,0.0,-14.0,14.0,14.0,14.0,3.0,3.0],[0.0,0.0,0.0,0.0,-14.0,14.0,3.0,14.0,3.0],[0.0,0.0,0.0,0.0,0.0,-14.0,3.0,3.0,14.0],[0.0,0.0,0.0,0.0,0.0,0.0,-14.0,14.0,14.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,-14.0,14.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,-14.0]],"num_vars":9}},"solutions":[{"source_config":[1,1,1],"target_config":[0,0,1,0,1,0,1,0,0]}]}
+  ]
+}
diff --git a/src/example_db/mod.rs b/src/example_db/mod.rs
index 94b0c7e80..756499d9b 100644
--- a/src/example_db/mod.rs
+++ b/src/example_db/mod.rs
@@ -1,15 +1,21 @@
 //! Canonical example database assembly.
 //!
-//! `rule_builders` and `model_builders` are the canonical in-memory sources for
-//! all example data. This module assembles, validates, and looks up structural
-//! records from those builders — no filesystem round-trip or legacy bridge.
+//! The example database has two layers:
+//!
+//! - **Fixtures** (`fixtures/examples.json`): pre-computed expected results
+//!   embedded at compile time as a wrapped JSON object. These are the "stored
+//!   expected results" used for fast export and lookups.
+//!
+//! - **Builders** (`model_builders`, `rule_builders`): code that constructs
+//!   problem instances and computes solutions via BruteForce/ILP. Used only
+//!   for regenerating fixtures and for verification tests.
+//!
+//! The public API (`build_*_db`, `find_*_example`) loads from fixtures.
+//! Use `compute_*_db` to regenerate from code (slow, test/CI only).
 
 use crate::error::{ProblemError, Result};
-use crate::export::{
-    examples_output_dir, ModelDb, ModelExample, ProblemRef, RuleDb, RuleExample, EXAMPLE_DB_VERSION,
-};
+use crate::export::{ExampleDb, ModelDb, ModelExample, ProblemRef, RuleDb, RuleExample};
 use std::collections::BTreeSet;
-use std::path::PathBuf;
 
 mod model_builders;
 mod rule_builders;
@@ -51,24 +57,56 @@ fn validate_model_uniqueness(models: &[ModelExample]) -> Result<()> {
     Ok(())
 }
 
+// ---- Fixture loading (fast, used by default) ----
+
+/// Load the full example database from the embedded fixture file.
+pub fn build_example_db() -> Result<ExampleDb> {
+    static EXAMPLES_JSON: &str = include_str!("fixtures/examples.json");
+    let db: ExampleDb = serde_json::from_str(EXAMPLES_JSON)
+        .map_err(|e| ProblemError::SerializationError(format!("invalid example fixture: {e}")))?;
+    validate_model_uniqueness(&db.models)?;
+    validate_rule_uniqueness(&db.rules)?;
+    Ok(db)
+}
+
+/// Load the model database from the embedded fixture file.
+pub fn build_model_db() -> Result<ModelDb> {
+    let db = build_example_db()?;
+    Ok(ModelDb { models: db.models })
+}
+
+/// Load the rule database from the embedded fixture file.
 pub fn build_rule_db() -> Result<RuleDb> {
-    let mut rules = rule_builders::build_rule_examples();
-    rules.sort_by_key(rule_key);
-    validate_rule_uniqueness(&rules)?;
-    Ok(RuleDb {
-        version: EXAMPLE_DB_VERSION,
-        rules,
+    let db = build_example_db()?;
+    Ok(RuleDb { rules: db.rules })
+}
+
+// ---- Computation from builders (slow, for regeneration and verification) ----
+
+/// Recompute the full example database from builder code.
+pub fn compute_example_db() -> Result<ExampleDb> {
+    let model_db = compute_model_db()?;
+    let rule_db = compute_rule_db()?;
+    Ok(ExampleDb {
+        models: model_db.models,
+        rules: rule_db.rules,
     })
 }
 
-pub fn build_model_db() -> Result<ModelDb> {
+/// Recompute the model database from builder code (runs BruteForce).
+pub fn compute_model_db() -> Result<ModelDb> {
     let mut models = model_builders::build_model_examples();
     models.sort_by_key(model_key);
     validate_model_uniqueness(&models)?;
-    Ok(ModelDb {
-        version: EXAMPLE_DB_VERSION,
-        models,
-    })
+    Ok(ModelDb { models })
+}
+
+/// Recompute the rule database from builder code (runs BruteForce/ILP).
+pub fn compute_rule_db() -> Result<RuleDb> {
+    let mut rules = rule_builders::build_rule_examples();
+    rules.sort_by_key(rule_key);
+    validate_rule_uniqueness(&rules)?;
+    Ok(RuleDb { rules })
 }
 
 pub fn find_rule_example(source: &ProblemRef, target: &ProblemRef) -> Result<RuleExample> {
@@ -96,11 +134,6 @@ pub fn find_model_example(problem: &ProblemRef) -> Result<ModelExample> {
             ))
         })
 }
-
-pub fn default_generated_dir() -> PathBuf {
-    examples_output_dir()
-}
-
 #[cfg(test)]
 #[path = "../unit_tests/example_db.rs"]
 mod tests;
diff --git a/src/example_db/rule_builders.rs b/src/example_db/rule_builders.rs
index 503835505..741f75835 100644
--- a/src/example_db/rule_builders.rs
+++ b/src/example_db/rule_builders.rs
@@ -9,11 +9,11 @@ pub fn build_rule_examples() -> Vec<RuleExample> {
 
 #[cfg(test)]
 mod tests {
-    use super::*;
-
     #[test]
     fn builds_all_canonical_rule_examples() {
-        let examples = build_rule_examples();
+        let examples = crate::example_db::compute_rule_db()
+            .expect("compute should succeed")
+            .rules;
 
         assert!(!examples.is_empty());
         assert!(examples
diff --git a/src/example_db/specs.rs b/src/example_db/specs.rs
index 8904abae4..6d058a7f3 100644
--- a/src/example_db/specs.rs
+++ b/src/example_db/specs.rs
@@ -3,16 +3,16 @@
 //! These types describe canonical model and rule examples with metadata
 //! that can be validated against the catalog and reduction registry.
 
-use crate::export::{
-    lookup_overhead, overhead_to_json, variant_to_map, ModelExample, ProblemSide, RuleExample,
-    SampleEval, SolutionPair,
-};
+use crate::export::{ModelExample, ProblemSide, RuleExample, SampleEval, SolutionPair};
 use crate::models::algebraic::{VariableDomain, ILP};
 use crate::prelude::{OptimizationProblem, Problem, ReduceTo, ReductionResult};
-use crate::rules::{PathCostFn, ReductionGraph};
+use crate::rules::{MinimizeSteps, ReductionGraph};
 use crate::solvers::{BruteForce, ILPSolver};
 use crate::types::ProblemSize;
 use serde::Serialize;
+use std::any::Any;
+#[cfg(feature = "ilp-solver")]
+use std::sync::OnceLock;
 
 /// Specification for a canonical model example.
 #[allow(dead_code)]
@@ -102,7 +102,6 @@ where
 pub fn assemble_rule_example<S, T>(
     source: &S,
     target: &T,
-    overhead: crate::rules::ReductionOverhead,
     solutions: Vec<SolutionPair>,
 ) -> RuleExample
 where
@@ -112,72 +111,41 @@ where
     RuleExample {
         source: ProblemSide::from_problem(source),
         target: ProblemSide::from_problem(target),
-        overhead: overhead_to_json(&overhead),
         solutions,
     }
 }
 
-pub fn direct_overhead<S, T>() -> crate::rules::ReductionOverhead
-where
-    S: Problem,
-    T: Problem,
-{
-    let source_variant = variant_to_map(S::variant());
-    let target_variant = variant_to_map(T::variant());
-    lookup_overhead(S::NAME, &source_variant, T::NAME, &target_variant).unwrap_or_else(|| {
-        panic!(
-            "missing exact direct overhead for {} {:?} -> {} {:?}",
-            S::NAME,
-            source_variant,
-            T::NAME,
-            target_variant
-        )
-    })
-}
-
 pub fn direct_best_example<S, T, Keep>(source: S, keep: Keep) -> RuleExample
 where
     S: Problem + Serialize + ReduceTo<T>,
-    T: OptimizationProblem + Serialize,
+    T: OptimizationProblem + Serialize + 'static,
     T::Metric: Serialize,
     Keep: Fn(&S, &[usize]) -> bool,
 {
     let reduction = ReduceTo::<T>::reduce_to(&source);
     let target = reduction.target_problem();
-    let solutions = BruteForce::new()
-        .find_all_best(target)
-        .into_iter()
-        .filter_map(|target_config| {
-            let source_config = reduction.extract_solution(&target_config);
-            keep(&source, &source_config).then_some(SolutionPair {
-                source_config,
-                target_config,
-            })
-        })
-        .collect();
-    assemble_rule_example(&source, target, direct_overhead::<S, T>(), solutions)
+    let solutions = choose_best_target_solution(target, |target_config| {
+        build_solution_pair(&source, &reduction, target_config, &keep)
+    })
+    .into_iter()
+    .collect();
+    assemble_rule_example(&source, target, solutions)
 }
 
 pub fn direct_satisfying_example<S, T, Keep>(source: S, keep: Keep) -> RuleExample
 where
     S: Problem + Serialize + ReduceTo<T>,
-    T: Problem<Metric = bool> + Serialize,
+    T: Problem<Metric = bool> + Serialize + 'static,
     Keep: Fn(&S, &[usize]) -> bool,
 {
     let reduction = ReduceTo::<T>::reduce_to(&source);
     let target = reduction.target_problem();
-    let solutions = BruteForce::new()
-        .find_all_satisfying(target)
-        .into_iter()
-        .filter_map(|target_config| {
-            let source_config = reduction.extract_solution(&target_config);
-            keep(&source, &source_config).then_some(SolutionPair {
-                source_config,
-                target_config,
-            })
-        })
-        .collect();
-    assemble_rule_example(&source, target, direct_overhead::<S, T>(), solutions)
+    let solutions = choose_satisfying_target_solution(target, |target_config| {
+        build_solution_pair(&source, &reduction, target_config, &keep)
+    })
+    .into_iter()
+    .collect();
+    assemble_rule_example(&source, target, solutions)
 }
 
 pub fn direct_ilp_example<S, V, Keep>(source: S, keep: Keep) -> RuleExample
@@ -189,123 +157,129 @@ where
 {
     let reduction = ReduceTo::<ILP<V>>::reduce_to(&source);
     let target = reduction.target_problem();
-    let target_config = ILPSolver::new()
-        .solve(target)
-        .expect("canonical ILP target example should solve");
-    let source_config = reduction.extract_solution(&target_config);
-    let solutions = if keep(&source, &source_config) {
-        vec![SolutionPair {
-            source_config,
-            target_config,
-        }]
-    } else {
-        Vec::new()
-    };
-    assemble_rule_example(&source, target, direct_overhead::<S, ILP<V>>(), solutions)
+    let solutions = choose_best_target_solution(target, |target_config| {
+        build_solution_pair(&source, &reduction, target_config, &keep)
+    })
+    .into_iter()
+    .collect();
+    assemble_rule_example(&source, target, solutions)
 }
 
-pub fn path_best_example<S, T, C, Keep>(
-    source: S,
-    input_size: ProblemSize,
-    cost: C,
-    keep: Keep,
-) -> RuleExample
+pub fn keep_bool_source<S>(source: &S, config: &[usize]) -> bool
 where
-    S: Problem + Serialize + 'static,
-    T: OptimizationProblem + Serialize + 'static,
-    T::Metric: Serialize,
-    C: PathCostFn,
+    S: Problem<Metric = bool>,
+{
+    source.evaluate(config)
+}
+
+fn choose_best_target_solution<T, Keep>(target: &T, keep: Keep) -> Option<SolutionPair>
+where
+    T: OptimizationProblem + 'static,
+    Keep: Fn(&[usize]) -> Option<SolutionPair>,
+{
+    choose_available_ilp_solution(target)
+        .as_deref()
+        .and_then(&keep)
+        .or_else(|| first_matching_solution(BruteForce::new().find_all_best(target), keep))
+}
+
+fn choose_satisfying_target_solution<T, Keep>(target: &T, keep: Keep) -> Option<SolutionPair>
+where
+    T: Problem<Metric = bool> + 'static,
+    Keep: Fn(&[usize]) -> Option<SolutionPair>,
+{
+    choose_available_ilp_solution(target)
+        .as_deref()
+        .and_then(&keep)
+        .or_else(|| first_matching_solution(BruteForce::new().find_all_satisfying(target), keep))
+}
+
+fn build_solution_pair<S, R, Keep>(
+    source: &S,
+    reduction: &R,
+    target_config: &[usize],
+    keep: &Keep,
+) -> Option<SolutionPair>
+where
+    S: Problem,
+    R: ReductionResult<Source = S>,
     Keep: Fn(&S, &[usize]) -> bool,
 {
-    let graph = ReductionGraph::new();
-    let source_variant = variant_to_map(S::variant());
-    let target_variant = variant_to_map(T::variant());
-    let path = graph
-        .find_cheapest_path(
-            S::NAME,
-            &source_variant,
-            T::NAME,
-            &target_variant,
-            &input_size,
-            &cost,
-        )
-        .expect("canonical path example should exist");
-    let chain = graph
-        .reduce_along_path(&path, &source as &dyn std::any::Any)
-        .expect("canonical path example should execute");
-    let target = chain.target_problem::<T>();
-    let solutions = BruteForce::new()
-        .find_all_best(target)
-        .into_iter()
-        .filter_map(|target_config| {
-            let source_config = chain.extract_solution(&target_config);
-            keep(&source, &source_config).then_some(SolutionPair {
-                source_config,
-                target_config,
-            })
-        })
-        .collect();
-    assemble_rule_example(
-        &source,
-        target,
-        graph.compose_path_overhead(&path),
-        solutions,
-    )
+    let source_config = reduction.extract_solution(target_config);
+    keep(source, &source_config).then_some(SolutionPair {
+        source_config,
+        target_config: target_config.to_vec(),
+    })
 }
 
-pub fn path_ilp_example<S, V, C, Keep>(
-    source: S,
-    input_size: ProblemSize,
-    cost: C,
+fn first_matching_solution<Keep>(
+    mut candidates: Vec<Vec<usize>>,
     keep: Keep,
-) -> RuleExample
+) -> Option<SolutionPair>
 where
-    S: Problem + Serialize + 'static,
-    ILP<V>: Serialize + 'static,
-    V: VariableDomain,
-    C: PathCostFn,
-    Keep: Fn(&S, &[usize]) -> bool,
+    Keep: Fn(&[usize]) -> Option<SolutionPair>,
 {
-    let graph = ReductionGraph::new();
-    let source_variant = variant_to_map(S::variant());
-    let target_variant = variant_to_map(ILP::<V>::variant());
-    let path = graph
-        .find_cheapest_path(
-            S::NAME,
-            &source_variant,
-            ILP::<V>::NAME,
-            &target_variant,
-            &input_size,
-            &cost,
-        )
-        .expect("canonical ILP path example should exist");
-    let chain = graph
-        .reduce_along_path(&path, &source as &dyn std::any::Any)
-        .expect("canonical ILP path example should execute");
-    let target = chain.target_problem::<ILP<V>>();
-    let target_config = ILPSolver::new()
-        .solve(target)
-        .expect("canonical ILP path target should solve");
-    let source_config = chain.extract_solution(&target_config);
-    let solutions = if keep(&source, &source_config) {
-        vec![SolutionPair {
-            source_config,
-            target_config,
-        }]
-    } else {
-        Vec::new()
-    };
-    assemble_rule_example(
-        &source,
-        target,
-        graph.compose_path_overhead(&path),
-        solutions,
-    )
+    candidates.sort();
+    candidates.iter().find_map(|candidate| keep(candidate))
 }
 
-pub fn keep_bool_source<S>(source: &S, config: &[usize]) -> bool
+#[cfg(feature = "ilp-solver")]
+fn choose_available_ilp_solution<T>(problem: &T) -> Option<Vec<usize>>
 where
-    S: Problem<Metric = bool>,
+    T: Problem + 'static,
 {
-    source.evaluate(config)
+    let problem_any = problem as &dyn Any;
+    if let Some(ilp) = problem_any.downcast_ref::<ILP<bool>>() {
+        return ILPSolver::new().solve(ilp);
+    }
+    if let Some(ilp) = problem_any.downcast_ref::<ILP<i32>>() {
+        return ILPSolver::new().solve(ilp);
+    }
+
+    let graph = ilp_reduction_graph();
+    let source_variant = ReductionGraph::variant_to_map(&T::variant());
+    let input_size = ProblemSize::new(vec![]);
+
+    let bool_variant = ReductionGraph::variant_to_map(&ILP::<bool>::variant());
+    if let Some(path) = graph.find_cheapest_path(
+        T::NAME,
+        &source_variant,
+        "ILP",
+        &bool_variant,
+        &input_size,
+        &MinimizeSteps,
+    ) {
+        let chain = graph.reduce_along_path(&path, problem as &dyn Any)?;
+        let ilp = chain.target_problem::<ILP<bool>>();
+        let ilp_solution = ILPSolver::new().solve(ilp)?;
+        return Some(chain.extract_solution(&ilp_solution));
+    }
+
+    let i32_variant = ReductionGraph::variant_to_map(&ILP::<i32>::variant());
+    let path = graph.find_cheapest_path(
+        T::NAME,
+        &source_variant,
+        "ILP",
+        &i32_variant,
+        &input_size,
+        &MinimizeSteps,
+    )?;
+    let chain = graph.reduce_along_path(&path, problem as &dyn Any)?;
+    let ilp = chain.target_problem::<ILP<i32>>();
+    let ilp_solution = ILPSolver::new().solve(ilp)?;
+    Some(chain.extract_solution(&ilp_solution))
+}
+
+#[cfg(feature = "ilp-solver")]
+fn ilp_reduction_graph() -> &'static ReductionGraph {
+    static GRAPH: OnceLock<ReductionGraph> = OnceLock::new();
+    GRAPH.get_or_init(ReductionGraph::new)
+}
+
+#[cfg(not(feature = "ilp-solver"))]
+fn choose_available_ilp_solution<T>(_problem: &T) -> Option<Vec<usize>>
+where
+    T: Problem + 'static,
+{
+    None
 }
diff --git a/src/export.rs b/src/export.rs
index 0f71b7fa0..a308ce075 100644
--- a/src/export.rs
+++ b/src/export.rs
@@ -1,16 +1,12 @@
 //! JSON export schema for example payloads.
 
-use crate::expr::Expr;
 use crate::rules::registry::ReductionOverhead;
 use crate::rules::ReductionGraph;
 use crate::traits::Problem;
 use serde::{Deserialize, Serialize};
 use std::collections::BTreeMap;
-use std::env;
 use std::fs;
-use std::path::{Path, PathBuf};
-
-pub const EXAMPLES_DIR_ENV: &str = "PROBLEMREDUCTIONS_EXAMPLES_DIR";
+use std::path::Path;
 
 /// One side (source or target) of a reduction.
 #[derive(Serialize, Deserialize, Clone, Debug, PartialEq)]
@@ -52,19 +48,6 @@ pub struct ProblemRef {
     pub variant: BTreeMap<String, String>,
 }
 
-/// One output field mapped to an expression.
-#[derive(Serialize, Deserialize, Clone, Debug, PartialEq)]
-pub struct OverheadEntry {
-    pub field: String,
-    #[serde(skip_deserializing, default = "default_expr")]
-    pub expr: Expr,
-    pub formula: String,
-}
-
-fn default_expr() -> Expr {
-    Expr::Const(0.0)
-}
-
 /// One source↔target solution pair.
 #[derive(Serialize, Deserialize, Clone, Debug, PartialEq)]
 pub struct SolutionPair {
@@ -77,7 +60,6 @@ pub struct SolutionPair {
 pub struct RuleExample {
     pub source: ProblemSide,
     pub target: ProblemSide,
-    pub overhead: Vec<OverheadEntry>,
     pub solutions: Vec<SolutionPair>,
 }
 
@@ -118,18 +100,21 @@ impl ModelExample {
 /// Canonical exported database of rule examples.
 #[derive(Serialize, Deserialize, Clone, Debug, PartialEq)]
 pub struct RuleDb {
-    pub version: u32,
     pub rules: Vec<RuleExample>,
 }
 
 /// Canonical exported database of model examples.
 #[derive(Serialize, Deserialize, Clone, Debug, PartialEq)]
 pub struct ModelDb {
-    pub version: u32,
     pub models: Vec<ModelExample>,
 }
 
-pub const EXAMPLE_DB_VERSION: u32 = 1;
+/// Canonical exported database of model and rule examples.
+#[derive(Serialize, Deserialize, Clone, Debug, PartialEq)]
+pub struct ExampleDb {
+    pub models: Vec<ModelExample>,
+    pub rules: Vec<RuleExample>,
+}
 
 #[derive(Serialize, Deserialize, Clone, Debug, PartialEq)]
 pub struct SampleEval {
@@ -137,19 +122,6 @@ pub struct SampleEval {
     pub metric: serde_json::Value,
 }
 
-/// Convert a `ReductionOverhead` to JSON-serializable entries.
-pub fn overhead_to_json(overhead: &ReductionOverhead) -> Vec<OverheadEntry> {
-    overhead
-        .output_size
-        .iter()
-        .map(|(field, expr)| OverheadEntry {
-            field: field.to_string(),
-            formula: expr.to_string(),
-            expr: expr.clone(),
-        })
-        .collect()
-}
-
 /// Look up `ReductionOverhead` for a direct reduction using `ReductionGraph::find_best_entry`.
 pub fn lookup_overhead(
     source_name: &str,
@@ -181,19 +153,40 @@ pub fn variant_to_map(variant: Vec<(&str, &str)>) -> BTreeMap<String, String> {
         .collect()
 }
 
-/// Default output directory for generated example JSON.
-pub fn examples_output_dir() -> PathBuf {
-    if let Some(dir) = env::var_os(EXAMPLES_DIR_ENV) {
-        PathBuf::from(dir)
+fn write_json_file<T: Serialize>(dir: &Path, name: &str, payload: &T) {
+    fs::create_dir_all(dir).expect("Failed to create examples directory");
+    let path = dir.join(format!("{name}.json"));
+    let json = serde_json::to_string_pretty(payload).expect("Failed to serialize example");
+    fs::write(&path, json).expect("Failed to write example JSON");
+    println!("Exported: {}", path.display());
+}
+
+fn render_compact_array<T: Serialize>(items: &[T]) -> String {
+    if items.is_empty() {
+        "[]".to_string()
     } else {
-        PathBuf::from("docs/paper/examples/generated")
+        let rows = items
+            .iter()
+            .map(|item| {
+                format!(
+                    "    {}",
+                    serde_json::to_string(item).expect("Failed to serialize example entry")
+                )
+            })
+            .collect::<Vec<_>>()
+            .join(",\n");
+        format!("[\n{rows}\n  ]")
     }
 }
 
-fn write_json_file<T: Serialize>(dir: &Path, name: &str, payload: &T) {
+fn write_example_db_file(dir: &Path, db: &ExampleDb) {
     fs::create_dir_all(dir).expect("Failed to create examples directory");
-    let path = dir.join(format!("{name}.json"));
-    let json = serde_json::to_string_pretty(payload).expect("Failed to serialize example");
+    let path = dir.join("examples.json");
+    let json = format!(
+        "{{\n  \"models\": {},\n  \"rules\": {}\n}}\n",
+        render_compact_array(&db.models),
+        render_compact_array(&db.rules)
+    );
     fs::write(&path, json).expect("Failed to write example JSON");
     println!("Exported: {}", path.display());
 }
@@ -203,31 +196,26 @@ pub fn write_rule_example_to(dir: &Path, name: &str, example: &RuleExample) {
     write_json_file(dir, name, example);
 }
 
-/// Write a merged rule example JSON file to the configured output directory.
-pub fn write_rule_example(name: &str, example: &RuleExample) {
-    write_rule_example_to(&examples_output_dir(), name, example);
-}
-
 /// Write a model example JSON file to a target directory.
 pub fn write_model_example_to(dir: &Path, name: &str, example: &ModelExample) {
     write_json_file(dir, name, example);
 }
 
-/// Write a model example JSON file to the configured output directory.
-pub fn write_model_example(name: &str, example: &ModelExample) {
-    write_model_example_to(&examples_output_dir(), name, example);
-}
-
-/// Write the canonical rule database to `rules.json`.
+/// Write the canonical rule database as a wrapped JSON object.
 pub fn write_rule_db_to(dir: &Path, db: &RuleDb) {
     write_json_file(dir, "rules", db);
 }
 
-/// Write the canonical model database to `models.json`.
+/// Write the canonical model database as a wrapped JSON object.
 pub fn write_model_db_to(dir: &Path, db: &ModelDb) {
     write_json_file(dir, "models", db);
 }
 
+/// Write the canonical example database as a wrapped JSON object.
+pub fn write_example_db_to(dir: &Path, db: &ExampleDb) {
+    write_example_db_file(dir, db);
+}
+
 #[cfg(test)]
 #[path = "unit_tests/export.rs"]
 mod tests;
diff --git a/src/models/misc/minimum_tardiness_sequencing.rs b/src/models/misc/minimum_tardiness_sequencing.rs
index ed383c816..d33c17423 100644
--- a/src/models/misc/minimum_tardiness_sequencing.rs
+++ b/src/models/misc/minimum_tardiness_sequencing.rs
@@ -197,11 +197,7 @@ pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::M
         build: || {
             // 4 tasks with precedence 0 -> 2 (task 0 before task 2).
             // Deadlines: task 0 by time 2, task 1 by time 3, task 2 by time 1, task 3 by time 4.
-            let problem = MinimumTardinessSequencing::new(
-                4,
-                vec![2, 3, 1, 4],
-                vec![(0, 2)],
-            );
+            let problem = MinimumTardinessSequencing::new(4, vec![2, 3, 1, 4], vec![(0, 2)]);
             // Sample config: Lehmer code [0,0,0,0] = identity permutation (schedule order 0,1,2,3)
             crate::example_db::specs::optimization_example(problem, vec![vec![0, 0, 0, 0]])
         },
diff --git a/src/rules/circuit_spinglass.rs b/src/rules/circuit_spinglass.rs
index a22a422c8..16af9375c 100644
--- a/src/rules/circuit_spinglass.rs
+++ b/src/rules/circuit_spinglass.rs
@@ -279,7 +279,8 @@ where
 
     /// Build the final SpinGlass.
     fn build(self) -> (SpinGlass<SimpleGraph, W>, HashMap<String, usize>) {
-        let interactions: Vec<((usize, usize), W)> = self.interactions.into_iter().collect();
+        let mut interactions: Vec<((usize, usize), W)> = self.interactions.into_iter().collect();
+        interactions.sort_by_key(|((u, v), _)| (*u, *v));
         let sg = SpinGlass::new(self.num_spins, interactions, self.fields);
         (sg, self.variable_map)
     }
diff --git a/src/rules/factoring_circuit.rs b/src/rules/factoring_circuit.rs
index 4508dea4a..e4733a4e9 100644
--- a/src/rules/factoring_circuit.rs
+++ b/src/rules/factoring_circuit.rs
@@ -294,10 +294,11 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
             let source = Factoring::new(3, 3, 35);
             let reduction = ReduceTo::<CircuitSAT>::reduce_to(&source);
             let target = reduction.target_problem();
-            let source_solutions = BruteForce::new().find_all_best(&source);
             let var_names = target.variable_names();
-            let solutions = source_solutions
+            let solutions = BruteForce::new()
+                .find_all_best(&source)
                 .into_iter()
+                .min()
                 .map(|source_config| {
                     let mut inputs: HashMap<String, bool> = HashMap::new();
                     for (i, &bit) in source_config.iter().enumerate().take(source.m()) {
@@ -315,18 +316,13 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                         .iter()
                         .map(|name| usize::from(*values.get(name).unwrap_or(&false)))
                         .collect();
-                    SolutionPair {
+                    vec![SolutionPair {
                         source_config,
                         target_config,
-                    }
+                    }]
                 })
-                .collect();
-            crate::example_db::specs::assemble_rule_example(
-                &source,
-                target,
-                crate::example_db::specs::direct_overhead::<Factoring, CircuitSAT>(),
-                solutions,
-            )
+                .unwrap_or_default();
+            crate::example_db::specs::assemble_rule_example(&source, target, solutions)
         },
     }]
 }
diff --git a/src/rules/ksatisfiability_qubo.rs b/src/rules/ksatisfiability_qubo.rs
index 565ce8673..e7cb2c975 100644
--- a/src/rules/ksatisfiability_qubo.rs
+++ b/src/rules/ksatisfiability_qubo.rs
@@ -329,27 +329,47 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     use crate::models::algebraic::QUBO;
     use crate::models::formula::CNFClause;
 
-    vec![crate::example_db::specs::RuleExampleSpec {
-        id: "ksatisfiability_to_qubo",
-        build: || {
-            let source = KSatisfiability::<K3>::new(
-                5,
-                vec![
-                    CNFClause::new(vec![1, 2, -3]),
-                    CNFClause::new(vec![-1, 3, 4]),
-                    CNFClause::new(vec![2, -4, 5]),
-                    CNFClause::new(vec![-2, 3, -5]),
-                    CNFClause::new(vec![1, -3, 5]),
-                    CNFClause::new(vec![-1, -2, 4]),
-                    CNFClause::new(vec![3, -4, -5]),
-                ],
-            );
-            crate::example_db::specs::direct_best_example::<_, QUBO<f64>, _>(
-                source,
-                crate::example_db::specs::keep_bool_source,
-            )
+    vec![
+        crate::example_db::specs::RuleExampleSpec {
+            id: "ksatisfiability_k2_to_qubo",
+            build: || {
+                let source = KSatisfiability::<K2>::new(
+                    4,
+                    vec![
+                        CNFClause::new(vec![1, 2]),
+                        CNFClause::new(vec![-1, 3]),
+                        CNFClause::new(vec![-2, 4]),
+                        CNFClause::new(vec![-3, -4]),
+                    ],
+                );
+                crate::example_db::specs::direct_best_example::<_, QUBO<f64>, _>(
+                    source,
+                    crate::example_db::specs::keep_bool_source,
+                )
+            },
         },
-    }]
+        crate::example_db::specs::RuleExampleSpec {
+            id: "ksatisfiability_to_qubo",
+            build: || {
+                let source = KSatisfiability::<K3>::new(
+                    5,
+                    vec![
+                        CNFClause::new(vec![1, 2, -3]),
+                        CNFClause::new(vec![-1, 3, 4]),
+                        CNFClause::new(vec![2, -4, 5]),
+                        CNFClause::new(vec![-2, 3, -5]),
+                        CNFClause::new(vec![1, -3, 5]),
+                        CNFClause::new(vec![-1, -2, 4]),
+                        CNFClause::new(vec![3, -4, -5]),
+                    ],
+                );
+                crate::example_db::specs::direct_best_example::<_, QUBO<f64>, _>(
+                    source,
+                    crate::example_db::specs::keep_bool_source,
+                )
+            },
+        },
+    ]
 }
 
 #[cfg(test)]
diff --git a/src/rules/maximumindependentset_maximumclique.rs b/src/rules/maximumindependentset_maximumclique.rs
index 1523ba7df..3cd897116 100644
--- a/src/rules/maximumindependentset_maximumclique.rs
+++ b/src/rules/maximumindependentset_maximumclique.rs
@@ -63,52 +63,19 @@ impl ReduceTo<MaximumClique<SimpleGraph, i32>> for MaximumIndependentSet<SimpleG
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::models::algebraic::QUBO;
-    use crate::rules::{Minimize, MinimizeSteps};
-    use crate::types::ProblemSize;
-
-    fn mis_petersen() -> MaximumIndependentSet<SimpleGraph, i32> {
-        let (n, edges) = crate::topology::small_graphs::petersen();
-        MaximumIndependentSet::new(SimpleGraph::new(n, edges), vec![1i32; 10])
-    }
-
-    vec![
-        crate::example_db::specs::RuleExampleSpec {
-            id: "maximumindependentset_to_maximumclique",
-            build: || {
-                let source = MaximumIndependentSet::new(
-                    SimpleGraph::new(5, vec![(0, 1), (1, 2), (2, 3), (3, 4)]),
-                    vec![1i32; 5],
-                );
-                crate::example_db::specs::direct_best_example::<_, MaximumClique<SimpleGraph, i32>, _>(
-                    source,
-                    |_, _| true,
-                )
-            },
-        },
-        crate::example_db::specs::RuleExampleSpec {
-            id: "maximumindependentset_to_ilp",
-            build: || {
-                crate::example_db::specs::path_ilp_example::<_, bool, _, _>(
-                    mis_petersen(),
-                    ProblemSize::new(vec![]),
-                    MinimizeSteps,
-                    |_, _| true,
-                )
-            },
-        },
-        crate::example_db::specs::RuleExampleSpec {
-            id: "maximumindependentset_to_qubo",
-            build: || {
-                crate::example_db::specs::path_best_example::<_, QUBO<f64>, _, _>(
-                    mis_petersen(),
-                    ProblemSize::new(vec![("num_vertices", 10), ("num_edges", 15)]),
-                    Minimize("num_vars"),
-                    |_, _| true,
-                )
-            },
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "maximumindependentset_to_maximumclique",
+        build: || {
+            let source = MaximumIndependentSet::new(
+                SimpleGraph::new(5, vec![(0, 1), (1, 2), (2, 3), (3, 4)]),
+                vec![1i32; 5],
+            );
+            crate::example_db::specs::direct_best_example::<_, MaximumClique<SimpleGraph, i32>, _>(
+                source,
+                |_, _| true,
+            )
         },
-    ]
+    }]
 }
 
 #[cfg(test)]
diff --git a/src/rules/maximumindependentset_maximumsetpacking.rs b/src/rules/maximumindependentset_maximumsetpacking.rs
index 19069f475..9ca2bb90a 100644
--- a/src/rules/maximumindependentset_maximumsetpacking.rs
+++ b/src/rules/maximumindependentset_maximumsetpacking.rs
@@ -135,6 +135,17 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 )
             },
         },
+        crate::example_db::specs::RuleExampleSpec {
+            id: "maximumindependentset_one_to_maximumsetpacking_one",
+            build: || {
+                let (n, edges) = crate::topology::small_graphs::petersen();
+                let source = MaximumIndependentSet::new(SimpleGraph::new(n, edges), vec![One; 10]);
+                crate::example_db::specs::direct_best_example::<_, MaximumSetPacking<One>, _>(
+                    source,
+                    |_, _| true,
+                )
+            },
+        },
         crate::example_db::specs::RuleExampleSpec {
             id: "maximumsetpacking_to_maximumindependentset",
             build: || {
@@ -153,6 +164,24 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 >(source, |_, _| true)
             },
         },
+        crate::example_db::specs::RuleExampleSpec {
+            id: "maximumsetpacking_one_to_maximumindependentset_one",
+            build: || {
+                let sets = vec![
+                    vec![0, 1, 2],
+                    vec![2, 3],
+                    vec![4, 5, 6],
+                    vec![1, 5, 7],
+                    vec![3, 6],
+                ];
+                let source = MaximumSetPacking::with_weights(sets, vec![One; 5]);
+                crate::example_db::specs::direct_best_example::<
+                    _,
+                    MaximumIndependentSet<SimpleGraph, One>,
+                    _,
+                >(source, |_, _| true)
+            },
+        },
     ]
 }
 
diff --git a/src/rules/maximummatching_ilp.rs b/src/rules/maximummatching_ilp.rs
index 68ca17fb9..54211b499 100644
--- a/src/rules/maximummatching_ilp.rs
+++ b/src/rules/maximummatching_ilp.rs
@@ -55,11 +55,11 @@ impl ReduceTo<ILP<bool>> for MaximumMatching<SimpleGraph, i32> {
         // Constraints: For each vertex v, sum of incident edge variables <= 1
         // This ensures at most one incident edge is selected per vertex
         let v2e = self.vertex_to_edges();
-        let constraints: Vec<LinearConstraint> = v2e
-            .into_iter()
-            .filter(|(_, edges)| !edges.is_empty())
-            .map(|(_, edges)| {
-                let terms: Vec<(usize, f64)> = edges.into_iter().map(|e| (e, 1.0)).collect();
+        let constraints: Vec<LinearConstraint> = (0..self.graph().num_vertices())
+            .filter_map(|vertex| v2e.get(&vertex))
+            .filter(|edges| !edges.is_empty())
+            .map(|edges| {
+                let terms: Vec<(usize, f64)> = edges.iter().map(|&e| (e, 1.0)).collect();
                 LinearConstraint::le(terms, 1.0)
             })
             .collect();
diff --git a/src/rules/minimumvertexcover_maximumindependentset.rs b/src/rules/minimumvertexcover_maximumindependentset.rs
index 74d189114..f238e3984 100644
--- a/src/rules/minimumvertexcover_maximumindependentset.rs
+++ b/src/rules/minimumvertexcover_maximumindependentset.rs
@@ -93,10 +93,6 @@ impl ReduceTo<MaximumIndependentSet<SimpleGraph, i32>> for MinimumVertexCover<Si
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
-    use crate::models::algebraic::QUBO;
-    use crate::rules::{Minimize, MinimizeSteps};
-    use crate::types::ProblemSize;
-
     fn vc_petersen() -> MinimumVertexCover<SimpleGraph, i32> {
         let (n, edges) = crate::topology::small_graphs::petersen();
         MinimumVertexCover::new(SimpleGraph::new(n, edges), vec![1i32; 10])
@@ -128,28 +124,6 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 >(vc_petersen(), |_, _| true)
             },
         },
-        crate::example_db::specs::RuleExampleSpec {
-            id: "minimumvertexcover_to_ilp",
-            build: || {
-                crate::example_db::specs::path_ilp_example::<_, bool, _, _>(
-                    vc_petersen(),
-                    ProblemSize::new(vec![]),
-                    MinimizeSteps,
-                    |_, _| true,
-                )
-            },
-        },
-        crate::example_db::specs::RuleExampleSpec {
-            id: "minimumvertexcover_to_qubo",
-            build: || {
-                crate::example_db::specs::path_best_example::<_, QUBO<f64>, _, _>(
-                    vc_petersen(),
-                    ProblemSize::new(vec![("num_vertices", 10), ("num_edges", 15)]),
-                    Minimize("num_vars"),
-                    |_, _| true,
-                )
-            },
-        },
     ]
 }
 
diff --git a/src/rules/mod.rs b/src/rules/mod.rs
index b5e3c9326..6fc0ae7a0 100644
--- a/src/rules/mod.rs
+++ b/src/rules/mod.rs
@@ -34,6 +34,8 @@ pub(crate) mod sat_minimumdominatingset;
 mod spinglass_casts;
 pub(crate) mod spinglass_maxcut;
 pub(crate) mod spinglass_qubo;
+#[cfg(test)]
+pub(crate) mod test_helpers;
 mod traits;
 pub(crate) mod travelingsalesman_qubo;
 
diff --git a/src/rules/test_helpers.rs b/src/rules/test_helpers.rs
new file mode 100644
index 000000000..a03655075
--- /dev/null
+++ b/src/rules/test_helpers.rs
@@ -0,0 +1,380 @@
+use crate::rules::{ReductionChain, ReductionResult};
+use crate::solvers::{BruteForce, Solver};
+use crate::traits::{OptimizationProblem, Problem, SatisfactionProblem};
+use std::collections::HashSet;
+
+fn verify_optimization_round_trip<Source, Extract>(
+    source: &Source,
+    target_solutions: Vec<Vec<usize>>,
+    extract_solution: Extract,
+    target_solution_kind: &str,
+    context: &str,
+) where
+    Source: OptimizationProblem + 'static,
+    <Source as OptimizationProblem>::Value: std::fmt::Debug + PartialEq,
+    <Source as Problem>::Metric: std::fmt::Debug + PartialEq,
+    Extract: Fn(&[usize]) -> Vec<usize>,
+{
+    assert!(
+        !target_solutions.is_empty(),
+        "{context}: target solver found no {target_solution_kind} solutions"
+    );
+
+    let solver = BruteForce::new();
+    let reference_solutions: HashSet<Vec<usize>> =
+        solver.find_all_best(source).into_iter().collect();
+    assert!(
+        !reference_solutions.is_empty(),
+        "{context}: direct source solver found no optimal solutions"
+    );
+
+    let reference_metric = source.evaluate(
+        reference_solutions
+            .iter()
+            .next()
+            .expect("reference set is non-empty"),
+    );
+    let extracted: HashSet<Vec<usize>> = target_solutions
+        .iter()
+        .map(|target_solution| extract_solution(target_solution))
+        .collect();
+    assert!(
+        !extracted.is_empty(),
+        "{context}: no extracted source solutions"
+    );
+    assert!(
+        extracted.is_subset(&reference_solutions),
+        "{context}: extracted source solutions are not all directly optimal"
+    );
+    for source_solution in &extracted {
+        let extracted_metric = source.evaluate(source_solution);
+        assert!(
+            extracted_metric.is_valid(),
+            "{context}: extracted source solution is infeasible: {:?}",
+            source_solution
+        );
+        assert_eq!(
+            extracted_metric, reference_metric,
+            "{context}: extracted source objective does not match direct solve"
+        );
+    }
+}
+
+fn verify_satisfaction_round_trip<Source, Extract>(
+    source: &Source,
+    target_solutions: Vec<Vec<usize>>,
+    extract_solution: Extract,
+    target_solution_kind: &str,
+    context: &str,
+) where
+    Source: SatisfactionProblem + 'static,
+    Extract: Fn(&[usize]) -> Vec<usize>,
+{
+    assert!(
+        !target_solutions.is_empty(),
+        "{context}: target solver found no {target_solution_kind} solutions"
+    );
+    let extracted: HashSet<Vec<usize>> = target_solutions
+        .iter()
+        .map(|target_solution| extract_solution(target_solution))
+        .collect();
+    assert!(
+        !extracted.is_empty(),
+        "{context}: no extracted source solutions"
+    );
+    for source_solution in &extracted {
+        assert!(
+            source.evaluate(source_solution),
+            "{context}: extracted source solution is not satisfying: {:?}",
+            source_solution
+        );
+    }
+}
+
+pub(crate) fn assert_optimization_round_trip_from_optimization_target<R>(
+    source: &R::Source,
+    reduction: &R,
+    context: &str,
+) where
+    R: ReductionResult,
+    R::Source: OptimizationProblem + 'static,
+    R::Target: OptimizationProblem + 'static,
+    <R::Source as OptimizationProblem>::Value: std::fmt::Debug + PartialEq,
+    <R::Source as Problem>::Metric: std::fmt::Debug + PartialEq,
+{
+    let target_solutions = BruteForce::new().find_all_best(reduction.target_problem());
+    verify_optimization_round_trip(
+        source,
+        target_solutions,
+        |target_solution| reduction.extract_solution(target_solution),
+        "optimal",
+        context,
+    );
+}
+
+pub(crate) fn assert_optimization_round_trip_from_satisfaction_target<R>(
+    source: &R::Source,
+    reduction: &R,
+    context: &str,
+) where
+    R: ReductionResult,
+    R::Source: OptimizationProblem + 'static,
+    R::Target: SatisfactionProblem + 'static,
+    <R::Source as OptimizationProblem>::Value: std::fmt::Debug + PartialEq,
+    <R::Source as Problem>::Metric: std::fmt::Debug + PartialEq,
+{
+    let target_solutions = BruteForce::new().find_all_satisfying(reduction.target_problem());
+    verify_optimization_round_trip(
+        source,
+        target_solutions,
+        |target_solution| reduction.extract_solution(target_solution),
+        "satisfying",
+        context,
+    );
+}
+
+pub(crate) fn assert_optimization_round_trip_chain<Source, Target>(
+    source: &Source,
+    chain: &ReductionChain,
+    context: &str,
+) where
+    Source: OptimizationProblem + 'static,
+    Target: OptimizationProblem + 'static,
+    <Source as OptimizationProblem>::Value: std::fmt::Debug + PartialEq,
+    <Source as Problem>::Metric: std::fmt::Debug + PartialEq,
+{
+    let target_solutions = BruteForce::new().find_all_best(chain.target_problem::<Target>());
+    verify_optimization_round_trip(
+        source,
+        target_solutions,
+        |target_solution| chain.extract_solution(target_solution),
+        "optimal",
+        context,
+    );
+}
+
+pub(crate) fn assert_satisfaction_round_trip_from_optimization_target<R>(
+    source: &R::Source,
+    reduction: &R,
+    context: &str,
+) where
+    R: ReductionResult,
+    R::Source: SatisfactionProblem + 'static,
+    R::Target: OptimizationProblem + 'static,
+{
+    let target_solutions = BruteForce::new().find_all_best(reduction.target_problem());
+    verify_satisfaction_round_trip(
+        source,
+        target_solutions,
+        |target_solution| reduction.extract_solution(target_solution),
+        "optimal",
+        context,
+    );
+}
+
+pub(crate) fn assert_satisfaction_round_trip_from_satisfaction_target<R>(
+    source: &R::Source,
+    reduction: &R,
+    context: &str,
+) where
+    R: ReductionResult,
+    R::Source: SatisfactionProblem + 'static,
+    R::Target: SatisfactionProblem + 'static,
+{
+    let target_solutions = BruteForce::new().find_all_satisfying(reduction.target_problem());
+    verify_satisfaction_round_trip(
+        source,
+        target_solutions,
+        |target_solution| reduction.extract_solution(target_solution),
+        "satisfying",
+        context,
+    );
+}
+
+pub(crate) fn solve_optimization_problem<P>(problem: &P) -> Option<Vec<usize>>
+where
+    P: OptimizationProblem + 'static,
+{
+    BruteForce::new().find_best(problem)
+}
+
+pub(crate) fn solve_satisfaction_problem<P>(problem: &P) -> Option<Vec<usize>>
+where
+    P: SatisfactionProblem + 'static,
+{
+    BruteForce::new().find_satisfying(problem)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::{
+        assert_optimization_round_trip_from_optimization_target,
+        assert_optimization_round_trip_from_satisfaction_target,
+        assert_satisfaction_round_trip_from_optimization_target,
+        assert_satisfaction_round_trip_from_satisfaction_target,
+    };
+    use crate::rules::ReductionResult;
+    use crate::traits::{OptimizationProblem, Problem, SatisfactionProblem};
+    use crate::types::{Direction, SolutionSize};
+
+    #[derive(Clone)]
+    struct ToyOptimizationProblem;
+
+    impl Problem for ToyOptimizationProblem {
+        const NAME: &'static str = "ToyOptimizationProblem";
+        type Metric = SolutionSize<i32>;
+
+        fn dims(&self) -> Vec<usize> {
+            vec![2, 2]
+        }
+
+        fn evaluate(&self, config: &[usize]) -> Self::Metric {
+            match config {
+                [1, 0] | [0, 1] => SolutionSize::Valid(1),
+                _ => SolutionSize::Invalid,
+            }
+        }
+
+        fn variant() -> Vec<(&'static str, &'static str)> {
+            vec![]
+        }
+    }
+
+    impl OptimizationProblem for ToyOptimizationProblem {
+        type Value = i32;
+
+        fn direction(&self) -> Direction {
+            Direction::Maximize
+        }
+    }
+
+    #[derive(Clone)]
+    struct ToySatisfactionProblem;
+
+    impl Problem for ToySatisfactionProblem {
+        const NAME: &'static str = "ToySatisfactionProblem";
+        type Metric = bool;
+
+        fn dims(&self) -> Vec<usize> {
+            vec![2, 2]
+        }
+
+        fn evaluate(&self, config: &[usize]) -> Self::Metric {
+            matches!(config, [1, 0] | [0, 1])
+        }
+
+        fn variant() -> Vec<(&'static str, &'static str)> {
+            vec![]
+        }
+    }
+
+    impl SatisfactionProblem for ToySatisfactionProblem {}
+
+    struct OptToOptReduction {
+        target: ToyOptimizationProblem,
+    }
+
+    impl ReductionResult for OptToOptReduction {
+        type Source = ToyOptimizationProblem;
+        type Target = ToyOptimizationProblem;
+
+        fn target_problem(&self) -> &Self::Target {
+            &self.target
+        }
+
+        fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
+            target_solution.to_vec()
+        }
+    }
+
+    struct OptToSatReduction {
+        target: ToySatisfactionProblem,
+    }
+
+    impl ReductionResult for OptToSatReduction {
+        type Source = ToyOptimizationProblem;
+        type Target = ToySatisfactionProblem;
+
+        fn target_problem(&self) -> &Self::Target {
+            &self.target
+        }
+
+        fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
+            target_solution.to_vec()
+        }
+    }
+
+    struct SatToOptReduction {
+        target: ToyOptimizationProblem,
+    }
+
+    impl ReductionResult for SatToOptReduction {
+        type Source = ToySatisfactionProblem;
+        type Target = ToyOptimizationProblem;
+
+        fn target_problem(&self) -> &Self::Target {
+            &self.target
+        }
+
+        fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
+            target_solution.to_vec()
+        }
+    }
+
+    struct SatToSatReduction {
+        target: ToySatisfactionProblem,
+    }
+
+    impl ReductionResult for SatToSatReduction {
+        type Source = ToySatisfactionProblem;
+        type Target = ToySatisfactionProblem;
+
+        fn target_problem(&self) -> &Self::Target {
+            &self.target
+        }
+
+        fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
+            target_solution.to_vec()
+        }
+    }
+
+    #[test]
+    fn test_optimization_round_trip_wrappers_accept_identity_reductions() {
+        let source = ToyOptimizationProblem;
+
+        assert_optimization_round_trip_from_optimization_target(
+            &source,
+            &OptToOptReduction {
+                target: ToyOptimizationProblem,
+            },
+            "opt->opt",
+        );
+        assert_optimization_round_trip_from_satisfaction_target(
+            &source,
+            &OptToSatReduction {
+                target: ToySatisfactionProblem,
+            },
+            "opt->sat",
+        );
+    }
+
+    #[test]
+    fn test_satisfaction_round_trip_wrappers_accept_identity_reductions() {
+        let source = ToySatisfactionProblem;
+
+        assert_satisfaction_round_trip_from_optimization_target(
+            &source,
+            &SatToOptReduction {
+                target: ToyOptimizationProblem,
+            },
+            "sat->opt",
+        );
+        assert_satisfaction_round_trip_from_satisfaction_target(
+            &source,
+            &SatToSatReduction {
+                target: ToySatisfactionProblem,
+            },
+            "sat->sat",
+        );
+    }
+}
diff --git a/src/solvers/ilp/solver.rs b/src/solvers/ilp/solver.rs
index 881d706f3..42f832924 100644
--- a/src/solvers/ilp/solver.rs
+++ b/src/solvers/ilp/solver.rs
@@ -2,7 +2,13 @@
 
 use crate::models::algebraic::{Comparison, ObjectiveSense, VariableDomain, ILP};
 use crate::rules::{ReduceTo, ReductionResult};
-use good_lp::{default_solver, variable, ProblemVariables, Solution, SolverModel, Variable};
+#[cfg(not(feature = "ilp-highs"))]
+use good_lp::default_solver;
+#[cfg(feature = "ilp-highs")]
+use good_lp::highs;
+#[cfg(feature = "ilp-highs")]
+use good_lp::solvers::highs::HighsParallelType;
+use good_lp::{variable, ProblemVariables, Solution, SolverModel, Variable};
 
 /// An ILP solver using the HiGHS backend.
 ///
@@ -82,6 +88,20 @@ impl ILPSolver {
         };
 
         // Create the solver model
+        #[cfg(feature = "ilp-highs")]
+        let mut model = {
+            let mut model = unsolved
+                .using(highs)
+                .set_option("random_seed", 0i32)
+                .set_parallel(HighsParallelType::Off)
+                .set_threads(1);
+            if let Some(seconds) = self.time_limit {
+                model = model.set_time_limit(seconds);
+            }
+            model
+        };
+
+        #[cfg(not(feature = "ilp-highs"))]
         let mut model = unsolved.using(default_solver);
 
         // Add constraints
diff --git a/src/unit_tests/example_db.rs b/src/unit_tests/example_db.rs
index dc056dfd6..1152ffbd6 100644
--- a/src/unit_tests/example_db.rs
+++ b/src/unit_tests/example_db.rs
@@ -1,11 +1,19 @@
-use crate::example_db::{build_model_db, build_rule_db, find_model_example, find_rule_example};
-use crate::export::{lookup_overhead, ProblemRef, EXAMPLE_DB_VERSION};
+use crate::example_db::{
+    build_example_db, build_model_db, build_rule_db, compute_model_db, compute_rule_db,
+    find_model_example, find_rule_example,
+};
+use crate::export::ProblemRef;
+use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP, QUBO};
+use crate::models::graph::{MaximumMatching, SpinGlass};
+use crate::registry::load_dyn;
+use crate::rules::{registry::reduction_entries, ReductionGraph};
+use crate::topology::SimpleGraph;
+use serde_json::Value;
 use std::collections::{BTreeMap, BTreeSet, HashSet};
 
 #[test]
 fn test_build_model_db_contains_curated_examples() {
     let db = build_model_db().expect("model db should build");
-    assert_eq!(db.version, EXAMPLE_DB_VERSION);
     assert!(!db.models.is_empty(), "model db should not be empty");
     assert!(
         db.models
@@ -15,6 +23,13 @@ fn test_build_model_db_contains_curated_examples() {
     );
 }
 
+#[test]
+fn test_build_example_db_contains_models_and_rules() {
+    let db = build_example_db().expect("example db should build");
+    assert!(!db.models.is_empty(), "example db should contain models");
+    assert!(!db.rules.is_empty(), "example db should contain rules");
+}
+
 #[test]
 fn test_find_model_example_mis_simplegraph_i32() {
     let problem = ProblemRef {
@@ -117,7 +132,7 @@ fn test_build_rule_db_has_unique_structural_keys() {
 }
 
 #[test]
-fn test_path_based_rule_example_does_not_require_direct_overhead() {
+fn test_find_rule_example_rejects_composed_path_pairs() {
     let source = ProblemRef {
         name: "MaximumIndependentSet".to_string(),
         variant: BTreeMap::from([
@@ -130,14 +145,10 @@ fn test_path_based_rule_example_does_not_require_direct_overhead() {
         variant: BTreeMap::from([("variable".to_string(), "bool".to_string())]),
     };
 
-    let example = find_rule_example(&source, &target).expect("path example should exist");
-    assert!(
-        !example.overhead.is_empty(),
-        "path example should carry composed overhead"
-    );
+    let result = find_rule_example(&source, &target);
     assert!(
-        lookup_overhead(&source.name, &source.variant, &target.name, &target.variant).is_none(),
-        "path example should not require a direct-edge overhead entry"
+        result.is_err(),
+        "rule example db should only expose primitive direct reductions"
     );
 }
 
@@ -162,6 +173,38 @@ fn test_build_rule_db_nonempty() {
     assert!(!db.rules.is_empty(), "rule db should not be empty");
 }
 
+#[test]
+fn test_rule_examples_store_single_solution_pair() {
+    let db = build_rule_db().expect("rule db should build");
+    for rule in &db.rules {
+        assert_eq!(
+            rule.solutions.len(),
+            1,
+            "canonical rule example should store one witness pair for {} {:?} -> {} {:?}",
+            rule.source.problem,
+            rule.source.variant,
+            rule.target.problem,
+            rule.target.variant
+        );
+    }
+}
+
+#[test]
+fn test_computed_rule_examples_store_single_solution_pair() {
+    let db = compute_rule_db().expect("computed rule db should build");
+    for rule in &db.rules {
+        assert_eq!(
+            rule.solutions.len(),
+            1,
+            "computed canonical rule example should store one witness pair for {} {:?} -> {} {:?}",
+            rule.source.problem,
+            rule.source.variant,
+            rule.target.problem,
+            rule.target.variant
+        );
+    }
+}
+
 #[test]
 fn test_build_model_db_nonempty() {
     let db = build_model_db().expect("model db should build");
@@ -201,6 +244,38 @@ fn canonical_rule_example_ids_are_unique() {
     }
 }
 
+#[test]
+fn canonical_rule_examples_cover_exactly_authored_direct_reductions() {
+    let computed = compute_rule_db().expect("computed rule db should build");
+    let example_keys: BTreeSet<_> = computed
+        .rules
+        .iter()
+        .map(|rule| (rule.source.problem_ref(), rule.target.problem_ref()))
+        .collect();
+
+    let direct_reduction_keys: BTreeSet<_> = reduction_entries()
+        .into_iter()
+        .filter(|entry| entry.source_name != entry.target_name)
+        .map(|entry| {
+            (
+                ProblemRef {
+                    name: entry.source_name.to_string(),
+                    variant: ReductionGraph::variant_to_map(&entry.source_variant()),
+                },
+                ProblemRef {
+                    name: entry.target_name.to_string(),
+                    variant: ReductionGraph::variant_to_map(&entry.target_variant()),
+                },
+            )
+        })
+        .collect();
+
+    assert_eq!(
+        example_keys, direct_reduction_keys,
+        "rule example coverage should match authored direct reductions exactly"
+    );
+}
+
 // ---- Error path tests for example_db ----
 
 #[test]
@@ -237,10 +312,420 @@ fn find_model_example_nonexistent_returns_error() {
     );
 }
 
+fn problem_json_key(value: &Value) -> String {
+    serde_json::to_string(value).expect("json value should serialize")
+}
+
+fn edge_key(edge: &Value) -> (u64, u64, String) {
+    let values = edge
+        .as_array()
+        .expect("graph edge should serialize as a JSON array");
+    let u = values.first().and_then(Value::as_u64).unwrap_or(u64::MAX);
+    let v = values.get(1).and_then(Value::as_u64).unwrap_or(u64::MAX);
+    (u, v, problem_json_key(edge))
+}
+
+fn term_key(term: &Value) -> (u64, String) {
+    let values = term
+        .as_array()
+        .expect("ILP term should serialize as a JSON array");
+    let variable = values.first().and_then(Value::as_u64).unwrap_or(u64::MAX);
+    (variable, problem_json_key(term))
+}
+
+fn graph_edges_mut(object: &mut serde_json::Map<String, Value>) -> Option<&mut Vec<Value>> {
+    let graph = object.get_mut("graph")?.as_object_mut()?;
+    if graph.contains_key("inner") {
+        return graph
+            .get_mut("inner")?
+            .as_object_mut()?
+            .get_mut("edges")?
+            .as_array_mut();
+    }
+    graph.get_mut("edges")?.as_array_mut()
+}
+
+fn reorder_array(values: &mut Vec<Value>, old_indices: &[usize]) {
+    let reordered: Vec<Value> = old_indices.iter().map(|&idx| values[idx].clone()).collect();
+    *values = reordered;
+}
+
+fn edge_aligned_fields(problem_name: &str) -> &'static [&'static str] {
+    match problem_name {
+        "MaximumMatching" | "MaxCut" | "TravelingSalesman" => &["edge_weights"],
+        "SpinGlass" => &["couplings"],
+        _ => &[],
+    }
+}
+
+fn normalize_graph_instance(problem_name: &str, instance: &mut Value) {
+    let Some(object) = instance.as_object_mut() else {
+        return;
+    };
+    let edge_order = {
+        let Some(edges) = graph_edges_mut(object) else {
+            return;
+        };
+        let mut indexed_edges: Vec<(usize, Value)> = edges.iter().cloned().enumerate().collect();
+        indexed_edges.sort_by_key(|(_, edge)| edge_key(edge));
+        *edges = indexed_edges.iter().map(|(_, edge)| edge.clone()).collect();
+        indexed_edges
+            .into_iter()
+            .map(|(old_index, _)| old_index)
+            .collect::<Vec<_>>()
+    };
+
+    for field in edge_aligned_fields(problem_name) {
+        if let Some(values) = object.get_mut(*field).and_then(Value::as_array_mut) {
+            assert_eq!(
+                values.len(),
+                edge_order.len(),
+                "{problem_name}.{field} should stay aligned with graph edges",
+            );
+            reorder_array(values, &edge_order);
+        }
+    }
+}
+
+fn normalize_ilp_instance(instance: &mut Value) {
+    let Some(object) = instance.as_object_mut() else {
+        return;
+    };
+
+    if let Some(objective) = object.get_mut("objective").and_then(Value::as_array_mut) {
+        objective.sort_by_key(term_key);
+    }
+
+    if let Some(constraints) = object.get_mut("constraints").and_then(Value::as_array_mut) {
+        for constraint in constraints.iter_mut() {
+            if let Some(terms) = constraint.get_mut("terms").and_then(Value::as_array_mut) {
+                terms.sort_by_key(term_key);
+            }
+        }
+        constraints.sort_by_key(problem_json_key);
+    }
+}
+
+fn normalize_problem_instance(problem: &ProblemRef, instance: &Value) -> Value {
+    let loaded =
+        load_dyn(&problem.name, &problem.variant, instance.clone()).unwrap_or_else(|err| {
+            panic!(
+                "fixture instance should deserialize for {} {:?}: {}",
+                problem.name, problem.variant, err
+            )
+        });
+    let mut normalized = loaded.serialize_json();
+    normalize_graph_instance(&problem.name, &mut normalized);
+    if problem.name == "ILP" {
+        normalize_ilp_instance(&mut normalized);
+    }
+    normalized
+}
+
+fn numbers_semantically_equal(left: &serde_json::Number, right: &serde_json::Number) -> bool {
+    match (left.as_i64(), right.as_i64(), left.as_u64(), right.as_u64()) {
+        (Some(a), Some(b), _, _) => a == b,
+        (_, _, Some(a), Some(b)) => a == b,
+        _ => {
+            let Some(left) = left.as_f64() else {
+                return false;
+            };
+            let Some(right) = right.as_f64() else {
+                return false;
+            };
+            let scale = left.abs().max(right.abs()).max(1.0);
+            (left - right).abs() <= 1e-12 * scale
+        }
+    }
+}
+
+fn json_semantically_equal(left: &Value, right: &Value) -> bool {
+    match (left, right) {
+        (Value::Null, Value::Null) => true,
+        (Value::Bool(a), Value::Bool(b)) => a == b,
+        (Value::Number(a), Value::Number(b)) => numbers_semantically_equal(a, b),
+        (Value::String(a), Value::String(b)) => a == b,
+        (Value::Array(a), Value::Array(b)) => {
+            a.len() == b.len()
+                && a.iter()
+                    .zip(b.iter())
+                    .all(|(left, right)| json_semantically_equal(left, right))
+        }
+        (Value::Object(a), Value::Object(b)) => {
+            a.len() == b.len()
+                && a.iter().all(|(key, left_value)| {
+                    b.get(key)
+                        .map(|right_value| json_semantically_equal(left_value, right_value))
+                        .unwrap_or(false)
+                })
+        }
+        _ => false,
+    }
+}
+
 #[test]
-fn default_generated_dir_returns_path() {
-    use crate::example_db::default_generated_dir;
-    let dir = default_generated_dir();
-    // Should return a valid path (either from env or the default)
-    assert!(!dir.as_os_str().is_empty());
+fn normalize_problem_instance_treats_reordered_ilp_as_equal() {
+    let problem = ProblemRef {
+        name: "ILP".to_string(),
+        variant: BTreeMap::from([("variable".to_string(), "bool".to_string())]),
+    };
+    let canonical = ILP::<bool>::new(
+        3,
+        vec![
+            LinearConstraint::le(vec![(0, 1.0), (2, 1.0)], 1.0),
+            LinearConstraint::ge(vec![(1, 2.0), (0, 1.0)], 2.0),
+        ],
+        vec![(2, 3.0), (0, 1.0)],
+        ObjectiveSense::Maximize,
+    );
+    let canonical = serde_json::to_value(&canonical).expect("ILP should serialize");
+
+    let reordered = ILP::<bool>::new(
+        3,
+        vec![
+            LinearConstraint::ge(vec![(0, 1.0), (1, 2.0)], 2.0),
+            LinearConstraint::le(vec![(2, 1.0), (0, 1.0)], 1.0),
+        ],
+        vec![(0, 1.0), (2, 3.0)],
+        ObjectiveSense::Maximize,
+    );
+    let reordered = serde_json::to_value(&reordered).expect("ILP should serialize");
+
+    assert_eq!(
+        normalize_problem_instance(&problem, &canonical),
+        normalize_problem_instance(&problem, &reordered)
+    );
+}
+
+#[test]
+fn json_semantically_equal_treats_tiny_float_roundoff_as_equal() {
+    let problem = ProblemRef {
+        name: "QUBO".to_string(),
+        variant: BTreeMap::from([("weight".to_string(), "f64".to_string())]),
+    };
+    let canonical = QUBO::from_matrix(vec![vec![0.2, -1.5], vec![0.0, 1.0]]);
+    let canonical = normalize_problem_instance(
+        &problem,
+        &serde_json::to_value(&canonical).expect("QUBO should serialize"),
+    );
+
+    let noisy = QUBO::from_matrix(vec![vec![0.20000000000000018, -1.5], vec![0.0, 1.0]]);
+    let noisy = normalize_problem_instance(
+        &problem,
+        &serde_json::to_value(&noisy).expect("QUBO should serialize"),
+    );
+
+    assert!(
+        json_semantically_equal(&canonical, &noisy),
+        "tiny float noise should not count as a fixture mismatch"
+    );
+}
+
+#[test]
+fn normalize_problem_instance_treats_reordered_graph_edges_as_equal() {
+    let problem = ProblemRef {
+        name: "MaximumMatching".to_string(),
+        variant: BTreeMap::from([
+            ("graph".to_string(), "SimpleGraph".to_string()),
+            ("weight".to_string(), "i32".to_string()),
+        ]),
+    };
+    let canonical = MaximumMatching::<_, i32>::new(
+        SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]),
+        vec![5, 7, 11],
+    );
+    let canonical = serde_json::to_value(&canonical).expect("matching should serialize");
+
+    let reordered = MaximumMatching::<_, i32>::new(
+        SimpleGraph::new(4, vec![(2, 3), (0, 1), (1, 2)]),
+        vec![11, 5, 7],
+    );
+    let reordered = serde_json::to_value(&reordered).expect("matching should serialize");
+
+    assert_eq!(
+        normalize_problem_instance(&problem, &canonical),
+        normalize_problem_instance(&problem, &reordered)
+    );
+}
+
+#[test]
+fn normalize_problem_instance_treats_reordered_spin_glass_interactions_as_equal() {
+    let problem = ProblemRef {
+        name: "SpinGlass".to_string(),
+        variant: BTreeMap::from([
+            ("graph".to_string(), "SimpleGraph".to_string()),
+            ("weight".to_string(), "i32".to_string()),
+        ]),
+    };
+    let canonical = SpinGlass::<SimpleGraph, i32>::new(
+        3,
+        vec![((0, 1), 5), ((1, 2), -2), ((0, 2), 9)],
+        vec![1, 0, -1],
+    );
+    let canonical = serde_json::to_value(&canonical).expect("spin glass should serialize");
+
+    let reordered = SpinGlass::<SimpleGraph, i32>::new(
+        3,
+        vec![((0, 2), 9), ((0, 1), 5), ((1, 2), -2)],
+        vec![1, 0, -1],
+    );
+    let reordered = serde_json::to_value(&reordered).expect("spin glass should serialize");
+
+    assert_eq!(
+        normalize_problem_instance(&problem, &canonical),
+        normalize_problem_instance(&problem, &reordered)
+    );
+}
+
+// ---- Fixture verification tests ----
+// These verify that stored fixtures are structurally and semantically
+// consistent with freshly computed results. Rule fixture ordering can vary,
+// so compare keyed content instead of relying on positional equality.
+
+#[test]
+fn verify_model_fixtures_match_computed() {
+    let loaded = build_model_db().expect("fixture should load");
+    let computed = compute_model_db().expect("compute should succeed");
+    assert_eq!(
+        loaded.models.len(),
+        computed.models.len(),
+        "fixture and computed model counts differ — regenerate fixtures"
+    );
+    for (loaded_model, computed_model) in loaded.models.iter().zip(computed.models.iter()) {
+        assert_eq!(
+            loaded_model.problem, computed_model.problem,
+            "model fixture mismatch for {} {:?} — problem name drifted",
+            loaded_model.problem, loaded_model.variant
+        );
+        assert_eq!(
+            loaded_model.variant, computed_model.variant,
+            "model fixture mismatch for {} {:?} — variant drifted",
+            loaded_model.problem, loaded_model.variant
+        );
+        let loaded_instance =
+            normalize_problem_instance(&loaded_model.problem_ref(), &loaded_model.instance);
+        let computed_instance =
+            normalize_problem_instance(&computed_model.problem_ref(), &computed_model.instance);
+        assert!(
+            json_semantically_equal(&loaded_instance, &computed_instance),
+            "model fixture instance mismatch for {} {:?} — regenerate fixtures with: \
+             cargo run --release --example regenerate_fixtures --features \"ilp-highs example-db\"",
+            loaded_model.problem,
+            loaded_model.variant
+        );
+        assert_eq!(
+            loaded_model.samples, computed_model.samples,
+            "model fixture sample evaluations mismatch for {} {:?} — regenerate fixtures with: \
+             cargo run --release --example regenerate_fixtures --features \"ilp-highs example-db\"",
+            loaded_model.problem, loaded_model.variant
+        );
+        assert_eq!(
+            loaded_model.optimal, computed_model.optimal,
+            "model fixture optima mismatch for {} {:?} — regenerate fixtures with: \
+             cargo run --release --example regenerate_fixtures --features \"ilp-highs example-db\"",
+            loaded_model.problem, loaded_model.variant
+        );
+    }
+}
+
+#[test]
+fn verify_rule_fixtures_match_computed() {
+    let loaded = build_rule_db().expect("fixture should load");
+    let computed = compute_rule_db().expect("computed rule db should build");
+    assert_eq!(
+        loaded.rules.len(),
+        computed.rules.len(),
+        "fixture and computed rule counts differ — regenerate fixtures"
+    );
+    let loaded_keys: BTreeSet<_> = loaded
+        .rules
+        .iter()
+        .map(|r| (r.source.problem_ref(), r.target.problem_ref()))
+        .collect();
+    let computed_keys: BTreeSet<_> = computed
+        .rules
+        .iter()
+        .map(|r| (r.source.problem_ref(), r.target.problem_ref()))
+        .collect();
+    assert_eq!(
+        loaded_keys, computed_keys,
+        "fixture and computed rule sets differ — regenerate fixtures"
+    );
+    let loaded_by_key: BTreeMap<_, _> = loaded
+        .rules
+        .iter()
+        .map(|rule| ((rule.source.problem_ref(), rule.target.problem_ref()), rule))
+        .collect();
+    let computed_by_key: BTreeMap<_, _> = computed
+        .rules
+        .iter()
+        .map(|rule| ((rule.source.problem_ref(), rule.target.problem_ref()), rule))
+        .collect();
+
+    for key in loaded_keys {
+        let loaded_rule = loaded_by_key
+            .get(&key)
+            .expect("loaded fixture key should exist");
+        let computed_rule = computed_by_key
+            .get(&key)
+            .expect("computed fixture key should exist");
+
+        let loaded_source = normalize_problem_instance(
+            &loaded_rule.source.problem_ref(),
+            &loaded_rule.source.instance,
+        );
+        let computed_source = normalize_problem_instance(
+            &computed_rule.source.problem_ref(),
+            &computed_rule.source.instance,
+        );
+        assert!(
+            json_semantically_equal(&loaded_source, &computed_source),
+            "source instance mismatch for {} -> {} — regenerate fixtures",
+            loaded_rule.source.problem,
+            loaded_rule.target.problem
+        );
+        let loaded_target = normalize_problem_instance(
+            &loaded_rule.target.problem_ref(),
+            &loaded_rule.target.instance,
+        );
+        let computed_target = normalize_problem_instance(
+            &computed_rule.target.problem_ref(),
+            &computed_rule.target.instance,
+        );
+        assert!(
+            json_semantically_equal(&loaded_target, &computed_target),
+            "target instance mismatch for {} -> {} — regenerate fixtures",
+            loaded_rule.source.problem,
+            loaded_rule.target.problem
+        );
+        // Solution witnesses may differ across platforms (ILP solver
+        // nondeterminism), so compare energy (objective value) rather than
+        // exact configs — both must be optimal.
+        assert_eq!(
+            loaded_rule.solutions.len(),
+            computed_rule.solutions.len(),
+            "solution count mismatch for {} -> {} — regenerate fixtures",
+            loaded_rule.source.problem, loaded_rule.target.problem
+        );
+        let label =
+            format!("{} -> {}", loaded_rule.source.problem, loaded_rule.target.problem);
+        for (loaded_pair, computed_pair) in
+            loaded_rule.solutions.iter().zip(computed_rule.solutions.iter())
+        {
+            let loaded_target_problem = load_dyn(
+                &loaded_rule.target.problem,
+                &loaded_rule.target.variant,
+                loaded_rule.target.instance.clone(),
+            )
+            .unwrap_or_else(|e| panic!("{label}: load target: {e}"));
+            let loaded_energy =
+                loaded_target_problem.evaluate_dyn(&loaded_pair.target_config);
+            let computed_energy =
+                loaded_target_problem.evaluate_dyn(&computed_pair.target_config);
+            assert_eq!(
+                loaded_energy, computed_energy,
+                "{label}: target energy mismatch — regenerate fixtures"
+            );
+        }
+    }
 }
diff --git a/src/unit_tests/export.rs b/src/unit_tests/export.rs
index 46aefc7db..d6c4dc395 100644
--- a/src/unit_tests/export.rs
+++ b/src/unit_tests/export.rs
@@ -1,54 +1,4 @@
 use super::*;
-use crate::expr::Expr;
-use crate::rules::registry::ReductionOverhead;
-
-#[test]
-fn test_overhead_to_json_empty() {
-    let overhead = ReductionOverhead::default();
-    let entries = overhead_to_json(&overhead);
-    assert!(entries.is_empty());
-}
-
-#[test]
-fn test_overhead_to_json_single_field() {
-    let overhead = ReductionOverhead::new(vec![("num_vertices", Expr::Var("n") + Expr::Var("m"))]);
-    let entries = overhead_to_json(&overhead);
-    assert_eq!(entries.len(), 1);
-    assert_eq!(entries[0].field, "num_vertices");
-    assert_eq!(entries[0].formula, "n + m");
-}
-
-#[test]
-fn test_overhead_to_json_constant() {
-    let overhead = ReductionOverhead::new(vec![("num_vars", Expr::Const(42.0))]);
-    let entries = overhead_to_json(&overhead);
-    assert_eq!(entries.len(), 1);
-    assert_eq!(entries[0].field, "num_vars");
-    assert_eq!(entries[0].formula, "42");
-}
-
-#[test]
-fn test_overhead_to_json_scaled_power() {
-    let overhead = ReductionOverhead::new(vec![(
-        "num_edges",
-        Expr::Const(3.0) * Expr::pow(Expr::Var("n"), Expr::Const(2.0)),
-    )]);
-    let entries = overhead_to_json(&overhead);
-    assert_eq!(entries.len(), 1);
-    assert_eq!(entries[0].formula, "3 * n^2");
-}
-
-#[test]
-fn test_overhead_to_json_multiple_fields() {
-    let overhead = ReductionOverhead::new(vec![
-        ("num_vertices", Expr::Var("n")),
-        ("num_edges", Expr::pow(Expr::Var("n"), Expr::Const(2.0))),
-    ]);
-    let entries = overhead_to_json(&overhead);
-    assert_eq!(entries.len(), 2);
-    assert_eq!(entries[0].field, "num_vertices");
-    assert_eq!(entries[1].field, "num_edges");
-}
 
 #[test]
 fn test_variant_to_map_empty() {
@@ -93,7 +43,7 @@ fn test_lookup_overhead_unknown_reduction() {
 }
 
 #[test]
-fn test_write_canonical_example_dbs() {
+fn test_write_canonical_example_db() {
     use std::fs;
     use std::time::{SystemTime, UNIX_EPOCH};
 
@@ -106,8 +56,14 @@ fn test_write_canonical_example_dbs() {
     ));
     fs::create_dir_all(&dir).unwrap();
 
-    let rule_db = RuleDb {
-        version: EXAMPLE_DB_VERSION,
+    let db = ExampleDb {
+        models: vec![ModelExample {
+            problem: "ModelProblem".to_string(),
+            variant: variant_to_map(vec![("graph", "SimpleGraph")]),
+            instance: serde_json::json!({"n": 5}),
+            samples: vec![],
+            optimal: vec![],
+        }],
         rules: vec![RuleExample {
             source: ProblemSide {
                 problem: "SourceProblem".to_string(),
@@ -119,12 +75,46 @@ fn test_write_canonical_example_dbs() {
                 variant: variant_to_map(vec![("weight", "i32")]),
                 instance: serde_json::json!({"m": 4}),
             },
-            overhead: vec![],
             solutions: vec![],
         }],
     };
-    let model_db = ModelDb {
-        version: EXAMPLE_DB_VERSION,
+    write_example_db_to(&dir, &db);
+
+    let examples_json: serde_json::Value =
+        serde_json::from_str(&fs::read_to_string(dir.join("examples.json")).unwrap()).unwrap();
+
+    assert_eq!(
+        examples_json["rules"][0]["source"]["problem"],
+        "SourceProblem"
+    );
+    assert_eq!(examples_json["models"][0]["problem"], "ModelProblem");
+    assert!(
+        !dir.join("rules.json").exists(),
+        "canonical export should not split rules into a separate file"
+    );
+    assert!(
+        !dir.join("models.json").exists(),
+        "canonical export should not split models into a separate file"
+    );
+
+    let _ = fs::remove_dir_all(&dir);
+}
+
+#[test]
+fn test_write_example_db_uses_wrapped_json_contract() {
+    use std::fs;
+    use std::time::{SystemTime, UNIX_EPOCH};
+
+    let dir = std::env::temp_dir().join(format!(
+        "problemreductions-export-db-contract-test-{}",
+        SystemTime::now()
+            .duration_since(UNIX_EPOCH)
+            .unwrap()
+            .as_nanos()
+    ));
+    fs::create_dir_all(&dir).unwrap();
+
+    let db = ExampleDb {
         models: vec![ModelExample {
             problem: "ModelProblem".to_string(),
             variant: variant_to_map(vec![("graph", "SimpleGraph")]),
@@ -132,24 +122,125 @@ fn test_write_canonical_example_dbs() {
             samples: vec![],
             optimal: vec![],
         }],
+        rules: vec![RuleExample {
+            source: ProblemSide {
+                problem: "SourceProblem".to_string(),
+                variant: variant_to_map(vec![("graph", "SimpleGraph")]),
+                instance: serde_json::json!({"n": 3}),
+            },
+            target: ProblemSide {
+                problem: "TargetProblem".to_string(),
+                variant: variant_to_map(vec![("weight", "i32")]),
+                instance: serde_json::json!({"m": 4}),
+            },
+            solutions: vec![],
+        }],
     };
+    write_example_db_to(&dir, &db);
 
-    write_rule_db_to(&dir, &rule_db);
-    write_model_db_to(&dir, &model_db);
+    let examples_json: serde_json::Value =
+        serde_json::from_str(&fs::read_to_string(dir.join("examples.json")).unwrap()).unwrap();
 
-    let rules_json: serde_json::Value =
-        serde_json::from_str(&fs::read_to_string(dir.join("rules.json")).unwrap()).unwrap();
-    let models_json: serde_json::Value =
-        serde_json::from_str(&fs::read_to_string(dir.join("models.json")).unwrap()).unwrap();
+    assert_eq!(
+        examples_json["rules"][0]["source"]["problem"],
+        "SourceProblem"
+    );
+    assert_eq!(examples_json["models"][0]["problem"], "ModelProblem");
 
-    assert_eq!(rules_json["version"], EXAMPLE_DB_VERSION);
-    assert_eq!(rules_json["rules"][0]["source"]["problem"], "SourceProblem");
-    assert_eq!(models_json["version"], EXAMPLE_DB_VERSION);
-    assert_eq!(models_json["models"][0]["problem"], "ModelProblem");
+    let _ = fs::remove_dir_all(&dir);
+}
+
+#[test]
+fn test_write_example_db_uses_one_line_per_example_entry() {
+    use std::fs;
+    use std::time::{SystemTime, UNIX_EPOCH};
+
+    let dir = std::env::temp_dir().join(format!(
+        "problemreductions-export-db-lines-test-{}",
+        SystemTime::now()
+            .duration_since(UNIX_EPOCH)
+            .unwrap()
+            .as_nanos()
+    ));
+    fs::create_dir_all(&dir).unwrap();
+
+    let db = ExampleDb {
+        models: vec![ModelExample {
+            problem: "ModelProblem".to_string(),
+            variant: variant_to_map(vec![("graph", "SimpleGraph")]),
+            instance: serde_json::json!({"n": 5, "edges": [[0, 1], [1, 2]]}),
+            samples: vec![SampleEval {
+                config: vec![1, 0, 1],
+                metric: serde_json::json!({"Valid": 2}),
+            }],
+            optimal: vec![],
+        }],
+        rules: vec![RuleExample {
+            source: ProblemSide {
+                problem: "SourceProblem".to_string(),
+                variant: variant_to_map(vec![("graph", "SimpleGraph")]),
+                instance: serde_json::json!({"n": 3, "edges": [[0, 1], [1, 2]]}),
+            },
+            target: ProblemSide {
+                problem: "TargetProblem".to_string(),
+                variant: variant_to_map(vec![("weight", "i32")]),
+                instance: serde_json::json!({"m": 4, "weights": [1, 2, 3, 4]}),
+            },
+            solutions: vec![SolutionPair {
+                source_config: vec![1, 0, 1],
+                target_config: vec![0, 1, 1, 0],
+            }],
+        }],
+    };
+    write_example_db_to(&dir, &db);
+
+    let text = fs::read_to_string(dir.join("examples.json")).unwrap();
+    let model_line = text
+        .lines()
+        .find(|line| line.contains("\"problem\":\"ModelProblem\""))
+        .expect("model entry should appear on a single line");
+    let rule_line = text
+        .lines()
+        .find(|line| line.contains("\"problem\":\"SourceProblem\""))
+        .expect("rule entry should appear on a single line");
+
+    assert!(
+        model_line.trim().starts_with('{')
+            && model_line.trim().trim_end_matches(',').ends_with('}'),
+        "model entry should be serialized as one compact JSON object line"
+    );
+    assert!(
+        rule_line.trim().starts_with('{')
+            && rule_line.trim().trim_end_matches(',').ends_with('}'),
+        "rule entry should be serialized as one compact JSON object line"
+    );
 
     let _ = fs::remove_dir_all(&dir);
 }
 
+#[test]
+fn rule_example_serialization_omits_overhead() {
+    let example = RuleExample {
+        source: ProblemSide {
+            problem: "A".to_string(),
+            variant: variant_to_map(vec![]),
+            instance: serde_json::json!({"x": 1}),
+        },
+        target: ProblemSide {
+            problem: "B".to_string(),
+            variant: variant_to_map(vec![]),
+            instance: serde_json::json!({"y": 2}),
+        },
+        solutions: vec![],
+    };
+
+    let json = serde_json::to_value(&example).unwrap();
+    assert!(
+        json.get("overhead").is_none(),
+        "RuleExample should not duplicate reduction metadata"
+    );
+}
+
 #[test]
 fn test_problem_side_serialization() {
     let side = ProblemSide {
@@ -231,38 +322,6 @@ fn model_example_problem_ref() {
     assert_eq!(pref.variant["graph"], "SimpleGraph");
 }
 
-#[test]
-fn default_expr_returns_zero() {
-    let expr = default_expr();
-    assert_eq!(expr, Expr::Const(0.0));
-}
-
-#[test]
-fn examples_output_dir_fallback() {
-    // Without PROBLEMREDUCTIONS_EXAMPLES_DIR set, should fallback
-    let dir = examples_output_dir();
-    let expected = std::path::PathBuf::from("docs/paper/examples/generated");
-    // Clean env first to ensure deterministic result
-    if std::env::var_os(EXAMPLES_DIR_ENV).is_none() {
-        assert_eq!(dir, expected);
-    }
-}
-
-#[test]
-fn examples_output_dir_env_override() {
-    // Temporarily set the env var and check it's respected
-    let key = EXAMPLES_DIR_ENV;
-    let old = std::env::var_os(key);
-    std::env::set_var(key, "/tmp/custom_examples");
-    let dir = examples_output_dir();
-    assert_eq!(dir, std::path::PathBuf::from("/tmp/custom_examples"));
-    // Restore
-    match old {
-        Some(v) => std::env::set_var(key, v),
-        None => std::env::remove_var(key),
-    }
-}
-
 #[test]
 fn write_rule_example_to_creates_json_file() {
     use std::fs;
@@ -284,7 +343,6 @@ fn write_rule_example_to_creates_json_file() {
             variant: variant_to_map(vec![]),
             instance: serde_json::json!({"y": 2}),
         },
-        overhead: vec![],
         solutions: vec![],
     };
     write_rule_example_to(&dir, "test_rule", &example);
diff --git a/src/unit_tests/models/misc/minimum_tardiness_sequencing.rs b/src/unit_tests/models/misc/minimum_tardiness_sequencing.rs
index cfb1273d8..6d85c5ace 100644
--- a/src/unit_tests/models/misc/minimum_tardiness_sequencing.rs
+++ b/src/unit_tests/models/misc/minimum_tardiness_sequencing.rs
@@ -168,11 +168,7 @@ fn test_minimum_tardiness_sequencing_invalid_precedence() {
 #[test]
 fn test_minimum_tardiness_sequencing_cyclic_precedences() {
     // Cyclic precedences: 0 -> 1 -> 2 -> 0. No valid schedule exists.
-    let problem = MinimumTardinessSequencing::new(
-        3,
-        vec![3, 3, 3],
-        vec![(0, 1), (1, 2), (2, 0)],
-    );
+    let problem = MinimumTardinessSequencing::new(3, vec![3, 3, 3], vec![(0, 1), (1, 2), (2, 0)]);
     let solver = BruteForce::new();
     assert!(solver.find_best(&problem).is_none());
 }
diff --git a/src/unit_tests/rules/circuit_ilp.rs b/src/unit_tests/rules/circuit_ilp.rs
index 3e7bf257a..b40b5cc92 100644
--- a/src/unit_tests/rules/circuit_ilp.rs
+++ b/src/unit_tests/rules/circuit_ilp.rs
@@ -1,7 +1,7 @@
 use super::*;
 use crate::models::formula::{Assignment, BooleanExpr, Circuit, CircuitSAT};
+use crate::rules::test_helpers::assert_satisfaction_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
-use std::collections::HashSet;
 
 #[test]
 fn test_circuitsat_to_ilp_and_gate() {
@@ -12,18 +12,11 @@ fn test_circuitsat_to_ilp_and_gate() {
     )]);
     let source = CircuitSAT::new(circuit);
     let reduction = ReduceTo::<ILP>::reduce_to(&source);
-    let ilp = reduction.target_problem();
-
-    let solver = BruteForce::new();
-    let best_target = solver.find_all_best(ilp);
-    let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect();
-
-    let extracted: HashSet<_> = best_target
-        .iter()
-        .map(|t| reduction.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
-    assert!(!extracted.is_empty());
+    assert_satisfaction_round_trip_from_optimization_target(
+        &source,
+        &reduction,
+        "CircuitSAT->ILP AND gate",
+    );
 }
 
 #[test]
@@ -35,17 +28,11 @@ fn test_circuitsat_to_ilp_or_gate() {
     )]);
     let source = CircuitSAT::new(circuit);
     let reduction = ReduceTo::<ILP>::reduce_to(&source);
-    let ilp = reduction.target_problem();
-
-    let solver = BruteForce::new();
-    let best_target = solver.find_all_best(ilp);
-    let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect();
-
-    let extracted: HashSet<_> = best_target
-        .iter()
-        .map(|t| reduction.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_satisfaction_round_trip_from_optimization_target(
+        &source,
+        &reduction,
+        "CircuitSAT->ILP OR gate",
+    );
 }
 
 #[test]
@@ -57,17 +44,12 @@ fn test_circuitsat_to_ilp_xor_gate() {
     )]);
     let source = CircuitSAT::new(circuit);
     let reduction = ReduceTo::<ILP>::reduce_to(&source);
-
-    let solver = BruteForce::new();
-    let best_target = solver.find_all_best(reduction.target_problem());
-    let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect();
-
-    let extracted: HashSet<_> = best_target
-        .iter()
-        .map(|t| reduction.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
-    assert_eq!(extracted.len(), 4); // all 4 truth table rows satisfy c == (x XOR y)
+    assert_satisfaction_round_trip_from_optimization_target(
+        &source,
+        &reduction,
+        "CircuitSAT->ILP XOR gate",
+    );
+    assert_eq!(BruteForce::new().find_all_satisfying(&source).len(), 4);
 }
 
 #[test]
@@ -82,16 +64,11 @@ fn test_circuitsat_to_ilp_nested() {
     )]);
     let source = CircuitSAT::new(circuit);
     let reduction = ReduceTo::<ILP>::reduce_to(&source);
-
-    let solver = BruteForce::new();
-    let best_target = solver.find_all_best(reduction.target_problem());
-    let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect();
-
-    let extracted: HashSet<_> = best_target
-        .iter()
-        .map(|t| reduction.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_satisfaction_round_trip_from_optimization_target(
+        &source,
+        &reduction,
+        "CircuitSAT->ILP nested",
+    );
 }
 
 #[test]
@@ -112,14 +89,9 @@ fn test_circuitsat_to_ilp_closed_loop() {
     ]);
     let source = CircuitSAT::new(circuit);
     let reduction = ReduceTo::<ILP>::reduce_to(&source);
-
-    let solver = BruteForce::new();
-    let best_target = solver.find_all_best(reduction.target_problem());
-    let best_source: HashSet<_> = solver.find_all_satisfying(&source).into_iter().collect();
-
-    let extracted: HashSet<_> = best_target
-        .iter()
-        .map(|t| reduction.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_satisfaction_round_trip_from_optimization_target(
+        &source,
+        &reduction,
+        "CircuitSAT->ILP closed loop",
+    );
 }
diff --git a/src/unit_tests/rules/circuit_spinglass.rs b/src/unit_tests/rules/circuit_spinglass.rs
index e0331e029..d1b43c5a1 100644
--- a/src/unit_tests/rules/circuit_spinglass.rs
+++ b/src/unit_tests/rules/circuit_spinglass.rs
@@ -1,5 +1,6 @@
 use super::*;
 use crate::models::formula::Circuit;
+use crate::rules::test_helpers::assert_satisfaction_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
 use crate::types::{NumericSize, WeightElement};
 use num_traits::Num;
@@ -294,16 +295,9 @@ fn test_jl_parity_circuitsat_to_spinglass() {
     ]);
     let source = CircuitSAT::new(circuit);
     let result = ReduceTo::<SpinGlass<SimpleGraph, i32>>::reduce_to(&source);
-    let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
-    let best_source = solver.find_all_satisfying(&source);
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    let best_source_set: HashSet<Vec<usize>> = best_source.into_iter().collect();
-    assert!(
-        extracted.is_subset(&best_source_set),
-        "CircuitSAT->SpinGlass: extracted not satisfying"
+    assert_satisfaction_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "CircuitSAT->SpinGlass parity",
     );
 }
diff --git a/src/unit_tests/rules/factoring_circuit.rs b/src/unit_tests/rules/factoring_circuit.rs
index 16019ab9f..9b4345e04 100644
--- a/src/unit_tests/rules/factoring_circuit.rs
+++ b/src/unit_tests/rules/factoring_circuit.rs
@@ -1,6 +1,6 @@
 use super::*;
+use crate::rules::test_helpers::assert_optimization_round_trip_from_satisfaction_target;
 use crate::solvers::BruteForce;
-use crate::traits::Problem;
 use std::collections::HashMap;
 include!("../jl_helpers.rs");
 
@@ -300,20 +300,16 @@ fn test_factorization_1_trivial() {
 fn test_jl_parity_factoring_to_circuitsat() {
     let source = Factoring::new(1, 1, 1);
     let result = ReduceTo::<CircuitSAT>::reduce_to(&source);
-    let solver = BruteForce::new();
-    let best_target = solver.find_all_satisfying(result.target_problem());
-    for t in &best_target {
-        let sol = result.extract_solution(t);
-        assert_eq!(
-            source.evaluate(&sol).unwrap(),
-            0,
-            "Factoring extracted solution should be valid"
-        );
-    }
+    assert_optimization_round_trip_from_satisfaction_target(
+        &source,
+        &result,
+        "Factoring->CircuitSAT parity",
+    );
     let data: serde_json::Value = serde_json::from_str(include_str!(
         "../../../tests/data/jl/factoring_to_circuitsat.json"
     ))
     .unwrap();
+    let solver = BruteForce::new();
     let jl_best_source = jl_parse_configs_set(&data["cases"][0]["best_source"]);
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
     assert_eq!(
diff --git a/src/unit_tests/rules/knapsack_qubo.rs b/src/unit_tests/rules/knapsack_qubo.rs
index a92e552a2..2c18acc1a 100644
--- a/src/unit_tests/rules/knapsack_qubo.rs
+++ b/src/unit_tests/rules/knapsack_qubo.rs
@@ -1,4 +1,5 @@
 use super::*;
+use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
 use crate::traits::Problem;
 
@@ -10,18 +11,11 @@ fn test_knapsack_to_qubo_closed_loop() {
 
     assert_eq!(qubo.num_vars(), 7);
 
-    let solver = BruteForce::new();
-    let best_source = solver.find_all_best(&knapsack);
-    let best_target = solver.find_all_best(qubo);
-
-    let extracted: std::collections::HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| reduction.extract_solution(t))
-        .collect();
-    let source_set: std::collections::HashSet<Vec<usize>> = best_source.into_iter().collect();
-
-    assert!(extracted.is_subset(&source_set));
-    assert!(!extracted.is_empty());
+    assert_optimization_round_trip_from_optimization_target(
+        &knapsack,
+        &reduction,
+        "Knapsack->QUBO closed loop",
+    );
 }
 
 #[test]
diff --git a/src/unit_tests/rules/maximumclique_maximumindependentset.rs b/src/unit_tests/rules/maximumclique_maximumindependentset.rs
index 725f61cb3..8e871f7ba 100644
--- a/src/unit_tests/rules/maximumclique_maximumindependentset.rs
+++ b/src/unit_tests/rules/maximumclique_maximumindependentset.rs
@@ -1,9 +1,9 @@
 use super::*;
+use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
 use crate::topology::Graph;
 use crate::traits::Problem;
 use crate::types::SolutionSize;
-use std::collections::HashSet;
 
 #[test]
 fn test_maximumclique_to_maximumindependentset_closed_loop() {
@@ -21,21 +21,11 @@ fn test_maximumclique_to_maximumindependentset_closed_loop() {
     assert_eq!(target.graph().num_vertices(), 4);
     assert_eq!(target.graph().num_edges(), 3); // 4*3/2 - 3 = 3
 
-    let solver = BruteForce::new();
-
-    // Solve target (MIS on complement graph)
-    let target_solutions = solver.find_all_best(target);
-    assert!(!target_solutions.is_empty());
-
-    // Solve source directly
-    let source_solutions: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    assert!(!source_solutions.is_empty());
-
-    // Extract solutions and verify they are optimal for source
-    for target_sol in &target_solutions {
-        let source_sol = reduction.extract_solution(target_sol);
-        assert!(source_solutions.contains(&source_sol));
-    }
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &reduction,
+        "MaximumClique->MaximumIndependentSet closed loop",
+    );
 }
 
 #[test]
diff --git a/src/unit_tests/rules/maximumindependentset_maximumclique.rs b/src/unit_tests/rules/maximumindependentset_maximumclique.rs
index 1be4efe1e..9225eaf72 100644
--- a/src/unit_tests/rules/maximumindependentset_maximumclique.rs
+++ b/src/unit_tests/rules/maximumindependentset_maximumclique.rs
@@ -1,7 +1,7 @@
 use super::*;
+use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
 use crate::traits::Problem;
-use std::collections::HashSet;
 
 #[test]
 fn test_maximumindependentset_to_maximumclique_closed_loop() {
@@ -17,16 +17,11 @@ fn test_maximumindependentset_to_maximumclique_closed_loop() {
     assert_eq!(target.num_vertices(), 5);
     assert_eq!(target.num_edges(), 6);
 
-    let solver = BruteForce::new();
-    let best_target = solver.find_all_best(target);
-    let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-
-    // Extract solutions and verify they are valid source solutions
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| reduction.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &reduction,
+        "MaximumIndependentSet->MaximumClique closed loop",
+    );
 }
 
 #[test]
diff --git a/src/unit_tests/rules/maximumindependentset_maximumsetpacking.rs b/src/unit_tests/rules/maximumindependentset_maximumsetpacking.rs
index b80e4619e..6ed1983c6 100644
--- a/src/unit_tests/rules/maximumindependentset_maximumsetpacking.rs
+++ b/src/unit_tests/rules/maximumindependentset_maximumsetpacking.rs
@@ -1,4 +1,5 @@
 use super::*;
+use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
 use crate::types::One;
 include!("../jl_helpers.rs");
@@ -80,13 +81,12 @@ fn test_jl_parity_is_to_setpacking() {
         MaximumIndependentSet::new(SimpleGraph::new(nv, jl_parse_edges(inst)), vec![1i32; nv]);
     let result = ReduceTo::<MaximumSetPacking<i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity MIS->SetPacking",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -104,13 +104,12 @@ fn test_jl_parity_setpacking_to_is() {
     let source = MaximumSetPacking::<i32>::new(jl_parse_sets(&inst["sets"]));
     let result = ReduceTo::<MaximumIndependentSet<SimpleGraph, i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity SetPacking->MIS",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -130,13 +129,12 @@ fn test_jl_parity_rule_is_to_setpacking() {
         MaximumIndependentSet::new(SimpleGraph::new(nv, jl_parse_edges(inst)), vec![1i32; nv]);
     let result = ReduceTo::<MaximumSetPacking<i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity rule MIS->SetPacking",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -157,13 +155,12 @@ fn test_jl_parity_doc_is_to_setpacking() {
         MaximumIndependentSet::new(SimpleGraph::new(nv, jl_parse_edges(inst)), vec![1i32; nv]);
     let result = ReduceTo::<MaximumSetPacking<i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity doc MIS->SetPacking",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
diff --git a/src/unit_tests/rules/maximummatching_maximumsetpacking.rs b/src/unit_tests/rules/maximummatching_maximumsetpacking.rs
index 9b38e7b85..beab0a2c6 100644
--- a/src/unit_tests/rules/maximummatching_maximumsetpacking.rs
+++ b/src/unit_tests/rules/maximummatching_maximumsetpacking.rs
@@ -1,4 +1,5 @@
 use super::*;
+use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
 use crate::topology::SimpleGraph;
 use crate::traits::Problem;
@@ -169,15 +170,11 @@ fn test_jl_parity_matching_to_setpacking() {
         );
         let result = ReduceTo::<MaximumSetPacking<i32>>::reduce_to(&source);
         let solver = BruteForce::new();
-        let best_target = solver.find_all_best(result.target_problem());
         let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-        let extracted: HashSet<Vec<usize>> = best_target
-            .iter()
-            .map(|t| result.extract_solution(t))
-            .collect();
-        assert!(
-            extracted.is_subset(&best_source),
-            "Matching->SP [{label}]: extracted not subset"
+        assert_optimization_round_trip_from_optimization_target(
+            &source,
+            &result,
+            &format!("Matching->SP [{label}]"),
         );
         for case in data["cases"].as_array().unwrap() {
             assert_eq!(
diff --git a/src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs b/src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs
index 1664b8520..dd4533fd6 100644
--- a/src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs
+++ b/src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs
@@ -1,4 +1,5 @@
 use super::*;
+use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
 include!("../jl_helpers.rs");
 
@@ -41,13 +42,8 @@ fn test_jl_parity_is_to_vertexcovering() {
         MaximumIndependentSet::new(SimpleGraph::new(nv, jl_parse_edges(inst)), vec![1i32; nv]);
     let result = ReduceTo::<MinimumVertexCover<SimpleGraph, i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(&source, &result, "JL parity MIS->VC");
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -67,13 +63,12 @@ fn test_jl_parity_rule_is_to_vertexcovering() {
         MaximumIndependentSet::new(SimpleGraph::new(nv, jl_parse_edges(inst)), vec![1i32; nv]);
     let result = ReduceTo::<MinimumVertexCover<SimpleGraph, i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity rule MIS->VC",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
diff --git a/src/unit_tests/rules/minimumvertexcover_minimumsetcovering.rs b/src/unit_tests/rules/minimumvertexcover_minimumsetcovering.rs
index 6a9b56139..d3387ac46 100644
--- a/src/unit_tests/rules/minimumvertexcover_minimumsetcovering.rs
+++ b/src/unit_tests/rules/minimumvertexcover_minimumsetcovering.rs
@@ -1,4 +1,5 @@
 use super::*;
+use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
 include!("../jl_helpers.rs");
 
@@ -123,13 +124,12 @@ fn test_jl_parity_vc_to_setcovering() {
     );
     let result = ReduceTo::<MinimumSetCovering<i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity VC->SetCovering",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -151,13 +151,12 @@ fn test_jl_parity_rule_vc_to_setcovering() {
     );
     let result = ReduceTo::<MinimumSetCovering<i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity rule VC->SetCovering",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
diff --git a/src/unit_tests/rules/qubo_ilp.rs b/src/unit_tests/rules/qubo_ilp.rs
index 2e58770f7..e95c8f568 100644
--- a/src/unit_tests/rules/qubo_ilp.rs
+++ b/src/unit_tests/rules/qubo_ilp.rs
@@ -1,6 +1,6 @@
 use super::*;
+use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
-use std::collections::HashSet;
 
 #[test]
 fn test_qubo_to_ilp_closed_loop() {
@@ -10,17 +10,11 @@ fn test_qubo_to_ilp_closed_loop() {
     // Optimal: x = [0, 1] with obj = -3
     let qubo = QUBO::from_matrix(vec![vec![2.0, 1.0], vec![0.0, -3.0]]);
     let reduction = ReduceTo::<ILP<bool>>::reduce_to(&qubo);
-    let ilp = reduction.target_problem();
-
-    let solver = BruteForce::new();
-    let best_target = solver.find_all_best(ilp);
-    let best_source: HashSet<_> = solver.find_all_best(&qubo).into_iter().collect();
-
-    let extracted: HashSet<_> = best_target
-        .iter()
-        .map(|t| reduction.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &qubo,
+        &reduction,
+        "QUBO->ILP closed loop",
+    );
 }
 
 #[test]
diff --git a/src/unit_tests/rules/reduction_path_parity.rs b/src/unit_tests/rules/reduction_path_parity.rs
index 976085471..9388fa5c9 100644
--- a/src/unit_tests/rules/reduction_path_parity.rs
+++ b/src/unit_tests/rules/reduction_path_parity.rs
@@ -5,12 +5,12 @@
 use crate::models::algebraic::QUBO;
 use crate::models::graph::{MaxCut, SpinGlass};
 use crate::models::misc::Factoring;
+use crate::rules::test_helpers::assert_optimization_round_trip_chain;
 use crate::rules::{MinimizeSteps, ReductionGraph};
 use crate::solvers::{BruteForce, Solver};
 use crate::topology::SimpleGraph;
 use crate::traits::Problem;
 use crate::types::ProblemSize;
-use std::collections::HashSet;
 
 /// Julia: paths = reduction_paths(MaxCut, SpinGlass)
 /// Julia: res = reduceto(paths[1], MaxCut(smallgraph(:petersen)))
@@ -106,19 +106,10 @@ fn test_jl_parity_maxcut_to_qubo_path() {
     let chain = graph
         .reduce_along_path(&rpath, &source as &dyn std::any::Any)
         .expect("Should reduce along path");
-
-    let solver = BruteForce::new();
-    let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let best_target = solver.find_all_best(chain.target_problem::<QUBO<f64>>());
-
-    // Julia: sort(extract_solution.(Ref(res), best2)) == sort(best1)
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| chain.extract_solution(t))
-        .collect();
-    assert_eq!(
-        extracted, best_source,
-        "MaxCut->QUBO path: extracted solutions should match direct source solutions"
+    assert_optimization_round_trip_chain::<MaxCut<SimpleGraph, i32>, QUBO<f64>>(
+        &source,
+        &chain,
+        "MaxCut->QUBO path parity",
     );
 }
 
diff --git a/src/unit_tests/rules/sat_circuitsat.rs b/src/unit_tests/rules/sat_circuitsat.rs
index dd028a7c2..85a403ea9 100644
--- a/src/unit_tests/rules/sat_circuitsat.rs
+++ b/src/unit_tests/rules/sat_circuitsat.rs
@@ -1,9 +1,10 @@
 use super::*;
 use crate::models::formula::{CNFClause, CircuitSAT, Satisfiability};
+use crate::rules::test_helpers::{
+    assert_satisfaction_round_trip_from_satisfaction_target, solve_satisfaction_problem,
+};
 use crate::rules::ReduceTo;
 use crate::solvers::BruteForce;
-use crate::traits::Problem;
-use std::collections::HashSet;
 
 #[test]
 fn test_sat_to_circuitsat_closed_loop() {
@@ -16,24 +17,11 @@ fn test_sat_to_circuitsat_closed_loop() {
         ],
     );
     let result = ReduceTo::<CircuitSAT>::reduce_to(&sat);
-    let solver = BruteForce::new();
-
-    // All satisfying assignments of the circuit should map back to SAT solutions
-    let best_target = solver.find_all_satisfying(result.target_problem());
-    assert!(!best_target.is_empty(), "CircuitSAT should have solutions");
-
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    let sat_solutions: HashSet<Vec<usize>> = solver.find_all_satisfying(&sat).into_iter().collect();
-
-    // Every extracted solution must satisfy the original SAT
-    for sol in &extracted {
-        assert!(sat.evaluate(sol), "Extracted solution must satisfy SAT");
-    }
-    // The extracted set should equal all SAT solutions
-    assert_eq!(extracted, sat_solutions);
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &sat,
+        &result,
+        "SAT->CircuitSAT closed loop",
+    );
 }
 
 #[test]
@@ -54,16 +42,11 @@ fn test_sat_to_circuitsat_single_clause() {
     // Single clause: (x1 v x2)
     let sat = Satisfiability::new(2, vec![CNFClause::new(vec![1, 2])]);
     let result = ReduceTo::<CircuitSAT>::reduce_to(&sat);
-    let solver = BruteForce::new();
-
-    let best_target = solver.find_all_satisfying(result.target_problem());
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    let sat_solutions: HashSet<Vec<usize>> = solver.find_all_satisfying(&sat).into_iter().collect();
-
-    assert_eq!(extracted, sat_solutions);
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &sat,
+        &result,
+        "SAT->CircuitSAT single clause",
+    );
 }
 
 #[test]
@@ -71,17 +54,14 @@ fn test_sat_to_circuitsat_single_literal_clause() {
     // Single literal clause: (x1) & (x2)
     let sat = Satisfiability::new(2, vec![CNFClause::new(vec![1]), CNFClause::new(vec![2])]);
     let result = ReduceTo::<CircuitSAT>::reduce_to(&sat);
-    let solver = BruteForce::new();
-
-    let best_target = solver.find_all_satisfying(result.target_problem());
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    let sat_solutions: HashSet<Vec<usize>> = solver.find_all_satisfying(&sat).into_iter().collect();
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &sat,
+        &result,
+        "SAT->CircuitSAT single literal clause",
+    );
 
-    // Only solution should be x1=1, x2=1
-    assert_eq!(extracted, sat_solutions);
-    assert_eq!(sat_solutions.len(), 1);
-    assert!(sat_solutions.contains(&vec![1, 1]));
+    let target_solution = solve_satisfaction_problem(result.target_problem())
+        .expect("CircuitSAT should have a satisfying solution");
+    let extracted = result.extract_solution(&target_solution);
+    assert_eq!(extracted, vec![1, 1]);
 }
diff --git a/src/unit_tests/rules/sat_coloring.rs b/src/unit_tests/rules/sat_coloring.rs
index 7d7847b9c..0c058e24a 100644
--- a/src/unit_tests/rules/sat_coloring.rs
+++ b/src/unit_tests/rules/sat_coloring.rs
@@ -2,6 +2,7 @@ use super::*;
 use crate::models::formula::CNFClause;
 use crate::solvers::BruteForce;
 use crate::topology::Graph;
+use crate::traits::Problem;
 use crate::variant::K3;
 include!("../jl_helpers.rs");
 
@@ -328,8 +329,8 @@ fn test_jl_parity_sat_to_coloring() {
             .into_iter()
             .collect();
         assert!(
-            best_source.contains(&extracted),
-            "SAT->Coloring [{label}]: extracted not satisfying"
+            source.evaluate(&extracted),
+            "SAT->Coloring [{label}]: extracted assignment is not satisfying"
         );
         for case in data["cases"].as_array().unwrap() {
             assert_eq!(
diff --git a/src/unit_tests/rules/sat_ksat.rs b/src/unit_tests/rules/sat_ksat.rs
index c0bc63c08..0748038f3 100644
--- a/src/unit_tests/rules/sat_ksat.rs
+++ b/src/unit_tests/rules/sat_ksat.rs
@@ -1,4 +1,5 @@
 use super::*;
+use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target;
 use crate::solvers::BruteForce;
 use crate::traits::Problem;
 use crate::variant::K3;
@@ -130,10 +131,11 @@ fn test_sat_to_ksat_closed_loop() {
 
     // Extract solutions should map back correctly
     if ksat_satisfiable {
-        for ksat_sol in &ksat_solutions {
-            let sat_sol = reduction.extract_solution(ksat_sol);
-            assert_eq!(sat_sol.len(), 3); // Original variable count
-        }
+        assert_satisfaction_round_trip_from_satisfaction_target(
+            &sat,
+            &reduction,
+            "SAT->KSat closed loop",
+        );
     }
 }
 
@@ -285,14 +287,11 @@ fn test_mixed_clause_sizes() {
     }
 
     // Verify satisfiability is preserved - use find_all_satisfying for satisfaction problems
-    let solver = BruteForce::new();
-    let best_target = solver.find_all_satisfying(ksat);
-    let best_source: HashSet<Vec<usize>> = solver.find_all_satisfying(&sat).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| reduction.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &sat,
+        &reduction,
+        "SAT->KSat mixed clause sizes",
+    );
 }
 
 #[test]
@@ -325,14 +324,13 @@ fn test_jl_parity_sat_to_ksat() {
     let source = Satisfiability::new(num_vars, clauses);
     let result = ReduceTo::<KSatisfiability<K3>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_satisfying(result.target_problem());
     let best_source: HashSet<Vec<usize>> =
         solver.find_all_satisfying(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &result,
+        "JL parity SAT->KSat",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -351,14 +349,13 @@ fn test_jl_parity_ksat_to_sat() {
     let source = KSatisfiability::<K3>::new(num_vars, clauses);
     let result = ReduceTo::<Satisfiability>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_satisfying(result.target_problem());
     let best_source: HashSet<Vec<usize>> =
         solver.find_all_satisfying(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &result,
+        "JL parity KSat->SAT",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -377,14 +374,13 @@ fn test_jl_parity_rule_sat_to_ksat() {
     let source = Satisfiability::new(num_vars, clauses);
     let result = ReduceTo::<KSatisfiability<K3>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_satisfying(result.target_problem());
     let best_source: HashSet<Vec<usize>> =
         solver.find_all_satisfying(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &result,
+        "JL parity rule SAT->KSat",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
diff --git a/src/unit_tests/rules/sat_maximumindependentset.rs b/src/unit_tests/rules/sat_maximumindependentset.rs
index ce85a7eb5..bc4ba6af8 100644
--- a/src/unit_tests/rules/sat_maximumindependentset.rs
+++ b/src/unit_tests/rules/sat_maximumindependentset.rs
@@ -1,5 +1,8 @@
 use super::*;
 use crate::models::formula::CNFClause;
+use crate::rules::test_helpers::{
+    assert_satisfaction_round_trip_from_optimization_target, solve_optimization_problem,
+};
 use crate::solvers::BruteForce;
 use crate::topology::Graph;
 use crate::traits::Problem;
@@ -208,25 +211,22 @@ fn test_jl_parity_sat_to_independentset() {
         let source = Satisfiability::new(num_vars, clauses);
         let result = ReduceTo::<MaximumIndependentSet<SimpleGraph, One>>::reduce_to(&source);
         let solver = BruteForce::new();
-        let best_target = solver.find_all_best(result.target_problem());
-        let extracted: HashSet<Vec<usize>> = best_target
-            .iter()
-            .map(|t| result.extract_solution(t))
-            .collect();
         let sat_solutions: HashSet<Vec<usize>> =
             solver.find_all_satisfying(&source).into_iter().collect();
         for case in data["cases"].as_array().unwrap() {
             if sat_solutions.is_empty() {
-                for sol in &extracted {
-                    assert!(
-                        !source.evaluate(sol),
-                        "SAT->IS [{label}]: unsatisfiable but extracted satisfies"
-                    );
-                }
-            } else {
+                let target_solution = solve_optimization_problem(result.target_problem())
+                    .expect("SAT->IS: target should have an optimal solution");
+                let extracted = result.extract_solution(&target_solution);
                 assert!(
-                    extracted.is_subset(&sat_solutions),
-                    "SAT->IS [{label}]: extracted not subset"
+                    !source.evaluate(&extracted),
+                    "SAT->IS [{label}]: unsatisfiable but extracted satisfies"
+                );
+            } else {
+                assert_satisfaction_round_trip_from_optimization_target(
+                    &source,
+                    &result,
+                    &format!("SAT->IS [{label}]"),
                 );
                 assert_eq!(
                     sat_solutions,
diff --git a/src/unit_tests/rules/sat_minimumdominatingset.rs b/src/unit_tests/rules/sat_minimumdominatingset.rs
index 8627613b4..50902fda3 100644
--- a/src/unit_tests/rules/sat_minimumdominatingset.rs
+++ b/src/unit_tests/rules/sat_minimumdominatingset.rs
@@ -1,5 +1,8 @@
 use super::*;
 use crate::models::formula::CNFClause;
+use crate::rules::test_helpers::{
+    assert_satisfaction_round_trip_from_optimization_target, solve_optimization_problem,
+};
 use crate::solvers::BruteForce;
 use crate::topology::Graph;
 use crate::traits::Problem;
@@ -196,25 +199,22 @@ fn test_jl_parity_sat_to_dominatingset() {
         let source = Satisfiability::new(num_vars, clauses);
         let result = ReduceTo::<MinimumDominatingSet<SimpleGraph, i32>>::reduce_to(&source);
         let solver = BruteForce::new();
-        let best_target = solver.find_all_best(result.target_problem());
-        let extracted: HashSet<Vec<usize>> = best_target
-            .iter()
-            .map(|t| result.extract_solution(t))
-            .collect();
         let sat_solutions: HashSet<Vec<usize>> =
             solver.find_all_satisfying(&source).into_iter().collect();
         for case in data["cases"].as_array().unwrap() {
             if sat_solutions.is_empty() {
-                for sol in &extracted {
-                    assert!(
-                        !source.evaluate(sol),
-                        "SAT->DS [{label}]: unsatisfiable but extracted satisfies"
-                    );
-                }
-            } else {
+                let target_solution = solve_optimization_problem(result.target_problem())
+                    .expect("SAT->DS: target should have an optimal solution");
+                let extracted = result.extract_solution(&target_solution);
                 assert!(
-                    extracted.is_subset(&sat_solutions),
-                    "SAT->DS [{label}]: extracted not subset"
+                    !source.evaluate(&extracted),
+                    "SAT->DS [{label}]: unsatisfiable but extracted satisfies"
+                );
+            } else {
+                assert_satisfaction_round_trip_from_optimization_target(
+                    &source,
+                    &result,
+                    &format!("SAT->DS [{label}]"),
                 );
                 assert_eq!(
                     sat_solutions,
diff --git a/src/unit_tests/rules/spinglass_maxcut.rs b/src/unit_tests/rules/spinglass_maxcut.rs
index e24e17cb0..013bc4777 100644
--- a/src/unit_tests/rules/spinglass_maxcut.rs
+++ b/src/unit_tests/rules/spinglass_maxcut.rs
@@ -1,4 +1,5 @@
 use super::*;
+use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
 include!("../jl_helpers.rs");
 
@@ -96,13 +97,12 @@ fn test_jl_parity_spinglass_to_maxcut() {
     let source = SpinGlass::<SimpleGraph, i32>::new(nv, interactions, h_values);
     let result = ReduceTo::<MaxCut<SimpleGraph, i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity SpinGlass->MaxCut",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -124,13 +124,12 @@ fn test_jl_parity_maxcut_to_spinglass() {
     let source = MaxCut::new(SimpleGraph::new(nv, edges), weights);
     let result = ReduceTo::<SpinGlass<SimpleGraph, i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity MaxCut->SpinGlass",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -154,13 +153,12 @@ fn test_jl_parity_rule_maxcut_to_spinglass() {
     );
     let result = ReduceTo::<SpinGlass<SimpleGraph, i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity rule MaxCut->SpinGlass",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -183,13 +181,12 @@ fn test_jl_parity_rule_spinglass_to_maxcut() {
     let source = SpinGlass::<SimpleGraph, i32>::new(nv, interactions, h_values);
     let result = ReduceTo::<MaxCut<SimpleGraph, i32>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity rule SpinGlass->MaxCut",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
diff --git a/src/unit_tests/rules/spinglass_qubo.rs b/src/unit_tests/rules/spinglass_qubo.rs
index 5dd713965..633cb95b5 100644
--- a/src/unit_tests/rules/spinglass_qubo.rs
+++ b/src/unit_tests/rules/spinglass_qubo.rs
@@ -1,4 +1,5 @@
 use super::*;
+use crate::rules::test_helpers::assert_optimization_round_trip_from_optimization_target;
 use crate::solvers::BruteForce;
 use crate::traits::Problem;
 include!("../jl_helpers.rs");
@@ -83,13 +84,12 @@ fn test_jl_parity_spinglass_to_qubo() {
     let source = SpinGlass::<SimpleGraph, f64>::new(nv, interactions, h_values);
     let result = ReduceTo::<QUBO<f64>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity SpinGlass->QUBO",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -126,13 +126,12 @@ fn test_jl_parity_qubo_to_spinglass() {
     let source = QUBO::from_matrix(rust_matrix);
     let result = ReduceTo::<SpinGlass<SimpleGraph, f64>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity QUBO->SpinGlass",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }
@@ -170,13 +169,12 @@ fn test_jl_parity_rule_qubo_to_spinglass() {
     let source = QUBO::from_matrix(rust_matrix);
     let result = ReduceTo::<SpinGlass<SimpleGraph, f64>>::reduce_to(&source);
     let solver = BruteForce::new();
-    let best_target = solver.find_all_best(result.target_problem());
     let best_source: HashSet<Vec<usize>> = solver.find_all_best(&source).into_iter().collect();
-    let extracted: HashSet<Vec<usize>> = best_target
-        .iter()
-        .map(|t| result.extract_solution(t))
-        .collect();
-    assert!(extracted.is_subset(&best_source));
+    assert_optimization_round_trip_from_optimization_target(
+        &source,
+        &result,
+        "JL parity rule QUBO->SpinGlass",
+    );
     for case in data["cases"].as_array().unwrap() {
         assert_eq!(best_source, jl_parse_configs_set(&case["best_source"]));
     }