diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index b693e8e9..5cc9c9eb 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -16,7 +16,7 @@ make mdbook # Build and serve mdBook with live reload make paper # Build Typst paper (runs examples + exports first) make coverage # Generate coverage report (>95% required) make check # Quick pre-commit check (fmt + clippy + test) -make export-graph # Regenerate reduction graph JSON +make rust-export # Generate Rust mapping JSON exports make export-schemas # Regenerate problem schemas JSON make qubo-testdata # Regenerate QUBO ground truth JSON make clean # Clean build artifacts @@ -24,7 +24,7 @@ make clean # Clean build artifacts ## Verify Changes ```bash -make test clippy export-graph # Must pass before PR +make test clippy # Must pass before PR ``` ## Architecture @@ -47,7 +47,7 @@ make test clippy export-graph # Must pass before PR ``` Problem (core trait - all problems must implement) │ -├── const NAME: &'static str // Problem name, e.g., "IndependentSet" +├── const NAME: &'static str // Problem name, e.g., "MaximumIndependentSet" ├── type GraphType: GraphMarker // Graph topology marker ├── type Weight: NumericWeight // Weight type (i32, f64, Unweighted) ├── type Size // Objective value type @@ -75,20 +75,33 @@ ConstraintSatisfactionProblem : Problem (extension for CSPs) - Graph types: SimpleGraph, GridGraph, UnitDiskGraph, Hypergraph - Weight types: `Unweighted` (marker), `i32`, `f64` +### Problem Names +Problem types use explicit optimization prefixes: +- `MaximumIndependentSet`, `MaximumClique`, `MaximumMatching`, `MaximumSetPacking` +- `MinimumVertexCover`, `MinimumDominatingSet`, `MinimumSetCovering` +- No prefix: `MaxCut`, `SpinGlass`, `QUBO`, `ILP`, `Satisfiability`, `KSatisfiability`, `CircuitSAT`, `Factoring`, `MaximalIS` + ### Problem Variant IDs Reduction graph nodes use variant IDs: `ProblemName[/GraphType][/Weighted]` -- Base: `IndependentSet` (SimpleGraph, unweighted) -- Graph variant: `IndependentSet/GridGraph` -- Weighted variant: `IndependentSet/Weighted` -- Both: `IndependentSet/GridGraph/Weighted` +- Base: `MaximumIndependentSet` (SimpleGraph, unweighted) +- Graph variant: `MaximumIndependentSet/GridGraph` +- Weighted variant: `MaximumIndependentSet/Weighted` +- Both: `MaximumIndependentSet/GridGraph/Weighted` ## Conventions ### File Naming -- Reduction files: `src/rules/_.rs` -- Model files: `src/models//.rs` +- Reduction files: `src/rules/_.rs` (e.g., `maximumindependentset_qubo.rs`) +- Model files: `src/models//.rs` (e.g., `maximum_independent_set.rs`) +- Example files: `examples/reduction__to_.rs` - Test naming: `test__to__closed_loop` +### Paper (docs/paper/reductions.typ) +- `problem-def(name, title, body)` — defines a problem with auto-generated schema, reductions list, and label `` +- `reduction-rule(source, target, ...)` — generates a theorem with label `` and registers in `covered-rules` state +- Completeness warnings auto-check that all JSON graph nodes/edges are covered in the paper +- `display-name` dict maps `ProblemName` to display text + ## Contributing See `.claude/rules/` for detailed guides: - `adding-reductions.md` - How to add reduction rules diff --git a/.claude/rules/adding-models.md b/.claude/rules/adding-models.md index 4088da2c..fd98a957 100644 --- a/.claude/rules/adding-models.md +++ b/.claude/rules/adding-models.md @@ -36,9 +36,9 @@ pub use my_problem::MyProblem; ## 3. Categories Place models in appropriate category: -- `src/models/satisfiability/` - SAT, K-SAT, CircuitSAT -- `src/models/graph/` - IndependentSet, VertexCovering, Coloring, etc. -- `src/models/set/` - SetCovering, SetPacking +- `src/models/satisfiability/` - Satisfiability, KSatisfiability, CircuitSAT +- `src/models/graph/` - MaximumIndependentSet, MinimumVertexCover, KColoring, etc. +- `src/models/set/` - MinimumSetCovering, MaximumSetPacking - `src/models/optimization/` - SpinGlass, QUBO, ILP ## 4. Required Traits @@ -47,8 +47,11 @@ Place models in appropriate category: - `Problem` - Core trait with `num_variables()`, `problem_size()`, `is_valid_solution()` - Consider `ConstraintSatisfactionProblem` if applicable -## 5. Documentation -Document in `docs/paper/reductions.typ` +## 5. Naming +Use explicit optimization prefixes: `Maximum` for maximization, `Minimum` for minimization (e.g., `MaximumIndependentSet`, `MinimumVertexCover`). + +## 6. Documentation +Document in `docs/paper/reductions.typ` using `#problem-def("ProblemName", "Display Title")[...]` ## Anti-patterns - Don't create models without JSON serialization support diff --git a/.claude/rules/adding-reductions.md b/.claude/rules/adding-reductions.md index 20411ac8..b92664b5 100644 --- a/.claude/rules/adding-reductions.md +++ b/.claude/rules/adding-reductions.md @@ -20,7 +20,7 @@ Before writing any Rust code, follow this workflow: # Example: generate QUBO test data cd scripts && uv run python generate_qubo_tests.py ``` -3. **Create a practical example** — design a small, explainable instance for `examples/` (e.g., "wireless tower placement" for IndependentSet, "map coloring" for Coloring). This example will also appear in the `docs/paper/reductions.typ`. +3. **Create a practical example** — design a small, explainable instance for `examples/` (e.g., "wireless tower placement" for MaximumIndependentSet, "map coloring" for KColoring). This example will also appear in the `docs/paper/reductions.typ`. 4. **Write the implementation plan** — save to `docs/plans/` using `superpowers:writing-plans`. The plan must include implementation details from the brainstorming session (formulas, penalty terms, matrix construction, variable indexing). ## 1. Implementation @@ -84,9 +84,9 @@ Add a round-trip demo to `examples/` showing a practical, explainable instance: ## 4. Documentation Update `docs/paper/reductions.typ` (see `rules/documentation.md` for the pattern): -- Add theorem + proof sketch +- Add `reduction-rule("Source", "Target", ...)` theorem with proof sketch - Add Rust code example from the example program -- Add to summary table with overhead and citation +- Add `display-name` entry if the problem is new The goal is to 1. prove the correctness of the reduction to human beings. 2. provide a minimal working example to the readers. diff --git a/.claude/rules/documentation.md b/.claude/rules/documentation.md index 7cabfe0b..d29234c4 100644 --- a/.claude/rules/documentation.md +++ b/.claude/rules/documentation.md @@ -7,34 +7,48 @@ paths: The technical paper (`docs/paper/reductions.typ`) must include: -1. **Table of Contents** - Auto-generated outline of all sections -2. **Problem Data Structures** - Rust struct with fields in a code block -3. **Reduction Examples** - Minimal working example showing reduce → solve → extract +1. **Problem Definitions** — using `problem-def` wrapper +2. **Reduction Theorems** — using `reduction-rule` function +3. **Reduction Examples** — minimal working example showing reduce → solve → extract -## Pattern +## Adding a Problem Definition ```typst -#definition("Problem Name")[ +#problem-def("MaximumIndependentSet", "Maximum Independent Set (MIS)")[ Mathematical definition... ] +``` -// Rust data structure -```rust -pub struct ProblemName { - field1: Type1, - field2: Type2, -} -`` ` +This auto-generates: +- A label `` for cross-references +- The problem's schema (fields from Rust struct) +- The list of available reductions -#theorem[ - *(Source → Target)* Reduction description... -] +Also add an entry to the `display-name` dictionary: +```typst +"MaximumIndependentSet": "MIS", +``` + +## Adding a Reduction Theorem -// Minimal working example from closed-loop tests -```rust -let source = SourceProblem::new(...); -let reduction = ReduceTo::::reduce_to(&source); -let target = reduction.target_problem(); -// ... solve and extract -`` ` +```typst +#reduction-rule( + "MaximumIndependentSet", "QUBO", + example: "maximumindependentset_to_qubo", + overhead: (n: 0, m: 1), +)[ + Proof sketch... +] ``` + +This auto-generates: +- A theorem label `` +- References to source/target problem definitions (if they exist) +- Registration in `covered-rules` state for completeness checking +- The example code block from `examples/reduction_.rs` + +## Completeness Warnings + +The paper auto-checks completeness: +- After Problem Definitions: warns if JSON graph nodes are missing from `display-name` +- After Reductions section: warns if JSON graph edges are missing from `covered-rules` diff --git a/Makefile b/Makefile index 6e364f55..6b04e05d 100644 --- a/Makefile +++ b/Makefile @@ -51,14 +51,18 @@ doc: rm -rf docs/book/api cp -r target/doc docs/book/api -# Build and serve mdBook with live reload +# Build and serve mdBook with API docs mdbook: cargo run --example export_graph cp docs/paper/reduction_graph.json docs/src/reductions/ cargo doc --all-features --no-deps - rm -rf docs/book/api - cp -r target/doc docs/book/api - mdbook serve docs --open + mdbook build + rm -rf book/api + cp -r target/doc book/api + @-fuser -k 3001/tcp 2>/dev/null || true + @echo "Serving at http://localhost:3001" + python3 -m http.server 3001 -d book & + @sleep 1 && xdg-open http://localhost:3001 # Generate all example JSON files for the paper REDUCTION_EXAMPLES := $(patsubst examples/%.rs,%,$(wildcard examples/reduction_*.rs)) diff --git a/benches/solver_benchmarks.rs b/benches/solver_benchmarks.rs index bd2abf2b..b0a6e719 100644 --- a/benches/solver_benchmarks.rs +++ b/benches/solver_benchmarks.rs @@ -9,14 +9,14 @@ use problemreductions::models::set::*; use problemreductions::models::specialized::*; use problemreductions::prelude::*; -/// Benchmark IndependentSet on graphs of varying sizes. +/// Benchmark MaximumIndependentSet on graphs of varying sizes. fn bench_independent_set(c: &mut Criterion) { - let mut group = c.benchmark_group("IndependentSet"); + let mut group = c.benchmark_group("MaximumIndependentSet"); for n in [4, 6, 8, 10].iter() { // Create a path graph with n vertices let edges: Vec<(usize, usize)> = (0..*n - 1).map(|i| (i, i + 1)).collect(); - let problem = IndependentSet::::new(*n, edges); + let problem = MaximumIndependentSet::::new(*n, edges); let solver = BruteForce::new(); group.bench_with_input(BenchmarkId::new("path", n), n, |b, _| { @@ -27,13 +27,13 @@ fn bench_independent_set(c: &mut Criterion) { group.finish(); } -/// Benchmark VertexCovering on graphs of varying sizes. +/// Benchmark MinimumVertexCover on graphs of varying sizes. fn bench_vertex_covering(c: &mut Criterion) { - let mut group = c.benchmark_group("VertexCovering"); + let mut group = c.benchmark_group("MinimumVertexCover"); for n in [4, 6, 8, 10].iter() { let edges: Vec<(usize, usize)> = (0..*n - 1).map(|i| (i, i + 1)).collect(); - let problem = VertexCovering::::new(*n, edges); + let problem = MinimumVertexCover::::new(*n, edges); let solver = BruteForce::new(); group.bench_with_input(BenchmarkId::new("path", n), n, |b, _| { @@ -109,16 +109,16 @@ fn bench_spin_glass(c: &mut Criterion) { group.finish(); } -/// Benchmark SetCovering on varying sizes. +/// Benchmark MinimumSetCovering on varying sizes. fn bench_set_covering(c: &mut Criterion) { - let mut group = c.benchmark_group("SetCovering"); + let mut group = c.benchmark_group("MinimumSetCovering"); for num_sets in [4, 6, 8, 10].iter() { // Create overlapping sets let sets: Vec> = (0..*num_sets) .map(|i| vec![i, (i + 1) % *num_sets, (i + 2) % *num_sets]) .collect(); - let problem = SetCovering::::new(*num_sets, sets); + let problem = MinimumSetCovering::::new(*num_sets, sets); let solver = BruteForce::new(); group.bench_with_input( @@ -154,7 +154,7 @@ fn bench_matching(c: &mut Criterion) { for n in [4, 6, 8, 10].iter() { let edges: Vec<(usize, usize, i32)> = (0..*n - 1).map(|i| (i, i + 1, 1)).collect(); - let problem = Matching::new(*n, edges); + let problem = MaximumMatching::new(*n, edges); let solver = BruteForce::new(); group.bench_with_input(BenchmarkId::new("path", n), n, |b, _| { @@ -192,9 +192,9 @@ fn bench_comparison(c: &mut Criterion) { let solver = BruteForce::new(); - // IndependentSet with 8 vertices - let is_problem = IndependentSet::::new(8, vec![(0, 1), (2, 3), (4, 5), (6, 7)]); - group.bench_function("IndependentSet", |b| { + // MaximumIndependentSet with 8 vertices + let is_problem = MaximumIndependentSet::::new(8, vec![(0, 1), (2, 3), (4, 5), (6, 7)]); + group.bench_function("MaximumIndependentSet", |b| { b.iter(|| solver.find_best(black_box(&is_problem))) }); diff --git a/book.toml b/book.toml index 5d806f85..649f2e24 100644 --- a/book.toml +++ b/book.toml @@ -5,11 +5,8 @@ description = "A Rust library for reducing NP-hard problems" language = "en" src = "docs/src" -[preprocessor.mermaid] -command = "mdbook-mermaid" - [output.html] -default-theme = "rust" +default-theme = "navy" git-repository-url = "https://github.com/CodingThrust/problem-reductions" edit-url-template = "https://github.com/CodingThrust/problem-reductions/edit/main/{path}" additional-css = [] diff --git a/docs/paper/problem_schemas.json b/docs/paper/problem_schemas.json index 065c8bfa..1bb7e1a5 100644 --- a/docs/paper/problem_schemas.json +++ b/docs/paper/problem_schemas.json @@ -75,40 +75,6 @@ } ] }, - { - "name": "Clique", - "category": "graph", - "description": "Find maximum weight clique in a graph", - "fields": [ - { - "name": "graph", - "type_name": "G", - "description": "The underlying graph G=(V,E)" - }, - { - "name": "weights", - "type_name": "Vec", - "description": "Vertex weights w: V -> R" - } - ] - }, - { - "name": "DominatingSet", - "category": "graph", - "description": "Find minimum weight dominating set in a graph", - "fields": [ - { - "name": "graph", - "type_name": "G", - "description": "The underlying graph G=(V,E)" - }, - { - "name": "weights", - "type_name": "Vec", - "description": "Vertex weights w: V -> R" - } - ] - }, { "name": "Factoring", "category": "specialized", @@ -164,58 +130,109 @@ ] }, { - "name": "IndependentSet", + "name": "KColoring", "category": "graph", - "description": "Find maximum weight independent set in a graph", + "description": "Find valid k-coloring of a graph", "fields": [ { "name": "graph", "type_name": "G", "description": "The underlying graph G=(V,E)" + } + ] + }, + { + "name": "KSatisfiability", + "category": "satisfiability", + "description": "SAT with exactly k literals per clause", + "fields": [ + { + "name": "num_vars", + "type_name": "usize", + "description": "Number of Boolean variables" + }, + { + "name": "clauses", + "type_name": "Vec", + "description": "Clauses each with exactly K literals" }, { "name": "weights", "type_name": "Vec", - "description": "Vertex weights w: V -> R" + "description": "Clause weights for MAX-K-SAT" } ] }, { - "name": "KColoring", + "name": "MaxCut", "category": "graph", - "description": "Find valid k-coloring of a graph", + "description": "Find maximum weight cut in a graph", + "fields": [ + { + "name": "graph", + "type_name": "G", + "description": "The graph with edge weights" + }, + { + "name": "edge_weights", + "type_name": "Vec", + "description": "Edge weights w: E -> R" + } + ] + }, + { + "name": "MaximalIS", + "category": "graph", + "description": "Find maximum weight maximal independent set", "fields": [ { "name": "graph", "type_name": "G", "description": "The underlying graph G=(V,E)" + }, + { + "name": "weights", + "type_name": "Vec", + "description": "Vertex weights w: V -> R" } ] }, { - "name": "KSatisfiability", - "category": "satisfiability", - "description": "SAT with exactly k literals per clause", + "name": "MaximumClique", + "category": "graph", + "description": "Find maximum weight clique in a graph", "fields": [ { - "name": "num_vars", - "type_name": "usize", - "description": "Number of Boolean variables" + "name": "graph", + "type_name": "G", + "description": "The underlying graph G=(V,E)" }, { - "name": "clauses", - "type_name": "Vec", - "description": "Clauses each with exactly K literals" + "name": "weights", + "type_name": "Vec", + "description": "Vertex weights w: V -> R" + } + ] + }, + { + "name": "MaximumIndependentSet", + "category": "graph", + "description": "Find maximum weight independent set in a graph", + "fields": [ + { + "name": "graph", + "type_name": "G", + "description": "The underlying graph G=(V,E)" }, { "name": "weights", "type_name": "Vec", - "description": "Clause weights for MAX-K-SAT" + "description": "Vertex weights w: V -> R" } ] }, { - "name": "Matching", + "name": "MaximumMatching", "category": "graph", "description": "Find maximum weight matching in a graph", "fields": [ @@ -232,26 +249,65 @@ ] }, { - "name": "MaxCut", + "name": "MaximumSetPacking", + "category": "set", + "description": "Find maximum weight collection of disjoint sets", + "fields": [ + { + "name": "sets", + "type_name": "Vec>", + "description": "Collection of sets over a universe" + }, + { + "name": "weights", + "type_name": "Vec", + "description": "Weight for each set" + } + ] + }, + { + "name": "MinimumDominatingSet", "category": "graph", - "description": "Find maximum weight cut in a graph", + "description": "Find minimum weight dominating set in a graph", "fields": [ { "name": "graph", "type_name": "G", - "description": "The graph with edge weights" + "description": "The underlying graph G=(V,E)" }, { - "name": "edge_weights", + "name": "weights", "type_name": "Vec", - "description": "Edge weights w: E -> R" + "description": "Vertex weights w: V -> R" } ] }, { - "name": "MaximalIS", + "name": "MinimumSetCovering", + "category": "set", + "description": "Find minimum weight collection covering the universe", + "fields": [ + { + "name": "universe_size", + "type_name": "usize", + "description": "Size of the universe U" + }, + { + "name": "sets", + "type_name": "Vec>", + "description": "Collection of subsets of U" + }, + { + "name": "weights", + "type_name": "Vec", + "description": "Weight for each set" + } + ] + }, + { + "name": "MinimumVertexCover", "category": "graph", - "description": "Find maximum weight maximal independent set", + "description": "Find minimum weight vertex cover in a graph", "fields": [ { "name": "graph", @@ -331,45 +387,6 @@ } ] }, - { - "name": "SetCovering", - "category": "set", - "description": "Find minimum weight collection covering the universe", - "fields": [ - { - "name": "universe_size", - "type_name": "usize", - "description": "Size of the universe U" - }, - { - "name": "sets", - "type_name": "Vec>", - "description": "Collection of subsets of U" - }, - { - "name": "weights", - "type_name": "Vec", - "description": "Weight for each set" - } - ] - }, - { - "name": "SetPacking", - "category": "set", - "description": "Find maximum weight collection of disjoint sets", - "fields": [ - { - "name": "sets", - "type_name": "Vec>", - "description": "Collection of sets over a universe" - }, - { - "name": "weights", - "type_name": "Vec", - "description": "Weight for each set" - } - ] - }, { "name": "SpinGlass", "category": "optimization", @@ -391,22 +408,5 @@ "description": "On-site fields h_i" } ] - }, - { - "name": "VertexCovering", - "category": "graph", - "description": "Find minimum weight vertex cover in a graph", - "fields": [ - { - "name": "graph", - "type_name": "G", - "description": "The underlying graph G=(V,E)" - }, - { - "name": "weights", - "type_name": "Vec", - "description": "Vertex weights w: V -> R" - } - ] } ] \ No newline at end of file diff --git a/docs/paper/reduction_graph.json b/docs/paper/reduction_graph.json index 1e7fd7f1..d05d9f2b 100644 --- a/docs/paper/reduction_graph.json +++ b/docs/paper/reduction_graph.json @@ -24,21 +24,6 @@ "category": "satisfiability", "doc_path": "models/specialized/struct.CircuitSAT.html" }, - { - "name": "DominatingSet", - "variant": {}, - "category": "graph", - "doc_path": "models/graph/struct.DominatingSet.html" - }, - { - "name": "DominatingSet", - "variant": { - "graph": "SimpleGraph", - "weight": "Unweighted" - }, - "category": "graph", - "doc_path": "models/graph/struct.DominatingSet.html" - }, { "name": "Factoring", "variant": {}, @@ -69,30 +54,6 @@ "category": "optimization", "doc_path": "models/optimization/struct.ILP.html" }, - { - "name": "IndependentSet", - "variant": {}, - "category": "graph", - "doc_path": "models/graph/struct.IndependentSet.html" - }, - { - "name": "IndependentSet", - "variant": { - "graph": "SimpleGraph", - "weight": "Unweighted" - }, - "category": "graph", - "doc_path": "models/graph/struct.IndependentSet.html" - }, - { - "name": "IndependentSet", - "variant": { - "graph": "SimpleGraph", - "weight": "i32" - }, - "category": "graph", - "doc_path": "models/graph/struct.IndependentSet.html" - }, { "name": "KColoring", "variant": {}, @@ -152,151 +113,190 @@ "doc_path": "models/satisfiability/struct.KSatisfiability.html" }, { - "name": "Matching", + "name": "MaxCut", "variant": {}, "category": "graph", - "doc_path": "models/graph/struct.Matching.html" + "doc_path": "models/graph/struct.MaxCut.html" }, { - "name": "Matching", + "name": "MaxCut", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" }, "category": "graph", - "doc_path": "models/graph/struct.Matching.html" + "doc_path": "models/graph/struct.MaxCut.html" }, { - "name": "MaxCut", + "name": "MaximumIndependentSet", "variant": {}, "category": "graph", - "doc_path": "models/graph/struct.MaxCut.html" + "doc_path": "models/graph/struct.MaximumIndependentSet.html" }, { - "name": "MaxCut", + "name": "MaximumIndependentSet", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" }, "category": "graph", - "doc_path": "models/graph/struct.MaxCut.html" + "doc_path": "models/graph/struct.MaximumIndependentSet.html" }, { - "name": "QUBO", - "variant": {}, - "category": "optimization", - "doc_path": "models/optimization/struct.QUBO.html" - }, - { - "name": "QUBO", + "name": "MaximumIndependentSet", "variant": { "graph": "SimpleGraph", - "weight": "f64" + "weight": "i32" }, - "category": "optimization", - "doc_path": "models/optimization/struct.QUBO.html" + "category": "graph", + "doc_path": "models/graph/struct.MaximumIndependentSet.html" }, { - "name": "Satisfiability", + "name": "MaximumMatching", "variant": {}, - "category": "satisfiability", - "doc_path": "models/satisfiability/struct.Satisfiability.html" + "category": "graph", + "doc_path": "models/graph/struct.MaximumMatching.html" }, { - "name": "Satisfiability", + "name": "MaximumMatching", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" }, - "category": "satisfiability", - "doc_path": "models/satisfiability/struct.Satisfiability.html" + "category": "graph", + "doc_path": "models/graph/struct.MaximumMatching.html" }, { - "name": "SetCovering", + "name": "MaximumSetPacking", "variant": {}, "category": "set", - "doc_path": "models/set/struct.SetCovering.html" + "doc_path": "models/set/struct.MaximumSetPacking.html" }, { - "name": "SetCovering", + "name": "MaximumSetPacking", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" }, "category": "set", - "doc_path": "models/set/struct.SetCovering.html" + "doc_path": "models/set/struct.MaximumSetPacking.html" }, { - "name": "SetPacking", - "variant": {}, + "name": "MaximumSetPacking", + "variant": { + "graph": "SimpleGraph", + "weight": "i32" + }, "category": "set", - "doc_path": "models/set/struct.SetPacking.html" + "doc_path": "models/set/struct.MaximumSetPacking.html" + }, + { + "name": "MinimumDominatingSet", + "variant": {}, + "category": "graph", + "doc_path": "models/graph/struct.MinimumDominatingSet.html" }, { - "name": "SetPacking", + "name": "MinimumDominatingSet", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" }, + "category": "graph", + "doc_path": "models/graph/struct.MinimumDominatingSet.html" + }, + { + "name": "MinimumSetCovering", + "variant": {}, "category": "set", - "doc_path": "models/set/struct.SetPacking.html" + "doc_path": "models/set/struct.MinimumSetCovering.html" }, { - "name": "SetPacking", + "name": "MinimumSetCovering", "variant": { "graph": "SimpleGraph", - "weight": "i32" + "weight": "Unweighted" }, "category": "set", - "doc_path": "models/set/struct.SetPacking.html" + "doc_path": "models/set/struct.MinimumSetCovering.html" }, { - "name": "SpinGlass", + "name": "MinimumVertexCover", "variant": {}, - "category": "optimization", - "doc_path": "models/optimization/struct.SpinGlass.html" + "category": "graph", + "doc_path": "models/graph/struct.MinimumVertexCover.html" }, { - "name": "SpinGlass", + "name": "MinimumVertexCover", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" }, + "category": "graph", + "doc_path": "models/graph/struct.MinimumVertexCover.html" + }, + { + "name": "MinimumVertexCover", + "variant": { + "graph": "SimpleGraph", + "weight": "i32" + }, + "category": "graph", + "doc_path": "models/graph/struct.MinimumVertexCover.html" + }, + { + "name": "QUBO", + "variant": {}, "category": "optimization", - "doc_path": "models/optimization/struct.SpinGlass.html" + "doc_path": "models/optimization/struct.QUBO.html" }, { - "name": "SpinGlass", + "name": "QUBO", "variant": { "graph": "SimpleGraph", "weight": "f64" }, "category": "optimization", - "doc_path": "models/optimization/struct.SpinGlass.html" + "doc_path": "models/optimization/struct.QUBO.html" }, { - "name": "VertexCovering", + "name": "Satisfiability", "variant": {}, - "category": "graph", - "doc_path": "models/graph/struct.VertexCovering.html" + "category": "satisfiability", + "doc_path": "models/satisfiability/struct.Satisfiability.html" }, { - "name": "VertexCovering", + "name": "Satisfiability", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" }, - "category": "graph", - "doc_path": "models/graph/struct.VertexCovering.html" + "category": "satisfiability", + "doc_path": "models/satisfiability/struct.Satisfiability.html" + }, + { + "name": "SpinGlass", + "variant": {}, + "category": "optimization", + "doc_path": "models/optimization/struct.SpinGlass.html" }, { - "name": "VertexCovering", + "name": "SpinGlass", "variant": { "graph": "SimpleGraph", - "weight": "i32" + "weight": "Unweighted" }, - "category": "graph", - "doc_path": "models/graph/struct.VertexCovering.html" + "category": "optimization", + "doc_path": "models/optimization/struct.SpinGlass.html" + }, + { + "name": "SpinGlass", + "variant": { + "graph": "SimpleGraph", + "weight": "f64" + }, + "category": "optimization", + "doc_path": "models/optimization/struct.SpinGlass.html" } ], "edges": [ @@ -315,7 +315,18 @@ "weight": "Unweighted" } }, - "bidirectional": false + "bidirectional": false, + "overhead": [ + { + "field": "num_spins", + "formula": "num_assignments" + }, + { + "field": "num_interactions", + "formula": "num_assignments" + } + ], + "doc_path": "rules/circuit_spinglass/index.html" }, { "source": { @@ -332,7 +343,14 @@ "weight": "i32" } }, - "bidirectional": false + "bidirectional": false, + "overhead": [ + { + "field": "num_gates", + "formula": "num_bits_first * num_bits_second" + } + ], + "doc_path": "rules/factoring_circuit/index.html" }, { "source": { @@ -349,7 +367,18 @@ "weight": "Unweighted" } }, - "bidirectional": false + "bidirectional": false, + "overhead": [ + { + "field": "num_vars", + "formula": "2 * num_bits_first + 2 * num_bits_second + num_bits_first * num_bits_second" + }, + { + "field": "num_constraints", + "formula": "3 * num_bits_first * num_bits_second + num_bits_first + num_bits_second + 1" + } + ], + "doc_path": "rules/factoring_ilp/index.html" }, { "source": { @@ -366,49 +395,74 @@ "weight": "f64" } }, - "bidirectional": false + "bidirectional": false, + "overhead": [ + { + "field": "num_vars", + "formula": "num_vars" + } + ], + "doc_path": "rules/ilp_qubo/index.html" }, { "source": { - "name": "IndependentSet", + "name": "KColoring", "variant": { "graph": "SimpleGraph", + "k": "N", "weight": "i32" } }, "target": { - "name": "QUBO", + "name": "ILP", "variant": { "graph": "SimpleGraph", - "weight": "f64" + "weight": "Unweighted" } }, - "bidirectional": false + "bidirectional": false, + "overhead": [ + { + "field": "num_vars", + "formula": "num_vertices * num_colors" + }, + { + "field": "num_constraints", + "formula": "num_vertices + num_edges * num_colors" + } + ], + "doc_path": "rules/coloring_ilp/index.html" }, { "source": { "name": "KColoring", "variant": { "graph": "SimpleGraph", - "k": "N", - "weight": "i32" + "weight": "Unweighted" } }, "target": { - "name": "ILP", + "name": "QUBO", "variant": { "graph": "SimpleGraph", - "weight": "Unweighted" + "weight": "f64" } }, - "bidirectional": false + "bidirectional": false, + "overhead": [ + { + "field": "num_vars", + "formula": "num_vertices * num_colors" + } + ], + "doc_path": "rules/coloring_qubo/index.html" }, { "source": { - "name": "KColoring", + "name": "KSatisfiability", "variant": { "graph": "SimpleGraph", - "weight": "Unweighted" + "weight": "i32" } }, "target": { @@ -418,11 +472,18 @@ "weight": "f64" } }, - "bidirectional": false + "bidirectional": false, + "overhead": [ + { + "field": "num_vars", + "formula": "num_vars" + } + ], + "doc_path": "rules/ksatisfiability_qubo/index.html" }, { "source": { - "name": "KSatisfiability", + "name": "MaximumIndependentSet", "variant": { "graph": "SimpleGraph", "weight": "i32" @@ -435,201 +496,321 @@ "weight": "f64" } }, - "bidirectional": false + "bidirectional": false, + "overhead": [ + { + "field": "num_vars", + "formula": "num_vertices" + } + ], + "doc_path": "rules/maximumindependentset_qubo/index.html" }, { "source": { - "name": "Matching", + "name": "MaximumMatching", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, "target": { - "name": "SetPacking", + "name": "MaximumSetPacking", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, - "bidirectional": false + "bidirectional": false, + "overhead": [ + { + "field": "num_sets", + "formula": "num_edges" + }, + { + "field": "num_elements", + "formula": "num_vertices" + } + ], + "doc_path": "rules/maximummatching_maximumsetpacking/index.html" }, { "source": { - "name": "Satisfiability", + "name": "MaximumSetPacking", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, "target": { - "name": "DominatingSet", + "name": "MaximumIndependentSet", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, - "bidirectional": false + "bidirectional": true, + "overhead": [ + { + "field": "num_vertices", + "formula": "num_sets" + }, + { + "field": "num_edges", + "formula": "num_sets" + } + ], + "doc_path": "rules/maximumindependentset_maximumsetpacking/index.html" }, { "source": { - "name": "Satisfiability", + "name": "MaximumSetPacking", "variant": { "graph": "SimpleGraph", - "weight": "Unweighted" + "weight": "i32" } }, "target": { - "name": "IndependentSet", + "name": "QUBO", "variant": { "graph": "SimpleGraph", - "weight": "Unweighted" + "weight": "f64" } }, - "bidirectional": false + "bidirectional": false, + "overhead": [ + { + "field": "num_vars", + "formula": "num_sets" + } + ], + "doc_path": "rules/maximumsetpacking_qubo/index.html" }, { "source": { - "name": "Satisfiability", + "name": "MinimumVertexCover", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, "target": { - "name": "KColoring", + "name": "MaximumIndependentSet", "variant": { "graph": "SimpleGraph", - "weight": "i32" + "weight": "Unweighted" } }, - "bidirectional": false + "bidirectional": true, + "overhead": [ + { + "field": "num_vertices", + "formula": "num_vertices" + }, + { + "field": "num_edges", + "formula": "num_edges" + } + ], + "doc_path": "rules/minimumvertexcover_maximumindependentset/index.html" }, { "source": { - "name": "Satisfiability", + "name": "MinimumVertexCover", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, "target": { - "name": "KSatisfiability", + "name": "MinimumSetCovering", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, - "bidirectional": true + "bidirectional": false, + "overhead": [ + { + "field": "num_sets", + "formula": "num_vertices" + }, + { + "field": "num_elements", + "formula": "num_edges" + } + ], + "doc_path": "rules/minimumvertexcover_minimumsetcovering/index.html" }, { "source": { - "name": "SetPacking", + "name": "MinimumVertexCover", "variant": { "graph": "SimpleGraph", - "weight": "Unweighted" + "weight": "i32" } }, "target": { - "name": "IndependentSet", + "name": "QUBO", "variant": { "graph": "SimpleGraph", - "weight": "Unweighted" + "weight": "f64" } }, - "bidirectional": true + "bidirectional": false, + "overhead": [ + { + "field": "num_vars", + "formula": "num_vertices" + } + ], + "doc_path": "rules/minimumvertexcover_qubo/index.html" }, { "source": { - "name": "SetPacking", + "name": "Satisfiability", "variant": { "graph": "SimpleGraph", - "weight": "i32" + "weight": "Unweighted" } }, "target": { - "name": "QUBO", + "name": "KColoring", "variant": { "graph": "SimpleGraph", - "weight": "f64" + "weight": "i32" } }, - "bidirectional": false + "bidirectional": false, + "overhead": [ + { + "field": "num_vertices", + "formula": "2 * num_vars + 5 * num_literals - 5 * num_clauses + 3" + }, + { + "field": "num_colors", + "formula": "3" + } + ], + "doc_path": "rules/sat_coloring/index.html" }, { "source": { - "name": "SpinGlass", + "name": "Satisfiability", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, "target": { - "name": "MaxCut", + "name": "KSatisfiability", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, - "bidirectional": true + "bidirectional": true, + "overhead": [ + { + "field": "num_clauses", + "formula": "num_clauses + num_literals" + }, + { + "field": "num_vars", + "formula": "num_vars + num_literals" + } + ], + "doc_path": "rules/sat_ksat/index.html" }, { "source": { - "name": "SpinGlass", + "name": "Satisfiability", "variant": { "graph": "SimpleGraph", - "weight": "f64" + "weight": "Unweighted" } }, "target": { - "name": "QUBO", + "name": "MaximumIndependentSet", "variant": { "graph": "SimpleGraph", - "weight": "f64" + "weight": "Unweighted" } }, - "bidirectional": true + "bidirectional": false, + "overhead": [ + { + "field": "num_vertices", + "formula": "num_literals" + }, + { + "field": "num_edges", + "formula": "num_literals^2" + } + ], + "doc_path": "rules/sat_maximumindependentset/index.html" }, { "source": { - "name": "VertexCovering", + "name": "Satisfiability", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, "target": { - "name": "IndependentSet", + "name": "MinimumDominatingSet", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, - "bidirectional": true + "bidirectional": false, + "overhead": [ + { + "field": "num_vertices", + "formula": "3 * num_vars + num_clauses" + }, + { + "field": "num_edges", + "formula": "3 * num_vars + num_literals" + } + ], + "doc_path": "rules/sat_minimumdominatingset/index.html" }, { "source": { - "name": "VertexCovering", + "name": "SpinGlass", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, "target": { - "name": "SetCovering", + "name": "MaxCut", "variant": { "graph": "SimpleGraph", "weight": "Unweighted" } }, - "bidirectional": false + "bidirectional": true, + "overhead": [ + { + "field": "num_vertices", + "formula": "num_spins" + }, + { + "field": "num_edges", + "formula": "num_interactions" + } + ], + "doc_path": "rules/spinglass_maxcut/index.html" }, { "source": { - "name": "VertexCovering", + "name": "SpinGlass", "variant": { "graph": "SimpleGraph", - "weight": "i32" + "weight": "f64" } }, "target": { @@ -639,7 +820,14 @@ "weight": "f64" } }, - "bidirectional": false + "bidirectional": true, + "overhead": [ + { + "field": "num_vars", + "formula": "num_spins" + } + ], + "doc_path": "rules/spinglass_qubo/index.html" } ] } \ No newline at end of file diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index b4b4b794..d83a5fa0 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -23,31 +23,103 @@ #let problem-schemas = json("problem_schemas.json") -// Render a problem's Rust struct from the JSON schema -#let render-struct(name) = { - let schema = problem-schemas.find(s => s.name == name) - if schema == none { return } - let s = schema - let fields = s.fields.map(f => " " + f.name + ": " + f.type_name + ",").join("\n") - raw("pub struct " + name + " {\n" + fields + "\n}", lang: "rust", block: true) +// Problem display names for theorem headers +#let display-name = ( + "MaximumIndependentSet": [Maximum Independent Set], + "MinimumVertexCover": [Minimum Vertex Cover], + "MaxCut": [Max-Cut], + "KColoring": [$k$-Coloring], + "MinimumDominatingSet": [Minimum Dominating Set], + "MaximumMatching": [Maximum Matching], + "MaximumClique": [Maximum Clique], + "MaximumSetPacking": [Maximum Set Packing], + "MinimumSetCovering": [Minimum Set Covering], + "SpinGlass": [Spin Glass], + "QUBO": [QUBO], + "ILP": [Integer Linear Programming], + "Satisfiability": [SAT], + "KSatisfiability": [$k$-SAT], + "CircuitSAT": [CircuitSAT], + "Factoring": [Factoring], + "GridGraph": [GridGraph MIS], +) + +// Definition label: "def:" — each definition block must have a matching label + + +// Generate theorem label from source/target names (uses full names for consistency) +#let reduction-label(source, target) = { + label("thm:" + source + "-to-" + target) +} + +// State for tracking which reduction rules are described in the paper +#let covered-rules = state("covered-rules", ()) + +// Extract reductions for a problem from graph-data (returns (name, label) pairs) +#let get-reductions-to(problem-name) = { + graph-data.edges + .filter(e => e.source.name == problem-name) + .map(e => (name: e.target.name, lbl: reduction-label(e.source.name, e.target.name))) + .dedup(key: e => e.name) +} + +#let get-reductions-from(problem-name) = { + graph-data.edges + .filter(e => e.target.name == problem-name) + .map(e => (name: e.source.name, lbl: reduction-label(e.source.name, e.target.name))) + .dedup(key: e => e.name) +} + +// Render a single reduction with link +#let render-reduction-link(r) = { + link(r.lbl)[#r.name] +} + +// Render the "Reduces to/from" lines for a problem +#let render-reductions(problem-name) = { + let reduces-to = get-reductions-to(problem-name) + let reduces-from = get-reductions-from(problem-name) + if reduces-to.len() > 0 or reduces-from.len() > 0 { + block(above: 0.5em)[ + #set text(size: 9pt) + #if reduces-to.len() > 0 [ + - Reduces to: #reduces-to.map(render-reduction-link).join(", "). \ + ] + #if reduces-from.len() > 0 [ + - Reduces from: #reduces-from.map(render-reduction-link).join(", "). + ] + ] + } } -// Extract primary variable count from an instance dict. -#let instance-vars(inst) = { - if "num_variables" in inst { inst.num_variables } - else if "num_vertices" in inst { inst.num_vertices } - else if "num_vars" in inst { inst.num_vars } - else if "num_sets" in inst { inst.num_sets } - else if "num_spins" in inst { inst.num_spins } - else if "num_gates" in inst { inst.num_gates } - else if "num_bits_first" in inst and "num_bits_second" in inst { inst.num_bits_first + inst.num_bits_second } - else { 0 } +// Render a problem's JSON schema as a field table (subtle styling) +#let render-schema(name) = { + let schema = problem-schemas.find(s => s.name == name) + if schema == none { return } + block( + stroke: (left: 2pt + luma(180)), + inset: (left: 8pt), + )[ + #set text(size: 9pt) + #table( + columns: (auto, 1fr), + inset: (x: 2pt, y: 3pt), + align: (left, left), + stroke: none, + table.header( + text(fill: luma(30), raw(name)), + ), + table.hline(stroke: 0.3pt + luma(200)), + ..schema.fields.map(f => ( + text(fill: luma(60), raw(f.name)), + text(fill: luma(60), raw(f.description)) + )).flatten() + ) + ] } // Render a concrete example box from JSON data (unified schema) #let reduction-example(data, caption: none, body) = { - let src-vars = instance-vars(data.source.instance) - let tgt-vars = instance-vars(data.target.instance) block( width: 100%, inset: (x: 1em, y: 0.8em), @@ -55,18 +127,17 @@ stroke: (left: 2pt + rgb("#4a86e8")), )[ #if caption != none { - text(weight: "bold")[Concrete Example: #caption] + text(weight: "bold")[Example: #caption] parbreak() } - *Source:* #data.source.problem with #src-vars variables + *Source:* #data.source.problem #h(1em) - *Target:* #data.target.problem with #tgt-vars variables \ - *Overhead:* #if src-vars > 0 and tgt-vars > 0 [#calc.round(tgt-vars / src-vars, digits: 1)x variable growth] else [—] + *Target:* #data.target.problem #if body != none { parbreak(); body } ] } -#let theorem = thmplain("theorem", "Theorem", base_level: 1) +#let theorem = thmplain("theorem", [#h(-1.2em)Rule], base_level: 1) #let proof = thmproof("proof", "Proof") #let definition = thmbox( "definition", @@ -77,6 +148,86 @@ base_level: 1, ) +// Problem definition wrapper: auto-adds schema, reductions list, and label +#let problem-def(name, body) = { + let lbl = label("def:" + name) + let title = display-name.at(name) + [#definition(title)[ + #body + #render-schema(name) + #render-reductions(name) + ] #lbl] +} + +// Find edge in graph-data by source/target names +#let find-edge(source, target) = { + let edge = graph-data.edges.find(e => e.source.name == source and e.target.name == target) + if edge == none { + edge = graph-data.edges.find(e => e.source.name == target and e.target.name == source) + } + edge +} + +// Build display name from a graph-data node (name + variant) +#let variant-display(node) = { + let base = display-name.at(node.name) + if node.variant.len() == 0 { return base } + let parts = () + if "graph" in node.variant and node.variant.graph != "SimpleGraph" { + parts.push(node.variant.graph) + } + if "weight" in node.variant { + if node.variant.weight == "i32" { parts.push("weighted") } + else if node.variant.weight == "f64" { parts.push("real-weighted") } + } + if "k" in node.variant { parts.push[$k$-ary] } + if parts.len() > 0 { [#base (#parts.join(", "))] } else { base } +} + +// Format overhead fields as inline text +#let format-overhead(overhead) = { + let parts = overhead.map(o => raw(o.field + " = " + o.formula)) + [_Overhead:_ #parts.join(", ").] +} + +// Unified function for reduction rules: theorem + proof + optional example +#let reduction-rule( + source, target, + example: false, + example-caption: none, + extra: none, + theorem-body, proof-body, +) = { + let arrow = sym.arrow.r + let edge = find-edge(source, target) + let src-disp = if edge != none { variant-display(edge.source) } + else { display-name.at(source) } + let tgt-disp = if edge != none { variant-display(edge.target) } + else { display-name.at(target) } + let src-lbl = label("def:" + source) + let tgt-lbl = label("def:" + target) + let overhead = if edge != none and edge.overhead.len() > 0 { edge.overhead } else { none } + let thm-lbl = label("thm:" + source + "-to-" + target) + // Derive example filename from source/target: "Source" → "source", then "source_to_target" + let example-name = lower(source) + "_to_" + lower(target) + + covered-rules.update(old => old + ((source, target),)) + + [ + #v(1em) + #theorem[ + *(*#context { if query(src-lbl).len() > 0 { link(src-lbl)[#src-disp] } else [#src-disp] }* #arrow *#context { if query(tgt-lbl).len() > 0 { link(tgt-lbl)[#tgt-disp] } else [#tgt-disp] }*)* #theorem-body + #if overhead != none { linebreak(); format-overhead(overhead) } + ] #thm-lbl] + + proof[#proof-body] + + if example { + let data = load-example(example-name) + pad(left: 1.5em, reduction-example(data, caption: example-caption)[#extra]) + } +} + #align(center)[ #text(size: 16pt, weight: "bold")[Problem Reductions: Models and Transformations] #v(0.5em) @@ -102,293 +253,214 @@ A _reduction_ from problem $A$ to problem $B$, denoted $A arrow.long B$, is a po == Notation -We use the following notation throughout. An _undirected graph_ $G = (V, E)$ consists of a vertex set $V$ and edge set $E subset.eq binom(V, 2)$. For a set $S$, $overline(S)$ or $V backslash S$ denotes its complement. We write $|S|$ for cardinality. For Boolean variables, $overline(x)$ denotes negation ($not x$). A _literal_ is a variable $x$ or its negation $overline(x)$. A _clause_ is a disjunction of literals. A formula in _conjunctive normal form_ (CNF) is a conjunction of clauses. We abbreviate Independent Set as IS, Vertex Cover as VC, and use $n$ for problem size, $m$ for number of clauses, and $k_j = |C_j|$ for clause size. +We use the following notation throughout. An _undirected graph_ $G = (V, E)$ consists of a vertex set $V$ and edge set $E subset.eq binom(V, 2)$. For a set $S$, $overline(S)$ or $V backslash S$ denotes its complement. We write $|S|$ for cardinality. A _clique_ in $G$ is a subset $K subset.eq V$ where every pair of distinct vertices is adjacent: $(u, v) in E$ for all distinct $u, v in K$. A _unit disk graph_ is a graph where vertices are points on a 2D lattice and $(u, v) in E$ iff $d(u, v) <= r$ for some radius $r$; a _King's subgraph_ uses the 8-connectivity square grid with $r approx 1.5$. For Boolean variables, $overline(x)$ denotes negation ($not x$). A _literal_ is a variable $x$ or its negation $overline(x)$. A _clause_ is a disjunction of literals. A formula in _conjunctive normal form_ (CNF) is a conjunction of clauses. We abbreviate Independent Set as IS, Vertex Cover as VC, and use $n$ for problem size, $m$ for number of clauses, and $k_j = |C_j|$ for clause size. = Problem Definitions -== Graph Problems - -In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| = n$ vertices and $|E|$ edges. +Each problem definition follows this structure: -#definition("Independent Set (IS)")[ - Given $G = (V, E)$ with vertex weights $w: V -> RR$, find $S subset.eq V$ maximizing $sum_(v in S) w(v)$ such that no two vertices in $S$ are adjacent: $forall u, v in S: (u, v) in.not E$. - - _Implemented reductions:_ IS→VC (@thm:is-to-vc), IS→SetPacking (@thm:is-to-setpacking), IS→QUBO (@thm:is-to-qubo), IS→ILP (@thm:is-to-ilp), IS→GridGraph IS (@thm:is-to-gridgraph), VC→IS (@thm:is-to-vc), SAT→IS (@thm:sat-to-is). +#block( + inset: (x: 1em, y: 0.8em), + fill: rgb("#f8f8f8"), + stroke: (left: 2pt + rgb("#4a86e8")), +)[ + *Definition N (Problem Name).* Formal problem statement defining input, constraints, and objective. - #render-struct("IndependentSet") + #block( + stroke: (left: 2pt + luma(180)), + inset: (left: 8pt), + )[ + #set text(size: 9pt) + #table( + columns: (auto, 1fr), + inset: (x: 6pt, y: 3pt), + align: (left, left), + stroke: none, + table.header(text(fill: luma(30), raw("ProblemName"))), + table.hline(stroke: 0.3pt + luma(200)), + text(fill: luma(60), raw("field_name")), text(fill: luma(60), raw("Field description from JSON schema")), + ) + ] - Where `graph` represents $G = (V, E)$ with vertices indexed $0..n-1$, and `weights` stores vertex weights $w: V -> RR$ indexed by vertex ID. The solution is a subset $S subset.eq V$ represented as a `Vec` of vertex indices. -] + #set text(size: 9pt, fill: luma(60)) + _Reduces to:_ ProblemA, ProblemB. \ + _Reduces from:_ ProblemC. +] -#definition("Vertex Cover (VC)")[ - Given $G = (V, E)$ with vertex weights $w: V -> RR$, find $S subset.eq V$ minimizing $sum_(v in S) w(v)$ such that every edge has at least one endpoint in $S$: $forall (u, v) in E: u in S or v in S$. +The gray schema table shows the JSON field names used in the library's data structures. The reduction links at the bottom connect to the corresponding theorems in @sec:reductions. - _Implemented reductions:_ VC→IS (@thm:is-to-vc), VC→SetCovering (@thm:vc-to-setcovering), VC→QUBO (@thm:vc-to-qubo), VC→ILP (@thm:vc-to-ilp), IS→VC (@thm:is-to-vc). - #render-struct("VertexCovering") - Where `graph` represents $G = (V, E)$ with vertices indexed $0..n-1$, and `weights` stores vertex weights $w: V -> RR$ indexed by vertex ID. The solution is a subset $S subset.eq V$ represented as a `Vec` of vertex indices. -] +== Graph Problems -#definition("Max-Cut")[ - Given $G = (V, E)$ with weights $w: E -> RR$, find partition $(S, overline(S))$ maximizing $sum_((u,v) in E: u in S, v in overline(S)) w(u, v)$. +In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| = n$ vertices and $|E|$ edges. - _Implemented reductions:_ MaxCut→SpinGlass (@thm:spinglass-maxcut), SpinGlass→MaxCut (@thm:spinglass-maxcut). +#problem-def("MaximumIndependentSet")[ + Given $G = (V, E)$ with vertex weights $w: V -> RR$, find $S subset.eq V$ maximizing $sum_(v in S) w(v)$ such that no two vertices in $S$ are adjacent: $forall u, v in S: (u, v) in.not E$. +] - #render-struct("MaxCut") +#problem-def("MinimumVertexCover")[ + Given $G = (V, E)$ with vertex weights $w: V -> RR$, find $S subset.eq V$ minimizing $sum_(v in S) w(v)$ such that every edge has at least one endpoint in $S$: $forall (u, v) in E: u in S or v in S$. +] - Where `graph` represents $G = (V, E)$, and `edge_weights` stores weights $w: E -> RR$ indexed by edge index. The solution is a partition $(S, overline(S))$ represented as a binary assignment `Vec` where 0/1 indicates partition membership. -] +#problem-def("MaxCut")[ + Given $G = (V, E)$ with weights $w: E -> RR$, find partition $(S, overline(S))$ maximizing $sum_((u,v) in E: u in S, v in overline(S)) w(u, v)$. +] -#definition("Graph Coloring")[ +#problem-def("KColoring")[ Given $G = (V, E)$ and $k$ colors, find $c: V -> {1, ..., k}$ minimizing $|{(u, v) in E : c(u) = c(v)}|$. +] - _Implemented reductions:_ Coloring→ILP (@thm:coloring-to-ilp), Coloring→QUBO (@thm:coloring-to-qubo), SAT→Coloring (@thm:sat-to-coloring). - - #render-struct("KColoring") - - Where $k$ is a const generic parameter (not a struct field), and `graph` represents $G = (V, E)$ with vertices indexed $0..n-1$. The solution is a color assignment $c: V -> {0, ..., k-1}$ represented as a `Vec` indexed by vertex. -] - -#definition("Dominating Set")[ +#problem-def("MinimumDominatingSet")[ Given $G = (V, E)$ with weights $w: V -> RR$, find $S subset.eq V$ minimizing $sum_(v in S) w(v)$ s.t. $forall v in V: v in S or exists u in S: (u, v) in E$. +] - _Implemented reductions:_ DominatingSet→ILP (@thm:dominatingset-to-ilp), SAT→DominatingSet (@thm:sat-to-dominatingset). - - #render-struct("DominatingSet") - - Where `graph` represents $G = (V, E)$ with vertices indexed $0..n-1$, and `weights` stores vertex weights $w: V -> RR$ indexed by vertex ID. The solution is a subset $S subset.eq V$ represented as a `Vec` of vertex indices. -] - -#definition("Matching")[ +#problem-def("MaximumMatching")[ Given $G = (V, E)$ with weights $w: E -> RR$, find $M subset.eq E$ maximizing $sum_(e in M) w(e)$ s.t. $forall e_1, e_2 in M: e_1 inter e_2 = emptyset$. +] - _Implemented reductions:_ Matching→SetPacking (@thm:matching-to-setpacking), Matching→ILP (@thm:matching-to-ilp). - - #render-struct("Matching") - - Where `graph` represents $G = (V, E)$ with vertices indexed $0..n-1$, and `edge_weights` stores weights $w: E -> RR$ indexed by edge index. The solution is a subset $M subset.eq E$ represented as a `Vec` of edge indices. -] - -#definition("Clique")[ - Given a graph $G = (V, E)$ and an integer $k$, the *Clique* problem asks whether there exists a subset $K subset.eq V$ of size at least $k$ such that every pair of distinct vertices in $K$ is adjacent, i.e., $(u, v) in E$ for all distinct $u, v in K$. - - _Implemented reductions:_ Clique→ILP (@thm:clique-to-ilp). -] - -#definition("Unit Disk Graph (Grid Graph)")[ - A graph $G = (V, E)$ where vertices $V$ are points on a 2D lattice and $(u, v) in E$ iff the Euclidean distance $d(u, v) <= r$ for some radius $r$. A _King's subgraph_ uses the King's graph lattice (8-connectivity square grid) with $r approx 1.5$. +#problem-def("MaximumClique")[ + Given $G = (V, E)$, find $K subset.eq V$ maximizing $|K|$ such that all pairs in $K$ are adjacent: $forall u, v in K: (u, v) in E$. Equivalent to MIS on the complement graph $overline(G)$. ] + == Set Problems -#definition("Set Packing")[ +#problem-def("MaximumSetPacking")[ Given universe $U$, collection $cal(S) = {S_1, ..., S_m}$ with $S_i subset.eq U$, weights $w: cal(S) -> RR$, find $cal(P) subset.eq cal(S)$ maximizing $sum_(S in cal(P)) w(S)$ s.t. $forall S_i, S_j in cal(P): S_i inter S_j = emptyset$. +] - _Implemented reductions:_ IS→SetPacking (@thm:is-to-setpacking), SetPacking→QUBO (@thm:setpacking-to-qubo), SetPacking→ILP (@thm:setpacking-to-ilp), Matching→SetPacking (@thm:matching-to-setpacking). - - #render-struct("SetPacking") - - Where `sets` represents the collection $cal(S) = {S_1, ..., S_m}$ where each `Vec` contains universe element indices, and `weights` stores set weights $w: cal(S) -> RR$ indexed by set index. The solution is a subset $cal(P) subset.eq cal(S)$ represented as a `Vec` of set indices. -] - -#definition("Set Covering")[ +#problem-def("MinimumSetCovering")[ Given universe $U$, collection $cal(S)$ with weights $w: cal(S) -> RR$, find $cal(C) subset.eq cal(S)$ minimizing $sum_(S in cal(C)) w(S)$ s.t. $union.big_(S in cal(C)) S = U$. - - _Implemented reductions:_ SetCovering→ILP (@thm:setcovering-to-ilp), VC→SetCovering (@thm:vc-to-setcovering). - - #render-struct("SetCovering") - - Where `universe_size` is $|U|$, `sets` represents the collection $cal(S)$ where each `Vec` contains universe element indices, and `weights` stores set weights $w: cal(S) -> RR$ indexed by set index. The solution is a subset $cal(C) subset.eq cal(S)$ represented as a `Vec` of set indices. -] +] == Optimization Problems -#definition("Spin Glass (Ising Model)")[ +#problem-def("SpinGlass")[ Given $n$ spin variables $s_i in {-1, +1}$, pairwise couplings $J_(i j) in RR$, and external fields $h_i in RR$, minimize the Hamiltonian (energy function): $H(bold(s)) = -sum_((i,j)) J_(i j) s_i s_j - sum_i h_i s_i$. +] - _Implemented reductions:_ SpinGlass→MaxCut (@thm:spinglass-maxcut), SpinGlass→QUBO (@thm:spinglass-qubo), Circuit→SpinGlass (@thm:circuit-to-spinglass), MaxCut→SpinGlass (@thm:spinglass-maxcut), QUBO→SpinGlass (@thm:spinglass-qubo). - - #render-struct("SpinGlass") - - Where `graph` encodes the interaction topology, `couplings` stores pairwise couplings $J_(i j)$ as `Vec` in `graph.edges()` order, and `fields` stores external fields $h_i$ as `Vec` indexed by spin. The solution is a spin assignment $bold(s) in {-1, +1}^n$ encoded as `Vec` where 0 maps to $s=-1$ and 1 maps to $s=+1$. -] - -#definition("QUBO")[ +#problem-def("QUBO")[ Given $n$ binary variables $x_i in {0, 1}$, upper-triangular matrix $Q in RR^(n times n)$, minimize $f(bold(x)) = sum_(i=1)^n Q_(i i) x_i + sum_(i < j) Q_(i j) x_i x_j$ (using $x_i^2 = x_i$ for binary variables). +] - _Implemented reductions:_ QUBO→SpinGlass (@thm:spinglass-qubo), IS→QUBO (@thm:is-to-qubo), VC→QUBO (@thm:vc-to-qubo), Coloring→QUBO (@thm:coloring-to-qubo), SetPacking→QUBO (@thm:setpacking-to-qubo), kSAT→QUBO (@thm:ksat-to-qubo), ILP→QUBO (@thm:ilp-to-qubo), SpinGlass→QUBO (@thm:spinglass-qubo). - - #render-struct("QUBO") - - Where `num_vars` is $n$, and `matrix` stores the upper-triangular $Q in RR^(n times n)$ as `Vec>` where `matrix[i][j]` ($i <= j$) stores $Q_(i j)$. The solution is a binary assignment $bold(x) in {0, 1}^n$ represented as `Vec`. -] - -#definition("Integer Linear Programming (ILP)")[ +#problem-def("ILP")[ Given $n$ integer variables $bold(x) in ZZ^n$, constraint matrix $A in RR^(m times n)$, bounds $bold(b) in RR^m$, and objective $bold(c) in RR^n$, find $bold(x)$ minimizing $bold(c)^top bold(x)$ subject to $A bold(x) <= bold(b)$ and variable bounds. - - _Implemented reductions:_ ILP→QUBO (@thm:ilp-to-qubo), Coloring→ILP (@thm:coloring-to-ilp), Factoring→ILP (@thm:factoring-to-ilp), IS→ILP (@thm:is-to-ilp), VC→ILP (@thm:vc-to-ilp), Matching→ILP (@thm:matching-to-ilp), SetPacking→ILP (@thm:setpacking-to-ilp), SetCovering→ILP (@thm:setcovering-to-ilp), DominatingSet→ILP (@thm:dominatingset-to-ilp), Clique→ILP (@thm:clique-to-ilp). - - #render-struct("ILP") - - Where `num_vars` is $n$, `bounds` stores per-variable bounds $x_i in [l_i, u_i]$ as `Vec`, `constraints` encodes $A bold(x) <= bold(b)$ as `Vec`, `objective` is the sparse objective $bold(c)$ as `Vec<(usize, f64)>`, and `sense` specifies maximize or minimize. The solution is $bold(x) in ZZ^n$ represented as `Vec`. -] +] == Satisfiability Problems -#definition("SAT")[ +#problem-def("Satisfiability")[ Given a CNF formula $phi = and.big_(j=1)^m C_j$ with $m$ clauses over $n$ Boolean variables, where each clause $C_j = or.big_i ell_(j i)$ is a disjunction of literals, find an assignment $bold(x) in {0, 1}^n$ such that $phi(bold(x)) = 1$ (all clauses satisfied). +] - _Implemented reductions:_ SAT→IS (@thm:sat-to-is), SAT→Coloring (@thm:sat-to-coloring), SAT→DominatingSet (@thm:sat-to-dominatingset), SAT→kSAT (@thm:sat-ksat), kSAT→SAT (@thm:sat-ksat). - - #render-struct("Satisfiability") - - Where `num_vars` is $n$, `clauses` stores CNF clauses $C_j$ as `Vec`, and `weights` stores clause weights for MAX-SAT as `Vec`. Each `CNFClause` has `literals: Vec` where $+i$ denotes $x_i$ and $-i$ denotes $not x_i$ (1-indexed). The solution is an assignment $bold(x) in {0, 1}^n$ represented as `Vec`. -] - -#definition([$k$-SAT])[ +#problem-def("KSatisfiability")[ SAT with exactly $k$ literals per clause. +] - _Implemented reductions:_ kSAT→SAT (@thm:sat-ksat), kSAT→QUBO (@thm:ksat-to-qubo), SAT→kSAT (@thm:sat-ksat). - - #render-struct("KSatisfiability") - - Where `num_vars` is $n$, `clauses` stores clauses with exactly $k$ literals per clause as `Vec`, and `weights` stores clause weights as `Vec`. The solution is an assignment $bold(x) in {0, 1}^n$ represented as `Vec`. -] - -#definition("Circuit-SAT")[ +#problem-def("CircuitSAT")[ Given a Boolean circuit $C$ composed of logic gates (AND, OR, NOT, XOR) with $n$ input variables, find an input assignment $bold(x) in {0,1}^n$ such that $C(bold(x)) = 1$. +] - _Implemented reductions:_ Circuit→SpinGlass (@thm:circuit-to-spinglass), Factoring→Circuit (@thm:factoring-to-circuit). - - #render-struct("CircuitSAT") - - Where `circuit` is the Boolean circuit of logic gates (AND, OR, NOT, XOR), `variables` stores input variable names as `Vec`, and `weights` stores assignment weights as `Vec`. The solution is an input assignment $bold(x) in {0,1}^n$ represented as `Vec`. -] - -#definition("Factoring")[ +#problem-def("Factoring")[ Given a composite integer $N$ and bit sizes $m, n$, find integers $p in [2, 2^m - 1]$ and $q in [2, 2^n - 1]$ such that $p times q = N$. Here $p$ has $m$ bits and $q$ has $n$ bits. +] - _Implemented reductions:_ Factoring→Circuit (@thm:factoring-to-circuit), Factoring→ILP (@thm:factoring-to-ilp). - - #render-struct("Factoring") - - Where `m` is the number of bits for the first factor $p$, `n` is the number of bits for the second factor $q$, and `target` is the composite $N$ to factor. The solution is bit assignments for $p$ and $q$ represented as `Vec`. -] +// Completeness check: warn about problem types in JSON but missing from paper +#{ + let json-models = { + let names = graph-data.nodes.map(n => n.name) + let unique = () + for n in names { if n not in unique { unique.push(n) } } + unique + } + let defined = display-name.keys() + let missing = json-models.filter(n => n not in defined) + if missing.len() > 0 { + block(width: 100%, inset: (x: 1em, y: 0.5em), fill: rgb("#fff3cd"), stroke: (left: 3pt + rgb("#ffc107")))[ + #text(fill: rgb("#856404"), weight: "bold")[Warning: Missing problem definitions for:] + #text(fill: rgb("#856404"))[ #missing.join(", ")] + ] + } +} = Reductions -== Trivial Reductions - -#theorem[ - *(IS $arrow.l.r$ VC)* $S subset.eq V$ is independent iff $V backslash S$ is a vertex cover, with $|"IS"| + |"VC"| = |V|$. [_Problems:_ @def:independent-set, @def:vertex-cover.] -] +Each reduction is presented as a *Rule* (with linked problem names and overhead from the graph data), followed by a *Proof* (construction, correctness, variable mapping, solution extraction), and optionally a *Concrete Example* (a small instance with verified solution). Problem names in the rule title link back to their definitions in @sec:problems. -#proof[ - ($arrow.r.double$) If $S$ is independent, for any $(u, v) in E$, at most one endpoint lies in $S$, so $V backslash S$ covers all edges. ($arrow.l.double$) If $C$ is a cover, for any $u, v in V backslash C$, $(u, v) in.not E$, so $V backslash C$ is independent. _Variable mapping:_ Given IS instance $(G, w)$, create VC instance $(G, w)$ with identical graph and weights. Solution extraction: for VC solution $C$, return $S = V backslash C$. The complement operation preserves optimality since $|S| + |C| = |V|$ is constant. -] +== Trivial Reductions -```rust -// Minimal example: IS -> VC -> extract solution -let is_problem = IndependentSet::::new(3, vec![(0, 1), (1, 2), (0, 2)]); -let result = ReduceTo::>::reduce_to(&is_problem); -let vc_problem = result.target_problem(); - -let solver = BruteForce::new(); -let vc_solutions = solver.find_best(vc_problem); -let is_solution = result.extract_solution(&vc_solutions[0]); -assert!(is_problem.solution_size(&is_solution).is_valid); -``` - -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_is_to_vc.rs")[`reduction_is_to_vc.rs`]. - -#let is_vc = load-example("is_to_vc") -#let is_vc_r = load-results("is_to_vc") -#let is_vc_sol = is_vc_r.solutions.at(0) -#reduction-example(is_vc, caption: [Path graph $P_4$: IS $arrow.l.r$ VC])[ - Source IS: $S = {#is_vc_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ (size #is_vc_sol.source_config.filter(x => x == 1).len()) #h(1em) - Target VC: $C = {#is_vc_sol.target_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ (size #is_vc_sol.target_config.filter(x => x == 1).len()) \ - $|"IS"| + |"VC"| = #instance-vars(is_vc.source.instance) = |V|$ #sym.checkmark +#let mvc_mis = load-example("minimumvertexcover_to_maximumindependentset") +#let mvc_mis_r = load-results("minimumvertexcover_to_maximumindependentset") +#let mvc_mis_sol = mvc_mis_r.solutions.at(0) +#reduction-rule("MinimumVertexCover", "MaximumIndependentSet", + example: true, + example-caption: [Path graph $P_4$: VC $arrow.l.r$ IS], + extra: [ + Source VC: $C = {#mvc_mis_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ (size #mvc_mis_sol.source_config.filter(x => x == 1).len()) #h(1em) + Target IS: $S = {#mvc_mis_sol.target_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ (size #mvc_mis_sol.target_config.filter(x => x == 1).len()) \ + $|"VC"| + |"IS"| = #mvc_mis.source.instance.num_vertices = |V|$ #sym.checkmark + ], +)[ + $S subset.eq V$ is independent iff $V backslash S$ is a vertex cover, with $|"IS"| + |"VC"| = |V|$. +][ + ($arrow.r.double$) If $C$ is a vertex cover, for any $u, v in V backslash C$, $(u, v) in.not E$, so $V backslash C$ is independent. ($arrow.l.double$) If $S$ is independent, for any $(u, v) in E$, at most one endpoint is in $S$, so $V backslash S$ covers all edges. _Variable mapping:_ Given VC instance $(G, w)$, create IS instance $(G, w)$ with identical graph and weights. Solution extraction: for IS solution $S$, return $C = V backslash S$. The complement operation preserves optimality since $|S| + |C| = |V|$ is constant. ] -#theorem[ - *(IS $arrow.r$ Set Packing)* Construct $U = E$, $S_v = {e in E : v in e}$, $w(S_v) = w(v)$. Then $I$ is independent iff ${S_v : v in I}$ is a packing. [_Problems:_ @def:independent-set, @def:set-packing.] -] - -#proof[ - Independence implies disjoint incident edge sets; conversely, disjoint edge sets imply no shared edges. _Variable mapping:_ Universe $U = E$ (edges), sets $S_v = {e in E : v in e}$ (edges incident to vertex $v$), weights $w(S_v) = w(v)$. Solution extraction: for packing ${S_v : v in P}$, return IS $= P$ (the vertices whose sets were packed). +#reduction-rule("MaximumSetPacking", "MaximumIndependentSet")[ + Construct intersection graph $G' = (V', E')$ where $V' = cal(S)$ and $(S_i, S_j) in E'$ iff $S_i inter S_j != emptyset$, with $w(v_i) = w(S_i)$. Max packing $equiv$ Max IS on $G'$. +][ + Overlapping sets become adjacent vertices; disjoint sets become non-adjacent. A packing (mutually disjoint) maps to an IS (mutually non-adjacent). _Variable mapping:_ Vertices $= {S_1, ..., S_m}$, edges $= {(S_i, S_j) : S_i inter S_j != emptyset}$, $w(v_i) = w(S_i)$. Solution extraction: for IS $I subset.eq V'$, return packing $cal(P) = {S_i : v_i in I}$. ] -```rust -// Minimal example: IS -> SetPacking -> extract solution -let is_problem = IndependentSet::::new(3, vec![(0, 1), (1, 2), (0, 2)]); -let result = ReduceTo::>::reduce_to(&is_problem); -let sp_problem = result.target_problem(); - -let solver = BruteForce::new(); -let sp_solutions = solver.find_best(sp_problem); -let is_solution = result.extract_solution(&sp_solutions[0]); -assert!(is_problem.solution_size(&is_solution).is_valid); -``` - -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_is_to_setpacking.rs")[`reduction_is_to_setpacking.rs`]. - -#theorem[ - *(VC $arrow.r$ Set Covering)* Construct $U = {0, ..., |E|-1}$, $S_v = {i : e_i "incident to" v}$, $w(S_v) = w(v)$. Then $C$ is a cover iff ${S_v : v in C}$ covers $U$. [_Problems:_ @def:vertex-cover, @def:set-covering.] -] - -#proof[ +#reduction-rule("MinimumVertexCover", "MinimumSetCovering")[ + Construct $U = {0, ..., |E|-1}$, $S_v = {i : e_i "incident to" v}$, $w(S_v) = w(v)$. Then $C$ is a cover iff ${S_v : v in C}$ covers $U$. +][ Each vertex's edge set becomes a subset; the cover condition (every edge covered) maps to the covering condition (every universe element in some selected set). _Variable mapping:_ Universe $U = {0, ..., |E|-1}$ (edge indices), $S_v = {i : e_i "incident to" v}$, $w(S_v) = w(v)$. Solution extraction: for covering ${S_v : v in C}$, return VC $= C$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_vc_to_setcovering.rs")[`reduction_vc_to_setcovering.rs`]. - -#theorem[ - *(Matching $arrow.r$ Set Packing)* Construct $U = V$, $S_e = {u, v}$ for $e = (u,v)$, $w(S_e) = w(e)$. Then $M$ is a matching iff ${S_e : e in M}$ is a packing. [_Problems:_ @def:matching, @def:set-packing.] -] - -#proof[ +#reduction-rule("MaximumMatching", "MaximumSetPacking")[ + Construct $U = V$, $S_e = {u, v}$ for $e = (u,v)$, $w(S_e) = w(e)$. Then $M$ is a matching iff ${S_e : e in M}$ is a packing. +][ Each edge becomes a set of its endpoints; disjoint edges have disjoint endpoint sets. _Variable mapping:_ Universe $U = V$ (vertices), $S_e = {u, v}$ for $e = (u,v)$, $w(S_e) = w(e)$. Solution extraction: for packing ${S_e : e in P}$, return matching $= P$ (the edges whose endpoint sets were packed). ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_matching_to_setpacking.rs")[`reduction_matching_to_setpacking.rs`]. - -#theorem[ - *(Spin Glass $arrow.l.r$ QUBO)* The substitution $s_i = 2x_i - 1$ yields $H_"SG"(bold(s)) = H_"QUBO"(bold(x)) + "const"$. [_Problems:_ @def:spin-glass, @def:qubo.] -] - -#proof[ +#reduction-rule("SpinGlass", "QUBO", + example: true, + example-caption: [2-spin system with coupling $J_(01) = -1$, fields $h = (0.5, -0.5)$], +)[ + The substitution $s_i = 2x_i - 1$ yields $H_"SG"(bold(s)) = H_"QUBO"(bold(x)) + "const"$. +][ Expanding $-sum_(i,j) J_(i j) (2x_i - 1)(2x_j - 1) - sum_i h_i (2x_i - 1)$ gives $Q_(i j) = -4J_(i j)$, $Q_(i i) = 2sum_j J_(i j) - 2h_i$. _Variable mapping:_ Spin $s_i in {-1, +1}$ maps to binary $x_i in {0, 1}$ via $s_i = 2x_i - 1$. Solution extraction: for QUBO solution $bold(x)$, return spins $s_i = 2x_i - 1$. The reverse maps $x_i = (s_i + 1)/2$. ] -```rust -// Minimal example: SpinGlass -> QUBO -> extract solution -let sg = SpinGlass::new(2, vec![((0, 1), -1.0)], vec![0.5, -0.5]); -let result = ReduceTo::::reduce_to(&sg); -let qubo = result.target_problem(); - -let solver = BruteForce::new(); -let qubo_solutions = solver.find_best(qubo); -let sg_solution = result.extract_solution(&qubo_solutions[0]); -assert_eq!(sg_solution.len(), 2); -``` - -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_spinglass_to_qubo.rs")[`reduction_spinglass_to_qubo.rs`]. - -#let sg_qubo = load-example("spinglass_to_qubo") -#reduction-example(sg_qubo, caption: [2-spin system with coupling $J_(01) = -1$, fields $h = (0.5, -0.5)$])[] - == Penalty-Method QUBO Reductions The _penalty method_ @glover2019 @lucas2014 converts a constrained optimization problem into an unconstrained QUBO by adding quadratic penalty terms. Given an objective $"obj"(bold(x))$ to minimize and constraints $g_k (bold(x)) = 0$, construct: $ f(bold(x)) = "obj"(bold(x)) + P sum_k g_k (bold(x))^2 $ where $P$ is a penalty weight large enough that any constraint violation costs more than the entire objective range. Since $g_k (bold(x))^2 >= 0$ with equality iff $g_k (bold(x)) = 0$, minimizers of $f$ are feasible and optimal for the original problem. Because binary variables satisfy $x_i^2 = x_i$, the resulting $f$ is a quadratic in $bold(x)$, i.e.\ a QUBO. -#theorem[ - *(IS $arrow.r$ QUBO)* Given $G = (V, E)$ with weights $w$, construct upper-triangular $Q in RR^(n times n)$ with $Q_(i i) = -w_i$ and $Q_(i j) = P$ for $(i,j) in E$ ($i < j$), where $P = 1 + sum_i w_i$. Then minimizing $f(bold(x)) = sum_i Q_(i i) x_i + sum_(i - -#proof[ +#let mis_qubo = load-example("maximumindependentset_to_qubo") +#let mis_qubo_r = load-results("maximumindependentset_to_qubo") +#reduction-rule("MaximumIndependentSet", "QUBO", + example: true, + example-caption: [IS on path $P_4$ to QUBO], + extra: [ + *Source edges:* $= {#mis_qubo.source.instance.edges.map(e => $(#e.at(0), #e.at(1))$).join(", ")}$ \ + *QUBO matrix* ($Q in RR^(#mis_qubo.target.instance.num_vars times #mis_qubo.target.instance.num_vars)$): + $ Q = #math.mat(..mis_qubo.target.instance.matrix.map(row => row.map(v => { + let r = calc.round(v, digits: 0) + [#r] + }))) $ + *Optimal IS* (size #mis_qubo_r.solutions.at(0).source_config.filter(x => x == 1).len()): + #mis_qubo_r.solutions.map(sol => { + let verts = sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)) + $\{#verts.join(", ")\}$ + }).join(", ") + ], +)[ + Given $G = (V, E)$ with weights $w$, construct upper-triangular $Q in RR^(n times n)$ with $Q_(i i) = -w_i$ and $Q_(i j) = P$ for $(i,j) in E$ ($i < j$), where $P = 1 + sum_i w_i$. Then minimizing $f(bold(x)) = sum_i Q_(i i) x_i + sum_(i sum_i w_i >= -sum_i Q_(i i) x_i$ exceeds the maximum objective gain, so $bold(x)$ is not a minimizer. Among independent sets ($x_i x_j = 0$ for all edges), $f(bold(x)) = -sum_(i in S) w_i$, minimized exactly when $S$ is a maximum-weight IS. ] -```rust -// Minimal example: IS -> QUBO -> extract solution -let is = IndependentSet::::new(4, vec![(0, 1), (1, 2), (2, 3)]); -let result = ReduceTo::::reduce_to(&is); -let qubo = result.target_problem(); - -let solver = BruteForce::new(); -let solutions = solver.find_best(qubo); -let is_solution = result.extract_solution(&solutions[0]); -assert!(is.solution_size(&is_solution).is_valid); -``` - -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_is_to_qubo.rs")[`reduction_is_to_qubo.rs`]. - -#let is_qubo = load-example("is_to_qubo") -#let is_qubo_r = load-results("is_to_qubo") -#block( - width: 100%, - inset: (x: 1em, y: 0.8em), - fill: rgb("#f0f7ff"), - stroke: (left: 2pt + rgb("#4a86e8")), -)[ - #text(weight: "bold")[Concrete Example: IS on path $P_4$ to QUBO] - #parbreak() - *Source:* #is_qubo.source.problem with #is_qubo.source.instance.num_vertices vertices, edges $= {#is_qubo.source.instance.edges.map(e => $(#e.at(0), #e.at(1))$).join(", ")}$ \ - *QUBO matrix* ($Q in RR^(#is_qubo.target.instance.num_vars times #is_qubo.target.instance.num_vars)$): - $ Q = #math.mat(..is_qubo.target.instance.matrix.map(row => row.map(v => { - let r = calc.round(v, digits: 0) - [#r] - }))) $ - *Optimal IS* (size #is_qubo_r.solutions.at(0).source_config.filter(x => x == 1).len()): - #is_qubo_r.solutions.map(sol => { - let verts = sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)) - $\{#verts.join(", ")\}$ - }).join(", ") -] - -#theorem[ - *(VC $arrow.r$ QUBO)* Given $G = (V, E)$ with weights $w$, construct upper-triangular $Q$ with $Q_(i i) = w_i - P dot "deg"(i)$ and $Q_(i j) = P$ for $(i,j) in E$ ($i < j$), where $P = 1 + sum_i w_i$ and $"deg"(i)$ is the degree of vertex $i$. [_Problems:_ @def:vertex-cover, @def:qubo.] -] - -#proof[ +#reduction-rule("MinimumVertexCover", "QUBO")[ + Given $G = (V, E)$ with weights $w$, construct upper-triangular $Q$ with $Q_(i i) = w_i - P dot "deg"(i)$ and $Q_(i j) = P$ for $(i,j) in E$ ($i < j$), where $P = 1 + sum_i w_i$ and $"deg"(i)$ is the degree of vertex $i$. +][ _Construction._ The VC objective is: minimize $sum_i w_i x_i$ subject to $x_i + x_j >= 1$ for $(i,j) in E$. Applying the penalty method (@sec:penalty-method), the constraint $x_i + x_j >= 1$ is violated iff $x_i = x_j = 0$, with penalty $(1 - x_i)(1 - x_j)$: $ f(bold(x)) = sum_i w_i x_i + P sum_((i,j) in E) (1 - x_i)(1 - x_j) $ Expanding: $(1 - x_i)(1 - x_j) = 1 - x_i - x_j + x_i x_j$. Summing over all edges, each vertex $i$ appears in $"deg"(i)$ terms. The QUBO coefficients are: diagonal $Q_(i i) = w_i - P dot "deg"(i)$ (objective plus linear penalty), off-diagonal $Q_(i j) = P$ for edges. The constant $P |E|$ does not affect the minimizer. ] -```rust -// Minimal example: VC -> QUBO -> extract solution -let vc = VertexCovering::::new(4, vec![(0, 1), (1, 2), (2, 3), (0, 3)]); -let result = ReduceTo::::reduce_to(&vc); -let qubo = result.target_problem(); - -let solver = BruteForce::new(); -let solutions = solver.find_best(qubo); -let vc_solution = result.extract_solution(&solutions[0]); -assert!(vc.solution_size(&vc_solution).is_valid); -``` - -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_vc_to_qubo.rs")[`reduction_vc_to_qubo.rs`]. - -#theorem[ - *(KColoring $arrow.r$ QUBO)* Given $G = (V, E)$ with $k$ colors, construct upper-triangular $Q in RR^(n k times n k)$ using one-hot encoding $x_(v,c) in {0,1}$ ($n k$ variables indexed by $v dot k + c$). [_Problems:_ @def:coloring, @def:qubo.] -] - -#proof[ +#reduction-rule("KColoring", "QUBO")[ + Given $G = (V, E)$ with $k$ colors, construct upper-triangular $Q in RR^(n k times n k)$ using one-hot encoding $x_(v,c) in {0,1}$ ($n k$ variables indexed by $v dot k + c$). +][ _Construction._ Applying the penalty method (@sec:penalty-method), the QUBO objective combines a one-hot constraint penalty and an edge conflict penalty: $ f(bold(x)) = P_1 sum_(v in V) (1 - sum_(c=1)^k x_(v,c))^2 + P_2 sum_((u,v) in E) sum_(c=1)^k x_(u,c) x_(v,c) $ @@ -477,47 +494,15 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples _Solution extraction._ For each vertex $v$, find $c$ with $x_(v,c) = 1$. ] -```rust -// Minimal example: KColoring -> QUBO -> extract solution -let kc = KColoring::<3, SimpleGraph, i32>::new(3, vec![(0, 1), (1, 2), (0, 2)]); -let result = ReduceTo::::reduce_to(&kc); -let qubo = result.target_problem(); - -let solver = BruteForce::new(); -let solutions = solver.find_best(qubo); -let kc_solution = result.extract_solution(&solutions[0]); -assert_eq!(solutions.len(), 6); // 3! valid 3-colorings of K3 -``` - -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_coloring_to_qubo.rs")[`reduction_coloring_to_qubo.rs`]. - -#theorem[ - *(SetPacking $arrow.r$ QUBO)* Equivalent to IS on the intersection graph: $Q_(i i) = -w_i$ and $Q_(i j) = P$ for overlapping sets $i, j$ ($i < j$), where $P = 1 + sum_i w_i$. [_Problems:_ @def:set-packing, @def:qubo.] -] - -#proof[ +#reduction-rule("MaximumSetPacking", "QUBO")[ + Equivalent to IS on the intersection graph: $Q_(i i) = -w_i$ and $Q_(i j) = P$ for overlapping sets $i, j$ ($i < j$), where $P = 1 + sum_i w_i$. +][ Two sets conflict iff they share an element. The intersection graph has sets as vertices and edges between conflicting pairs. Applying the penalty method (@sec:penalty-method) yields the same QUBO as IS on this graph: diagonal rewards selection, off-diagonal penalizes overlap. Correctness follows from the IS→QUBO proof. ] -```rust -// Minimal example: SetPacking -> QUBO -> extract solution -let sp = SetPacking::::new(vec![vec![0, 1], vec![1, 2], vec![2, 3, 4]]); -let result = ReduceTo::::reduce_to(&sp); -let qubo = result.target_problem(); - -let solver = BruteForce::new(); -let solutions = solver.find_best(qubo); -let sp_solution = result.extract_solution(&solutions[0]); -assert!(sp.solution_size(&sp_solution).is_valid); -``` - -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_setpacking_to_qubo.rs")[`reduction_setpacking_to_qubo.rs`]. - -#theorem[ - *(2-SAT $arrow.r$ QUBO)* Given a Max-2-SAT instance with $m$ clauses over $n$ variables, construct upper-triangular $Q in RR^(n times n)$ where each clause $(ell_i or ell_j)$ contributes a penalty gadget encoding its unique falsifying assignment. [_Problems:_ @def:k-sat, @def:qubo.] -] - -#proof[ +#reduction-rule("KSatisfiability", "QUBO")[ + Given a Max-2-SAT instance with $m$ clauses over $n$ variables, construct upper-triangular $Q in RR^(n times n)$ where each clause $(ell_i or ell_j)$ contributes a penalty gadget encoding its unique falsifying assignment. +][ _Construction._ Applying the penalty method (@sec:penalty-method), each 2-literal clause has exactly one falsifying assignment (both literals false). The penalty for that assignment is a quadratic function of $x_i, x_j$: #table( @@ -534,29 +519,9 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples Summing over all clauses, $f(bold(x)) = sum_j "penalty"_j (bold(x))$ counts falsified clauses. Minimizers of $f$ maximize satisfied clauses. ] -```rust -// Minimal example: 2-SAT -> QUBO -> extract solution -let ksat = KSatisfiability::<2, i32>::new(3, vec![ - CNFClause::new(vec![1, 2]), // x1 OR x2 - CNFClause::new(vec![-1, 3]), // NOT x1 OR x3 - CNFClause::new(vec![2, -3]), // x2 OR NOT x3 -]); -let result = ReduceTo::::reduce_to(&ksat); -let qubo = result.target_problem(); - -let solver = BruteForce::new(); -let solutions = solver.find_best(qubo); -let sat_solution = result.extract_solution(&solutions[0]); -assert!(ksat.solution_size(&sat_solution).is_valid); -``` - -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_ksatisfiability_to_qubo.rs")[`reduction_ksatisfiability_to_qubo.rs`]. - -#theorem[ - *(Binary ILP $arrow.r$ QUBO)* Given binary ILP: maximize $bold(c)^top bold(x)$ subject to $A bold(x) = bold(b)$, $bold(x) in {0,1}^n$, construct upper-triangular $Q = -"diag"(bold(c) + 2P bold(b)^top A) + P A^top A$ where $P = 1 + ||bold(c)||_1 + ||bold(b)||_1$. [_Problems:_ @def:ilp, @def:qubo.] -] - -#proof[ +#reduction-rule("ILP", "QUBO")[ + Given binary ILP: maximize $bold(c)^top bold(x)$ subject to $A bold(x) = bold(b)$, $bold(x) in {0,1}^n$, construct upper-triangular $Q = -"diag"(bold(c) + 2P bold(b)^top A) + P A^top A$ where $P = 1 + ||bold(c)||_1 + ||bold(b)||_1$. +][ _Step 1: Normalize constraints._ Convert inequalities to equalities using slack variables: $bold(a)_k^top bold(x) <= b_k$ becomes $bold(a)_k^top bold(x) + sum_(s=0)^(S_k - 1) 2^s y_(k,s) = b_k$ where $S_k = ceil(log_2 (b_k + 1))$ slack bits. For $>=$ constraints, the slack has a negative sign. The extended system is $A' bold(x)' = bold(b)$ with $bold(x)' = (bold(x), bold(y)) in {0,1}^(n')$. For minimization, negate $bold(c)$ to convert to maximization. _Step 2: QUBO construction._ Applying the penalty method (@sec:penalty-method), combine objective and penalty: @@ -570,34 +535,21 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples _Solution extraction._ Discard slack variables: return $bold(x)' [0..n]$. ] -```rust -// Minimal example: binary ILP -> QUBO -> extract solution -let ilp = ILP::binary(3, - vec![ - LinearConstraint::le(vec![(0, 1.0), (1, 1.0)], 1.0), - LinearConstraint::le(vec![(1, 1.0), (2, 1.0)], 1.0), - ], - vec![(0, 1.0), (1, 2.0), (2, 3.0)], - ObjectiveSense::Maximize, -); -let result = ReduceTo::>::reduce_to(&ilp); -let qubo = result.target_problem(); - -let solver = BruteForce::new(); -let solutions = solver.find_best(qubo); -let ilp_solution = result.extract_solution(&solutions[0]); -assert_eq!(ilp_solution, vec![1, 0, 1]); // obj = 4 -``` - -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_ilp_to_qubo.rs")[`reduction_ilp_to_qubo.rs`]. - == Non-Trivial Reductions -#theorem[ - *(SAT $arrow.r$ IS)* @karp1972 Given CNF $phi$ with $m$ clauses, construct graph $G$ such that $phi$ is satisfiable iff $G$ has an IS of size $m$. [_Problems:_ @def:satisfiability, @def:independent-set.] -] - -#proof[ +#let sat_mis = load-example("satisfiability_to_maximumindependentset") +#let sat_mis_r = load-results("satisfiability_to_maximumindependentset") +#let sat_mis_sol = sat_mis_r.solutions.at(0) +#reduction-rule("Satisfiability", "MaximumIndependentSet", + example: true, + example-caption: [$phi = (x_1 or x_2) and (not x_1 or x_3) and (x_2 or not x_3)$], + extra: [ + SAT assignment: $x_1=#sat_mis_sol.source_config.at(0), x_2=#sat_mis_sol.source_config.at(1), x_3=#sat_mis_sol.source_config.at(2)$ #h(1em) + IS graph: #sat_mis.target.instance.num_vertices vertices, #sat_mis.target.instance.num_edges edges (one vertex per literal occurrence) + ], +)[ + @karp1972 Given CNF $phi$ with $m$ clauses, construct graph $G$ such that $phi$ is satisfiable iff $G$ has an IS of size $m$. +][ _Construction._ For $phi = and.big_(j=1)^m C_j$ with $C_j = (ell_(j,1) or ... or ell_(j,k_j))$: _Vertices:_ For each literal $ell_(j,i)$ in clause $C_j$, create $v_(j,i)$. Total: $|V| = sum_j k_j$. @@ -609,21 +561,9 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples _Solution extraction._ For $v_(j,i) in S$ with literal $x_k$: set $x_k = 1$; for $overline(x_k)$: set $x_k = 0$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_sat_to_is.rs")[`reduction_sat_to_is.rs`]. - -#let sat_is = load-example("sat_to_is") -#let sat_is_r = load-results("sat_to_is") -#let sat_is_sol = sat_is_r.solutions.at(0) -#reduction-example(sat_is, caption: [$phi = (x_1 or x_2) and (not x_1 or x_3) and (x_2 or not x_3)$])[ - SAT assignment: $x_1=#sat_is_sol.source_config.at(0), x_2=#sat_is_sol.source_config.at(1), x_3=#sat_is_sol.source_config.at(2)$ #h(1em) - IS graph: #sat_is.target.instance.num_vertices vertices, #sat_is.target.instance.num_edges edges (one vertex per literal occurrence) -] - -#theorem[ - *(SAT $arrow.r$ 3-Coloring)* @garey1979 Given CNF $phi$, construct graph $G$ such that $phi$ is satisfiable iff $G$ is 3-colorable. [_Problems:_ @def:satisfiability, @def:coloring.] -] - -#proof[ +#reduction-rule("Satisfiability", "KColoring")[ + @garey1979 Given CNF $phi$, construct graph $G$ such that $phi$ is satisfiable iff $G$ is 3-colorable. +][ _Construction._ (1) Base triangle: TRUE, FALSE, AUX vertices with all pairs connected. (2) Variable gadget for $x_i$: vertices $"pos"_i$, $"neg"_i$ connected to each other and to AUX. (3) Clause gadget: for $(ell_1 or ... or ell_k)$, apply OR-gadgets iteratively producing output $o$, then connect $o$ to FALSE and AUX. _OR-gadget$(a, b) arrow.bar o$:_ Five vertices encoding $o = a or b$: if both $a, b$ have FALSE color, $o$ cannot have TRUE color. @@ -631,13 +571,9 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples _Solution extraction._ Set $x_i = 1$ iff $"color"("pos"_i) = "color"("TRUE")$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_sat_to_coloring.rs")[`reduction_sat_to_coloring.rs`]. - -#theorem[ - *(SAT $arrow.r$ Dominating Set)* @garey1979 Given CNF $phi$ with $n$ variables and $m$ clauses, $phi$ is satisfiable iff the constructed graph has a dominating set of size $n$. [_Problems:_ @def:satisfiability, @def:dominating-set.] -] - -#proof[ +#reduction-rule("Satisfiability", "MinimumDominatingSet")[ + @garey1979 Given CNF $phi$ with $n$ variables and $m$ clauses, $phi$ is satisfiable iff the constructed graph has a dominating set of size $n$. +][ _Construction._ (1) Variable triangle for $x_i$: vertices $"pos"_i = 3i$, $"neg"_i = 3i+1$, $"dum"_i = 3i+2$ forming a triangle. (2) Clause vertex $c_j = 3n+j$ connected to $"pos"_i$ if $x_i in C_j$, to $"neg"_i$ if $overline(x_i) in C_j$. _Correctness._ Each triangle requires at least one vertex in any dominating set. Size-$n$ set must take exactly one per triangle, which dominates clause vertices iff corresponding literals satisfy all clauses. @@ -645,13 +581,9 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples _Solution extraction._ Set $x_i = 1$ if $"pos"_i$ selected; $x_i = 0$ if $"neg"_i$ selected. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_sat_to_dominatingset.rs")[`reduction_sat_to_dominatingset.rs`]. - -#theorem[ - *(SAT $arrow.l.r$ $k$-SAT)* @cook1971 @garey1979 Any SAT formula converts to $k$-SAT ($k >= 3$) preserving satisfiability. [_Problems:_ @def:satisfiability, @def:k-sat.] -] - -#proof[ +#reduction-rule("Satisfiability", "KSatisfiability")[ + @cook1971 @garey1979 Any SAT formula converts to $k$-SAT ($k >= 3$) preserving satisfiability. +][ _Small clauses ($|C| < k$):_ Pad $(ell_1 or ... or ell_r)$ with auxiliary $y$: $(ell_1 or ... or ell_r or y or overline(y) or ...)$ to length $k$. _Large clauses ($|C| > k$):_ Split $(ell_1 or ... or ell_r)$ with auxiliaries $y_1, ..., y_(r-k)$: @@ -660,13 +592,9 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples _Correctness._ Original clause true $arrow.l.r$ auxiliary chain can propagate truth through new clauses. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_sat_to_ksat.rs")[`reduction_sat_to_ksat.rs`]. - -#theorem[ - *(CircuitSAT $arrow.r$ Spin Glass)* @whitfield2012 @lucas2014 Each gate maps to a gadget whose ground states encode valid I/O. [_Problems:_ @def:circuit-sat, @def:spin-glass.] -] - -#proof[ +#reduction-rule("CircuitSAT", "SpinGlass")[ + @whitfield2012 @lucas2014 Each gate maps to a gadget whose ground states encode valid I/O. +][ _Spin mapping:_ $sigma in {0,1} arrow.bar s = 2sigma - 1 in {-1, +1}$. _Gate gadgets_ (inputs 0,1; output 2; auxiliary 3 for XOR) are shown in @tab:gadgets. Allocate spins per variable, instantiate gadgets, sum Hamiltonians. Ground states correspond to satisfying assignments. @@ -686,13 +614,9 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples caption: [Ising gadgets for logic gates. Ground states match truth tables.] ) -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_circuit_to_spinglass.rs")[`reduction_circuit_to_spinglass.rs`]. - -#theorem[ - *(Factoring $arrow.r$ Circuit-SAT)* An array multiplier with output constrained to $N$ is satisfiable iff $N$ factors within bit bounds. _(Folklore; no canonical reference.)_ [_Problems:_ @def:factoring, @def:circuit-sat.] -] - -#proof[ +#reduction-rule("Factoring", "CircuitSAT")[ + An array multiplier with output constrained to $N$ is satisfiable iff $N$ factors within bit bounds. _(Folklore; no canonical reference.)_ +][ _Construction._ Build $m times n$ array multiplier for $p times q$: _Full adder $(i,j)$:_ $s_(i,j) + 2c_(i,j) = (p_i and q_j) + s_"prev" + c_"prev"$ via: @@ -704,13 +628,9 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples _Solution extraction._ $p = sum_i p_i 2^(i-1)$, $q = sum_j q_j 2^(j-1)$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_factoring_to_circuit.rs")[`reduction_factoring_to_circuit.rs`]. - -#theorem[ - *(Spin Glass $arrow.l.r$ Max-Cut)* @barahona1982 @lucas2014 Ground states of Ising models correspond to maximum cuts. [_Problems:_ @def:spin-glass, @def:max-cut.] -] - -#proof[ +#reduction-rule("SpinGlass", "MaxCut")[ + @barahona1982 @lucas2014 Ground states of Ising models correspond to maximum cuts. +][ _MaxCut $arrow.r$ SpinGlass:_ Set $J_(i j) = w_(i j)$, $h_i = 0$. Maximizing cut equals minimizing $-sum J_(i j) s_i s_j$ since $s_i s_j = -1$ when $s_i != s_j$. _SpinGlass $arrow.r$ MaxCut:_ If $h_i = 0$: direct mapping $w_(i j) = J_(i j)$. Otherwise, add ancilla $a$ with $w_(i,a) = h_i$. @@ -718,25 +638,9 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples _Solution extraction._ Without ancilla: identity. With ancilla: if $sigma_a = 1$, flip all spins before removing ancilla. ] -```rust -// Minimal example: SpinGlass -> MaxCut -> extract solution -let sg = SpinGlass::new(3, vec![((0, 1), 1), ((1, 2), 1), ((0, 2), 1)], vec![0, 0, 0]); -let result = ReduceTo::>::reduce_to(&sg); -let maxcut = result.target_problem(); - -let solver = BruteForce::new(); -let maxcut_solutions = solver.find_best(maxcut); -let sg_solution = result.extract_solution(&maxcut_solutions[0]); -assert_eq!(sg_solution.len(), 3); -``` - -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_spinglass_to_maxcut.rs")[`reduction_spinglass_to_maxcut.rs`]. - -#theorem[ - *(Coloring $arrow.r$ ILP)* The $k$-coloring problem reduces to binary ILP with $|V| dot k$ variables and $|V| + |E| dot k$ constraints. [_Problems:_ @def:coloring, @def:ilp.] -] - -#proof[ +#reduction-rule("KColoring", "ILP")[ + The $k$-coloring problem reduces to binary ILP with $|V| dot k$ variables and $|V| + |E| dot k$ constraints. +][ _Construction._ For graph $G = (V, E)$ with $k$ colors: _Variables:_ Binary $x_(v,c) in {0, 1}$ for each vertex $v in V$ and color $c in {1, ..., k}$. Interpretation: $x_(v,c) = 1$ iff vertex $v$ has color $c$. @@ -750,13 +654,9 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples _Solution extraction._ For each vertex $v$, find $c$ with $x_(v,c) = 1$; assign color $c$ to $v$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_coloring_to_ilp.rs")[`reduction_coloring_to_ilp.rs`]. - -#theorem[ - *(Factoring $arrow.r$ ILP)* Integer factorization reduces to binary ILP using McCormick linearization with $O(m n)$ variables and constraints. [_Problems:_ @def:factoring, @def:ilp.] -] - -#proof[ +#reduction-rule("Factoring", "ILP")[ + Integer factorization reduces to binary ILP using McCormick linearization with $O(m n)$ variables and constraints. +][ _Construction._ For target $N$ with $m$-bit factor $p$ and $n$-bit factor $q$: _Variables:_ Binary $p_i, q_j in {0,1}$ for factor bits; binary $z_(i j) in {0,1}$ for products $p_i dot q_j$; integer $c_k >= 0$ for carries at each bit position. @@ -775,113 +675,57 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples _Solution extraction._ Read $p = sum_i p_i 2^i$ and $q = sum_j q_j 2^j$ from the binary variables. ] -_Example: Factoring 15._ The following Rust code demonstrates the closed-loop reduction (requires `ilp` feature: `cargo add problemreductions --features ilp`): - -```rust -use problemreductions::prelude::*; - -// 1. Create factoring instance: find p (4-bit) × q (4-bit) = 15 -let problem = Factoring::new(4, 4, 15); - -// 2. Reduce to ILP -let reduction = ReduceTo::::reduce_to(&problem); -let ilp = reduction.target_problem(); - -// 3. Solve ILP -let solver = ILPSolver::new(); -let ilp_solution = solver.solve(ilp).unwrap(); - -// 4. Extract factoring solution -let extracted = reduction.extract_solution(&ilp_solution); - -// 5. Verify: reads factors and confirms p × q = 15 -let (p, q) = problem.read_factors(&extracted); -assert_eq!(p * q, 15); // e.g., (3, 5) or (5, 3) -``` - -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_factoring_to_ilp.rs")[`reduction_factoring_to_ilp.rs`]. - == ILP Formulations The following reductions to Integer Linear Programming are straightforward formulations where problem constraints map directly to linear inequalities. -#theorem[ - *(IS $arrow.r$ ILP)* The maximum-weight IS problem reduces to binary ILP with $|V|$ variables and $|E|$ constraints. [_Problems:_ @def:independent-set, @def:ilp.] -] - -#proof[ +#reduction-rule("MaximumIndependentSet", "ILP")[ + The maximum-weight IS problem reduces to binary ILP with $|V|$ variables and $|E|$ constraints. +][ _Construction._ Variables: $x_v in {0, 1}$ for each $v in V$. Constraints: $x_u + x_v <= 1$ for each $(u, v) in E$. Objective: maximize $sum_v w_v x_v$. _Solution extraction:_ $S = {v : x_v = 1}$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_is_to_ilp.rs")[`reduction_is_to_ilp.rs`]. - -#theorem[ - *(VC $arrow.r$ ILP)* The minimum-weight VC problem reduces to binary ILP with $|V|$ variables and $|E|$ constraints. [_Problems:_ @def:vertex-cover, @def:ilp.] -] - -#proof[ +#reduction-rule("MinimumVertexCover", "ILP")[ + The minimum-weight VC problem reduces to binary ILP with $|V|$ variables and $|E|$ constraints. +][ _Construction._ Variables: $x_v in {0, 1}$ for each $v in V$. Constraints: $x_u + x_v >= 1$ for each $(u, v) in E$. Objective: minimize $sum_v w_v x_v$. _Solution extraction:_ $C = {v : x_v = 1}$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_vc_to_ilp.rs")[`reduction_vc_to_ilp.rs`]. - -#theorem[ - *(Matching $arrow.r$ ILP)* The maximum-weight matching reduces to binary ILP with $|E|$ variables and $|V|$ constraints. [_Problems:_ @def:matching, @def:ilp.] -] - -#proof[ +#reduction-rule("MaximumMatching", "ILP")[ + The maximum-weight matching reduces to binary ILP with $|E|$ variables and $|V|$ constraints. +][ _Construction._ Variables: $x_e in {0, 1}$ for each $e in E$. Constraints: $sum_(e in.rev v) x_e <= 1$ for each $v in V$. Objective: maximize $sum_e w_e x_e$. _Solution extraction:_ $M = {e : x_e = 1}$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_matching_to_ilp.rs")[`reduction_matching_to_ilp.rs`]. - -#theorem[ - *(SetPacking $arrow.r$ ILP)* Set packing reduces to binary ILP with $|cal(S)|$ variables and at most $binom(|cal(S)|, 2)$ constraints. [_Problems:_ @def:set-packing, @def:ilp.] -] - -#proof[ +#reduction-rule("MaximumSetPacking", "ILP")[ + Set packing reduces to binary ILP with $|cal(S)|$ variables and at most $binom(|cal(S)|, 2)$ constraints. +][ _Construction._ Variables: $x_i in {0, 1}$ for each $S_i in cal(S)$. Constraints: $x_i + x_j <= 1$ for each overlapping pair $S_i, S_j in cal(S)$ with $S_i inter S_j != emptyset$. Objective: maximize $sum_i w_i x_i$. _Solution extraction:_ $cal(P) = {S_i : x_i = 1}$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_setpacking_to_ilp.rs")[`reduction_setpacking_to_ilp.rs`]. - -#theorem[ - *(SetCovering $arrow.r$ ILP)* Set covering reduces to binary ILP with $|cal(S)|$ variables and $|U|$ constraints. [_Problems:_ @def:set-covering, @def:ilp.] -] - -#proof[ +#reduction-rule("MinimumSetCovering", "ILP")[ + Set covering reduces to binary ILP with $|cal(S)|$ variables and $|U|$ constraints. +][ _Construction._ Variables: $x_i in {0, 1}$ for each $S_i in cal(S)$. Constraints: $sum_(S_i in.rev u) x_i >= 1$ for each $u in U$. Objective: minimize $sum_i w_i x_i$. _Solution extraction:_ $cal(C) = {S_i : x_i = 1}$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_setcovering_to_ilp.rs")[`reduction_setcovering_to_ilp.rs`]. - -#theorem[ - *(DominatingSet $arrow.r$ ILP)* Dominating set reduces to binary ILP with $|V|$ variables and $|V|$ constraints. [_Problems:_ @def:dominating-set, @def:ilp.] -] - -#proof[ +#reduction-rule("MinimumDominatingSet", "ILP")[ + Dominating set reduces to binary ILP with $|V|$ variables and $|V|$ constraints. +][ _Construction._ Variables: $x_v in {0, 1}$ for each $v in V$. Constraints: $x_v + sum_(u in N(v)) x_u >= 1$ for each $v in V$ (each vertex dominated). Objective: minimize $sum_v w_v x_v$. _Solution extraction:_ $D = {v : x_v = 1}$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_dominatingset_to_ilp.rs")[`reduction_dominatingset_to_ilp.rs`]. - -#theorem[ - *(Clique $arrow.r$ ILP)* Maximum clique reduces to binary ILP with $|V|$ variables and $O(|overline(E)|)$ constraints. [_Problems:_ @def:clique, @def:ilp.] -] - -#proof[ +#reduction-rule("MaximumClique", "ILP")[ + Maximum clique reduces to binary ILP with $|V|$ variables and $O(|overline(E)|)$ constraints. +][ _Construction._ Variables: $x_v in {0, 1}$ for each $v in V$. Constraints: $x_u + x_v <= 1$ for each $(u, v) in.not E$ (non-edges). Objective: maximize $sum_v x_v$. Equivalently, IS on the complement graph. _Solution extraction:_ $K = {v : x_v = 1}$. ] -See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/reduction_clique_to_ilp.rs")[`reduction_clique_to_ilp.rs`]. - == Unit Disk Mapping -#theorem[ - *(IS $arrow.r$ GridGraph IS)* @nguyen2023 Any MIS problem on a general graph $G$ can be reduced to MIS on a unit disk graph (King's subgraph) with at most quadratic overhead in the number of vertices. [_Problem:_ @def:independent-set.] -] - -#proof[ +#reduction-rule("MaximumIndependentSet", "GridGraph")[ + @nguyen2023 Any MIS problem on a general graph $G$ can be reduced to MIS on a unit disk graph (King's subgraph) with at most quadratic overhead in the number of vertices. +][ _Construction (Copy-Line Method)._ Given $G = (V, E)$ with $n = |V|$: 1. _Vertex ordering:_ Compute a path decomposition of $G$ to obtain vertex order $(v_1, ..., v_n)$. The pathwidth determines the grid height. @@ -1036,23 +880,53 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples/export_petersen_mapping.rs")[`export_petersen_mapping.rs`]. +// Completeness check: warn about reduction rules in JSON but missing from paper +#context { + let covered = covered-rules.get() + let json-edges = { + let edges = graph-data.edges.map(e => (e.source.name, e.target.name)) + let unique = () + for e in edges { + if unique.find(u => u.at(0) == e.at(0) and u.at(1) == e.at(1)) == none { + unique.push(e) + } + } + unique + } + let missing = json-edges.filter(e => { + covered.find(c => + (c.at(0) == e.at(0) and c.at(1) == e.at(1)) or + (c.at(0) == e.at(1) and c.at(1) == e.at(0)) + ) == none + }) + if missing.len() > 0 { + block(width: 100%, inset: (x: 1em, y: 0.5em), fill: rgb("#fff3cd"), stroke: (left: 3pt + rgb("#ffc107")))[ + #text(fill: rgb("#856404"), weight: "bold")[Warning: Missing reduction rules:] \ + #for m in missing [ + #text(fill: rgb("#856404"))[- #m.at(0) #sym.arrow.r #m.at(1)] \ + ] + ] + } +} + == Resource Estimation from Examples The following table shows concrete variable overhead for example instances, generated from the reduction examples (`make examples`). #let example-files = ( - "is_to_vc", "vc_to_is", "is_to_setpacking", "matching_to_setpacking", - "vc_to_setcovering", + "maximumindependentset_to_minimumvertexcover", "minimumvertexcover_to_maximumindependentset", + "maximumindependentset_to_maximumsetpacking", "maximummatching_to_maximumsetpacking", + "minimumvertexcover_to_minimumsetcovering", "maxcut_to_spinglass", "spinglass_to_maxcut", "spinglass_to_qubo", "qubo_to_spinglass", - "is_to_qubo", "vc_to_qubo", "coloring_to_qubo", - "setpacking_to_qubo", "ksatisfiability_to_qubo", "ilp_to_qubo", - "sat_to_is", "sat_to_coloring", "sat_to_dominatingset", "sat_to_ksat", - "circuit_to_spinglass", "factoring_to_circuit", - "is_to_ilp", "vc_to_ilp", "matching_to_ilp", - "coloring_to_ilp", "factoring_to_ilp", - "setpacking_to_ilp", "setcovering_to_ilp", - "dominatingset_to_ilp", "clique_to_ilp", + "maximumindependentset_to_qubo", "minimumvertexcover_to_qubo", "kcoloring_to_qubo", + "maximumsetpacking_to_qubo", "ksatisfiability_to_qubo", "ilp_to_qubo", + "satisfiability_to_maximumindependentset", "satisfiability_to_kcoloring", "satisfiability_to_minimumdominatingset", "satisfiability_to_ksatisfiability", + "circuitsat_to_spinglass", "factoring_to_circuitsat", + "maximumindependentset_to_ilp", "minimumvertexcover_to_ilp", "maximummatching_to_ilp", + "kcoloring_to_ilp", "factoring_to_ilp", + "maximumsetpacking_to_ilp", "minimumsetcovering_to_ilp", + "minimumdominatingset_to_ilp", "maximumclique_to_ilp", ) #let examples = example-files.map(n => { @@ -1060,69 +934,5 @@ The following table shows concrete variable overhead for example instances, gene (name: n, data: d) }) -#figure( - table( - columns: (auto, auto, auto, auto, auto), - inset: 5pt, - align: (left, left, right, right, right), - table.header([*Reduction*], [*Instance*], [*Src Vars*], [*Tgt Vars*], [*Ratio*]), - ..examples.map(ex => { - let d = ex.data - let sv = instance-vars(d.source.instance) - let tv = instance-vars(d.target.instance) - let ratio = if sv > 0 { calc.round(tv / sv, digits: 1) } else { 0 } - let label = ex.name.replace("_to_", " $arrow.r$ ").replace("_", " ") - ( - [#label], - [#d.source.problem $arrow.r$ #d.target.problem], - [#sv], - [#tv], - [#(ratio)x], - ) - }).flatten() - ), - caption: [Concrete variable overhead for all example instances. Generated by `make examples`.] -) - -= Summary - -#let gray = rgb("#e8e8e8") - -#figure( - table( - columns: (auto, auto, auto), - inset: 5pt, - align: left, - table.header([*Reduction*], [*Overhead*], [*Reference*]), - table.cell(fill: gray)[IS $arrow.l.r$ VC], table.cell(fill: gray)[$O(|V|)$], table.cell(fill: gray)[—], - table.cell(fill: gray)[IS $arrow.r$ SetPacking], table.cell(fill: gray)[$O(|V| + |E|)$], table.cell(fill: gray)[—], - table.cell(fill: gray)[Matching $arrow.r$ SetPacking], table.cell(fill: gray)[$O(|E|)$], table.cell(fill: gray)[—], - table.cell(fill: gray)[VC $arrow.r$ SetCovering], table.cell(fill: gray)[$O(|V| + |E|)$], table.cell(fill: gray)[—], - [IS $arrow.r$ QUBO], [$O(n)$], [@lucas2014 @glover2019], - [VC $arrow.r$ QUBO], [$O(n)$], [@lucas2014 @glover2019], - [KColoring $arrow.r$ QUBO], [$O(n dot k)$], [@lucas2014 @glover2019], - [SetPacking $arrow.r$ QUBO], [$O(n)$], [@glover2019], - [2-SAT $arrow.r$ QUBO], [$O(n)$], [@glover2019], - [Binary ILP $arrow.r$ QUBO], [$O(n)$], [@lucas2014 @glover2019], - [SAT $arrow.r$ IS], [$O(sum_j |C_j|^2)$], [@karp1972], - [SAT $arrow.r$ 3-Coloring], [$O(n + sum_j |C_j|)$], [@garey1979], - [SAT $arrow.r$ DominatingSet], [$O(3n + m)$], [@garey1979], - [SAT $arrow.l.r$ $k$-SAT], [$O(sum_j |C_j|)$], [@cook1971 @garey1979], - [CircuitSAT $arrow.r$ SpinGlass], [$O(|"gates"|)$], [@whitfield2012 @lucas2014], - [Factoring $arrow.r$ CircuitSAT], [$O(m n)$], [Folklore], - [SpinGlass $arrow.l.r$ MaxCut], [$O(n + |J|)$], [@barahona1982 @lucas2014], - table.cell(fill: gray)[Coloring $arrow.r$ ILP], table.cell(fill: gray)[$O(|V| dot k + |E| dot k)$], table.cell(fill: gray)[—], - table.cell(fill: gray)[Factoring $arrow.r$ ILP], table.cell(fill: gray)[$O(m n)$], table.cell(fill: gray)[—], - table.cell(fill: gray)[IS $arrow.r$ ILP], table.cell(fill: gray)[$O(|V| + |E|)$], table.cell(fill: gray)[—], - table.cell(fill: gray)[VC $arrow.r$ ILP], table.cell(fill: gray)[$O(|V| + |E|)$], table.cell(fill: gray)[—], - table.cell(fill: gray)[Matching $arrow.r$ ILP], table.cell(fill: gray)[$O(|E| + |V|)$], table.cell(fill: gray)[—], - table.cell(fill: gray)[SetPacking $arrow.r$ ILP], table.cell(fill: gray)[$O(|cal(S)|^2)$], table.cell(fill: gray)[—], - table.cell(fill: gray)[SetCovering $arrow.r$ ILP], table.cell(fill: gray)[$O(|cal(S)| + |U|)$], table.cell(fill: gray)[—], - table.cell(fill: gray)[DominatingSet $arrow.r$ ILP], table.cell(fill: gray)[$O(|V| + |E|)$], table.cell(fill: gray)[—], - table.cell(fill: gray)[Clique $arrow.r$ ILP], table.cell(fill: gray)[$O(|V| + |overline(E)|)$], table.cell(fill: gray)[—], - [IS $arrow.r$ GridGraph IS], [$O(n^2)$], [@nguyen2023], - ), - caption: [Summary of reductions. Gray rows indicate trivial (complement/isomorphism) reductions.] -) - +#pagebreak() #bibliography("references.bib", style: "ieee") diff --git a/docs/plans/2026-02-10-improve-example-instances-impl.md b/docs/plans/2026-02-10-improve-example-instances-impl.md new file mode 100644 index 00000000..5ae27e55 --- /dev/null +++ b/docs/plans/2026-02-10-improve-example-instances-impl.md @@ -0,0 +1,708 @@ +# Improve Example Instances — Implementation Plan + +> **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task. + +**Goal:** Replace trivial instances (P4, K3, 2-3 variable SAT) in all 30 reduction examples with non-trivial instances (Petersen graph, 5-variable SAT, etc.) to produce better data for the paper. + +**Architecture:** Each example file is independent. We swap the instance construction code, update doc comments and print statements, then re-run to regenerate JSON. The code structure (reduce → solve → extract → export) stays identical. We use the existing `petersen()` and `octahedral()` helpers from `src/topology/small_graphs.rs`. + +**Tech Stack:** Rust, `problemreductions` crate, `small_graphs` module, BruteForce/ILPSolver + +--- + +## Shared Constants + +These concrete instances are referenced across multiple tasks. + +### Petersen Graph +```rust +use problemreductions::topology::small_graphs::petersen; +let (num_vertices, edges) = petersen(); +// 10 vertices, 15 edges, 3-regular, MIS=4, VC=6, Matching=5, DomSet=3, χ=3 +``` + +### Octahedron +```rust +use problemreductions::topology::small_graphs::octahedral; +let (num_vertices, edges) = octahedral(); +// 6 vertices, 12 edges, K_{2,2,2}, Clique=3 +``` + +### 3-SAT Instance (5 variables, 7 clauses) +```rust +let sat = Satisfiability::::new( + 5, + vec![ + CNFClause::new(vec![1, 2, -3]), // x1 ∨ x2 ∨ ¬x3 + CNFClause::new(vec![-1, 3, 4]), // ¬x1 ∨ x3 ∨ x4 + CNFClause::new(vec![2, -4, 5]), // x2 ∨ ¬x4 ∨ x5 + CNFClause::new(vec![-2, 3, -5]), // ¬x2 ∨ x3 ∨ ¬x5 + CNFClause::new(vec![1, -3, 5]), // x1 ∨ ¬x3 ∨ x5 + CNFClause::new(vec![-1, -2, 4]), // ¬x1 ∨ ¬x2 ∨ x4 + CNFClause::new(vec![3, -4, -5]), // x3 ∨ ¬x4 ∨ ¬x5 + ], +); +``` +**Note:** After implementing, verify this has 2-8 satisfying assignments (not 0 and not all 32). If it has 0 solutions, flip one literal sign. If too many, add a clause. + +### Petersen SpinGlass (frustrated, ±1 couplings) +```rust +use problemreductions::topology::small_graphs::petersen; +let (n, edges) = petersen(); +// Alternating ±1 couplings → frustration on odd cycles +let couplings: Vec<((usize, usize), f64)> = edges.iter().enumerate() + .map(|(i, &(u, v))| ((u, v), if i % 2 == 0 { 1.0 } else { -1.0 })) + .collect(); +let sg = SpinGlass::::new(n, couplings, vec![0.0; n]); +``` + +--- + +## Task 1: MIS → QUBO, ILP, MVC, MSP (4 files) + +**Files:** +- Modify: `examples/reduction_maximumindependentset_to_qubo.rs` +- Modify: `examples/reduction_maximumindependentset_to_ilp.rs` +- Modify: `examples/reduction_maximumindependentset_to_minimumvertexcover.rs` +- Modify: `examples/reduction_maximumindependentset_to_maximumsetpacking.rs` + +**Step 1: Update all 4 files** + +In each file, replace the graph construction with: +```rust +use problemreductions::topology::small_graphs::petersen; + +// Petersen graph: 10 vertices, 15 edges, 3-regular +let (num_vertices, edges) = petersen(); +let is = MaximumIndependentSet::::new(num_vertices, edges.clone()); +``` + +Replace the old: +```rust +let edges = vec![(0, 1), (1, 2), (2, 3)]; +let is = MaximumIndependentSet::::new(4, edges.clone()); +``` + +Update doc comments: +- `//! - Instance: Petersen graph with 10 vertices and 15 edges` +- `//! - Source: MaximumIndependentSet with maximum size 4` +- `//! - QUBO variables: 10` (for the QUBO example) + +Update print statements to say "Petersen graph" instead of "path P4". + +**Step 2: Run all 4 examples to verify** + +```bash +cargo run --all-features --example reduction_maximumindependentset_to_qubo +cargo run --all-features --example reduction_maximumindependentset_to_ilp +cargo run --all-features --example reduction_maximumindependentset_to_minimumvertexcover +cargo run --all-features --example reduction_maximumindependentset_to_maximumsetpacking +``` + +Expected: Each prints solutions with MIS size 4. No panics. + +**Step 3: Commit** + +```bash +git add examples/reduction_maximumindependentset_*.rs +git commit -m "examples: use Petersen graph for MIS reductions" +``` + +--- + +## Task 2: MVC → ILP, QUBO, MIS, MSC (4 files) + +**Files:** +- Modify: `examples/reduction_minimumvertexcover_to_ilp.rs` +- Modify: `examples/reduction_minimumvertexcover_to_qubo.rs` +- Modify: `examples/reduction_minimumvertexcover_to_maximumindependentset.rs` +- Modify: `examples/reduction_minimumvertexcover_to_minimumsetcovering.rs` + +**Step 1: Update all 4 files** + +Replace graph construction with: +```rust +use problemreductions::topology::small_graphs::petersen; + +let (num_vertices, edges) = petersen(); +let vc = MinimumVertexCover::::new(num_vertices, edges.clone()); +``` + +Replace old C4 `vec![(0, 1), (1, 2), (2, 3), (0, 3)]` or K3 `vec![(0, 1), (1, 2), (0, 2)]`. + +Update doc comments to reference Petersen, VC=6. + +**Step 2: Run all 4 examples** + +```bash +cargo run --all-features --example reduction_minimumvertexcover_to_ilp +cargo run --all-features --example reduction_minimumvertexcover_to_qubo +cargo run --all-features --example reduction_minimumvertexcover_to_maximumindependentset +cargo run --all-features --example reduction_minimumvertexcover_to_minimumsetcovering +``` + +Expected: VC size 6. No panics. + +**Step 3: Commit** + +```bash +git add examples/reduction_minimumvertexcover_*.rs +git commit -m "examples: use Petersen graph for MVC reductions" +``` + +--- + +## Task 3: Matching + DomSet → ILP, MSP (3 files) + +**Files:** +- Modify: `examples/reduction_maximummatching_to_ilp.rs` +- Modify: `examples/reduction_maximummatching_to_maximumsetpacking.rs` +- Modify: `examples/reduction_minimumdominatingset_to_ilp.rs` + +**Step 1: Update all 3 files** + +For Matching (uses `unweighted` constructor): +```rust +use problemreductions::topology::small_graphs::petersen; + +let (num_vertices, edges) = petersen(); +let matching = MaximumMatching::::unweighted(num_vertices, edges.clone()); +``` + +For DominatingSet: +```rust +use problemreductions::topology::small_graphs::petersen; + +let (num_vertices, edges) = petersen(); +let ds = MinimumDominatingSet::::new(num_vertices, edges.clone()); +``` + +Update doc comments: Matching=5 (perfect), DomSet=3. + +**Step 2: Run all 3 examples** + +```bash +cargo run --all-features --example reduction_maximummatching_to_ilp +cargo run --all-features --example reduction_maximummatching_to_maximumsetpacking +cargo run --all-features --example reduction_minimumdominatingset_to_ilp +``` + +Expected: Matching size 5, DomSet size 3. No panics. + +**Step 3: Commit** + +```bash +git add examples/reduction_maximummatching_*.rs examples/reduction_minimumdominatingset_*.rs +git commit -m "examples: use Petersen graph for Matching and DomSet reductions" +``` + +--- + +## Task 4: Coloring + MaxCut (3 files) + +**Files:** +- Modify: `examples/reduction_coloring_to_ilp.rs` +- Modify: `examples/reduction_coloring_to_qubo.rs` +- Modify: `examples/reduction_maxcut_to_spinglass.rs` + +**Step 1: Update Coloring files** + +Petersen has chromatic number 3, so `KColoring::<3, ...>` is correct: +```rust +use problemreductions::topology::small_graphs::petersen; + +let (num_vertices, edges) = petersen(); +let kc = KColoring::<3, SimpleGraph, i32>::new(num_vertices, edges.clone()); +``` + +**IMPORTANT for `coloring_to_qubo`**: KColoring::<3> on Petersen creates a QUBO with 10×3 = 30 variables. BruteForce on 30 variables (2^30 ≈ 1B) is too slow. Either: +- (a) Use a smaller graph for coloring QUBO examples (e.g., `house()` — 5 vertices, χ=3, QUBO=15 vars), or +- (b) Accept slow runtime (~minutes). + +**Recommended**: Use `house()` (5 vertices, 6 edges, χ=3) for `coloring_to_qubo` only. Keep Petersen for `coloring_to_ilp`. + +**Step 1b: Update MaxCut file** + +MaxCut with unit weights on Petersen: +```rust +use problemreductions::topology::small_graphs::petersen; + +let (num_vertices, edges) = petersen(); +let maxcut = MaxCut::::unweighted(num_vertices, edges.clone()); +``` + +**Step 2: Run all 3 examples** + +```bash +cargo run --all-features --example reduction_coloring_to_ilp +cargo run --all-features --example reduction_coloring_to_qubo +cargo run --all-features --example reduction_maxcut_to_spinglass +``` + +Expected: Coloring solutions with 3 colors. MaxCut solution. No panics. Verify `coloring_to_qubo` completes within ~2 minutes. + +**Step 3: Commit** + +```bash +git add examples/reduction_coloring_*.rs examples/reduction_maxcut_*.rs +git commit -m "examples: use Petersen graph for Coloring and MaxCut reductions" +``` + +--- + +## Task 5: MaximumClique → ILP (1 file) + +**Files:** +- Modify: `examples/reduction_maximumclique_to_ilp.rs` + +**Step 1: Update instance** + +```rust +use problemreductions::topology::small_graphs::octahedral; + +// Octahedron: 6 vertices, 12 edges, K_{2,2,2}, clique number = 3 +let (num_vertices, edges) = octahedral(); +let clique = MaximumClique::::new(num_vertices, edges.clone()); +``` + +Update doc comments: "Octahedron graph (K_{2,2,2}) with 6 vertices and 12 edges, max clique size 3." + +**Step 2: Run example** + +```bash +cargo run --all-features --example reduction_maximumclique_to_ilp +``` + +Expected: Clique of size 3. No panics. + +**Step 3: Commit** + +```bash +git add examples/reduction_maximumclique_to_ilp.rs +git commit -m "examples: use octahedron for MaximumClique reduction" +``` + +--- + +## Task 6: Standalone Set Problems (3 files) + +**Files:** +- Modify: `examples/reduction_maximumsetpacking_to_qubo.rs` +- Modify: `examples/reduction_maximumsetpacking_to_ilp.rs` +- Modify: `examples/reduction_minimumsetcovering_to_ilp.rs` + +**Step 1: Update instances** + +These are standalone set problems (not derived from graph reductions). Replace the trivial 3-set instances with 6 sets over 8 elements: + +For MaximumSetPacking: +```rust +let sets = vec![ + vec![0, 1, 2], // S0 + vec![2, 3, 4], // S1 (overlaps S0 at 2) + vec![4, 5, 6], // S2 (overlaps S1 at 4) + vec![6, 7, 0], // S3 (overlaps S2 at 6, S0 at 0) + vec![1, 3, 5], // S4 (overlaps S0,S1,S2) + vec![0, 4, 7], // S5 (overlaps S0,S1,S3) +]; +let sp = MaximumSetPacking::::new(sets.clone()); +``` + +For MinimumSetCovering (same 6 sets, universe size 8): +```rust +let sets = vec![ + vec![0, 1, 2], + vec![2, 3, 4], + vec![4, 5, 6], + vec![6, 7, 0], + vec![1, 3, 5], + vec![0, 4, 7], +]; +let sc = MinimumSetCovering::::new(8, sets.clone()); +``` + +**Step 2: Run all 3 examples** + +```bash +cargo run --all-features --example reduction_maximumsetpacking_to_qubo +cargo run --all-features --example reduction_maximumsetpacking_to_ilp +cargo run --all-features --example reduction_minimumsetcovering_to_ilp +``` + +Expected: MSP finds max packing (disjoint sets), MSC finds min covering. No panics. + +**IMPORTANT for `msp_to_qubo`**: SetPacking with 6 sets → QUBO with 6 variables. BruteForce on 6 vars is instant. Good. + +**Step 3: Commit** + +```bash +git add examples/reduction_maximumsetpacking_*.rs examples/reduction_minimumsetcovering_to_ilp.rs +git commit -m "examples: use 6-set instances for SetPacking and SetCovering" +``` + +--- + +## Task 7: SAT → MIS, Coloring, DomSet, kSAT (4 files) + +**Files:** +- Modify: `examples/reduction_sat_to_maximumindependentset.rs` +- Modify: `examples/reduction_sat_to_coloring.rs` +- Modify: `examples/reduction_sat_to_minimumdominatingset.rs` +- Modify: `examples/reduction_sat_to_ksat.rs` + +**Step 1: Update all 4 files** + +Replace the SAT construction with the shared 3-SAT instance (see Shared Constants above). Use the exact same formula in all 4 files: +```rust +let sat = Satisfiability::::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]), + ], +); +``` + +Update doc comments to reference "5-variable, 7-clause 3-SAT formula". + +**IMPORTANT**: For `sat_to_mis`, the target MIS graph has 7×3 = 21 vertices. BruteForce on 21 variables (2^21 ≈ 2M) is fast. For `sat_to_coloring`, the target has more variables (2×5 + 7×3 = 31 — too slow for BruteForce). If `sat_to_coloring` is too slow, reduce to 5 clauses instead of 7. For `sat_to_mds`, check the target variable count similarly. + +Run each example and verify it completes within ~30 seconds. If any is too slow, trim the formula to fewer clauses for that specific example. + +**Step 2: Run all 4 examples** + +```bash +cargo run --all-features --example reduction_sat_to_maximumindependentset +cargo run --all-features --example reduction_sat_to_coloring +cargo run --all-features --example reduction_sat_to_minimumdominatingset +cargo run --all-features --example reduction_sat_to_ksat +``` + +Expected: SAT solutions found, reductions verified. No panics. + +**Step 3: Commit** + +```bash +git add examples/reduction_sat_*.rs +git commit -m "examples: use 5-variable 3-SAT instance for SAT reductions" +``` + +--- + +## Task 8: kSAT → QUBO (1 file) + +**Files:** +- Modify: `examples/reduction_ksatisfiability_to_qubo.rs` + +**Step 1: Update instance** + +Use the same 3-SAT formula but as `KSatisfiability::<3, i32>`: +```rust +let clauses = 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]), +]; +let ksat = KSatisfiability::<3, i32>::new(5, clauses); +``` + +**IMPORTANT**: kSAT → QUBO creates auxiliary variables. Check that the QUBO has ≤ ~25 variables. If too many, reduce to fewer clauses. + +**Step 2: Run example** + +```bash +cargo run --all-features --example reduction_ksatisfiability_to_qubo +``` + +Expected: QUBO solutions found, kSAT verified. No panics. Completes within ~1 minute. + +**Step 3: Commit** + +```bash +git add examples/reduction_ksatisfiability_to_qubo.rs +git commit -m "examples: use 5-variable 3-SAT instance for kSAT-to-QUBO" +``` + +--- + +## Task 9: SpinGlass ↔ QUBO ↔ MaxCut (3 files) + +**Files:** +- Modify: `examples/reduction_spinglass_to_qubo.rs` +- Modify: `examples/reduction_qubo_to_spinglass.rs` +- Modify: `examples/reduction_spinglass_to_maxcut.rs` + +**Step 1: Update SpinGlass → QUBO and SpinGlass → MaxCut** + +Both start with a SpinGlass instance. Use the Petersen SpinGlass (see Shared Constants): +```rust +use problemreductions::topology::small_graphs::petersen; + +let (n, edges) = petersen(); +let couplings: Vec<((usize, usize), f64)> = edges.iter().enumerate() + .map(|(i, &(u, v))| ((u, v), if i % 2 == 0 { 1.0 } else { -1.0 })) + .collect(); +let sg = SpinGlass::::new(n, couplings, vec![0.0; n]); +``` + +For `spinglass_to_maxcut`, use `i32` weights instead of `f64`: +```rust +let couplings: Vec<((usize, usize), i32)> = edges.iter().enumerate() + .map(|(i, &(u, v))| ((u, v), if i % 2 == 0 { 1 } else { -1 })) + .collect(); +let sg = SpinGlass::::new(n, couplings, vec![0; n]); +``` + +**Step 1b: Update QUBO → SpinGlass** + +Create a 10-variable QUBO directly. Use a sparse upper-triangular matrix on Petersen edges: +```rust +use problemreductions::topology::small_graphs::petersen; + +let (n, edges) = petersen(); +let mut matrix = vec![vec![0.0; n]; n]; +// Diagonal: linear terms +for i in 0..n { + matrix[i][i] = -1.0 + 0.2 * i as f64; +} +// Off-diagonal: quadratic terms on Petersen edges +for (idx, &(u, v)) in edges.iter().enumerate() { + let (i, j) = if u < v { (u, v) } else { (v, u) }; + matrix[i][j] = if idx % 2 == 0 { 2.0 } else { -1.5 }; +} +let qubo = QUBO::from_matrix(matrix.clone()); +``` + +**Step 2: Run all 3 examples** + +```bash +cargo run --all-features --example reduction_spinglass_to_qubo +cargo run --all-features --example reduction_qubo_to_spinglass +cargo run --all-features --example reduction_spinglass_to_maxcut +``` + +Expected: Solutions found, round-trip verified. No panics. + +**Step 3: Commit** + +```bash +git add examples/reduction_spinglass_*.rs examples/reduction_qubo_to_spinglass.rs +git commit -m "examples: use Petersen topology for SpinGlass/QUBO/MaxCut" +``` + +--- + +## Task 10: ILP → QUBO (1 file) + +**Files:** +- Modify: `examples/reduction_ilp_to_qubo.rs` + +**Step 1: Update instance** + +Replace the trivial 3-variable ILP with a 6-variable binary knapsack: +```rust +let ilp = ILP::binary( + 6, + vec![ + // Knapsack weight constraint: 3x0 + 2x1 + 5x2 + 4x3 + 2x4 + 3x5 ≤ 10 + LinearConstraint::le( + vec![(0, 3.0), (1, 2.0), (2, 5.0), (3, 4.0), (4, 2.0), (5, 3.0)], + 10.0, + ), + // Category limit: x0 + x1 + x2 ≤ 2 + LinearConstraint::le(vec![(0, 1.0), (1, 1.0), (2, 1.0)], 2.0), + // Category limit: x3 + x4 + x5 ≤ 2 + LinearConstraint::le(vec![(3, 1.0), (4, 1.0), (5, 1.0)], 2.0), + ], + vec![(0, 10.0), (1, 7.0), (2, 12.0), (3, 8.0), (4, 6.0), (5, 9.0)], + ObjectiveSense::Maximize, +); +``` + +**IMPORTANT**: ILP → QUBO adds slack variables. Check the QUBO has ≤ ~25 variables. If too many, reduce the RHS of the knapsack constraint (fewer slack bits needed). + +**Step 2: Run example** + +```bash +cargo run --all-features --example reduction_ilp_to_qubo +``` + +Expected: QUBO solution extracts to a valid knapsack solution. No panics. + +**Step 3: Commit** + +```bash +git add examples/reduction_ilp_to_qubo.rs +git commit -m "examples: use 6-variable knapsack for ILP-to-QUBO" +``` + +--- + +## Task 11: CircuitSAT → SpinGlass (1 file) + +**Files:** +- Modify: `examples/reduction_circuit_to_spinglass.rs` + +**Step 1: Update instance** + +Replace the single AND gate with a full adder circuit (1-bit addition with carry): +```rust +use problemreductions::models::specialized::Circuit; + +// Full adder: inputs a, b, cin → outputs sum, cout +// sum = a XOR b XOR cin +// cout = (a AND b) OR (cin AND (a XOR b)) +let circuit = Circuit::new(vec![ + // Intermediate: t = a XOR b + Assignment::new( + vec!["t".to_string()], + BooleanExpr::xor(vec![BooleanExpr::var("a"), BooleanExpr::var("b")]), + ), + // sum = t XOR cin + Assignment::new( + vec!["sum".to_string()], + BooleanExpr::xor(vec![BooleanExpr::var("t"), BooleanExpr::var("cin")]), + ), + // ab = a AND b + Assignment::new( + vec!["ab".to_string()], + BooleanExpr::and(vec![BooleanExpr::var("a"), BooleanExpr::var("b")]), + ), + // cin_t = cin AND t + Assignment::new( + vec!["cin_t".to_string()], + BooleanExpr::and(vec![BooleanExpr::var("cin"), BooleanExpr::var("t")]), + ), + // cout = ab OR cin_t + Assignment::new( + vec!["cout".to_string()], + BooleanExpr::or(vec![BooleanExpr::var("ab"), BooleanExpr::var("cin_t")]), + ), +]); +let circuit_sat = CircuitSAT::::new(circuit); +``` + +This gives ~7 variables (a, b, cin, t, sum, ab, cin_t, cout). BruteForce on 8 variables is instant. + +**Step 2: Run example** + +```bash +cargo run --all-features --example reduction_circuit_to_spinglass +``` + +Expected: SpinGlass solutions found. No panics. + +**Step 3: Commit** + +```bash +git add examples/reduction_circuit_to_spinglass.rs +git commit -m "examples: use full adder circuit for CircuitSAT-to-SpinGlass" +``` + +--- + +## Task 12: Factoring → Circuit, ILP (2 files) + +**Files:** +- Modify: `examples/reduction_factoring_to_circuit.rs` +- Modify: `examples/reduction_factoring_to_ilp.rs` + +**Step 1: Update instances** + +Replace `Factoring::new(2, 2, 6)` and `Factoring::new(4, 4, 15)` with: +```rust +let factoring = Factoring::new(3, 3, 35); +// Factor 35 = 5 × 7, 3-bit factors, 6 binary variables +``` + +For `factoring_to_circuit.rs`: update the variable name format strings. The current code uses `format!("p{}", i + 1)` and `format!("q{}", i + 1)` which should still work for 3-bit factors. + +Update doc comments: "Factor 35 = 5 × 7 (m=3 bits, n=3 bits)". + +For `factoring_to_ilp.rs`: the ILPSolver is used (not BruteForce). This should handle 3×3 fine. + +**Step 2: Run both examples** + +```bash +cargo run --all-features --example reduction_factoring_to_circuit +cargo run --all-features --example reduction_factoring_to_ilp +``` + +Expected: Finds factors 5 and 7 (and 7 and 5). No panics. + +**Step 3: Commit** + +```bash +git add examples/reduction_factoring_*.rs +git commit -m "examples: use factoring 35=5×7 for Factoring reductions" +``` + +--- + +## Task 13: Regenerate JSON and Full Verification + +**Files:** +- All `docs/paper/examples/*.json` and `*.result.json` (auto-generated) + +**Step 1: Run all examples to regenerate JSON** + +```bash +make examples +``` + +If no `make examples` target exists, run manually: +```bash +for ex in $(ls examples/reduction_*.rs | sed 's|examples/||;s|\.rs||'); do + cargo run --all-features --example "$ex" +done +``` + +**Step 2: Run full test suite** + +```bash +make test +``` + +Expected: All tests pass. The QUBO ground truth tests in `tests/data/qubo/` use different instances than the examples, so they should not be affected. + +**Step 3: Run clippy** + +```bash +make clippy +``` + +Expected: No warnings. + +**Step 4: Verify JSON files updated** + +```bash +git diff --stat docs/paper/examples/ +``` + +Expected: All 60 JSON files (30 × `.json` + 30 × `.result.json`) show changes. + +**Step 5: Commit generated files** + +```bash +git add docs/paper/examples/ +git commit -m "chore: regenerate example JSON with improved instances" +``` + +--- + +## Parallel Execution Groups + +Tasks 1-12 are independent and can run in parallel. Task 13 depends on all others completing. + +**Group A (graph, can run in parallel):** Tasks 1, 2, 3, 4, 5 +**Group B (non-graph, can run in parallel):** Tasks 6, 7, 8, 9, 10, 11, 12 +**Group C (verification, sequential after A+B):** Task 13 diff --git a/docs/plans/2026-02-10-improve-example-instances.md b/docs/plans/2026-02-10-improve-example-instances.md new file mode 100644 index 00000000..b5b08ca4 --- /dev/null +++ b/docs/plans/2026-02-10-improve-example-instances.md @@ -0,0 +1,94 @@ +# Improve Example Instances + +**Date**: 2026-02-10 +**Branch**: TBD +**Status**: Design approved + +## Problem + +All 30 reduction examples use trivially small instances (P4 path graph, K3 triangle, 2-3 variable SAT formulas). The P4 path graph alone appears in 8 examples. These produce unserious-looking data for the paper and don't illustrate interesting reduction behavior. + +## Design Decisions + +- **Purpose**: Examples are primarily data generators for the Typst paper (JSON export) +- **Size range**: 6-10 variables per instance +- **Strategy**: One canonical graph (Petersen) for all graph problems, with exceptions only where necessary +- **Solver**: BruteForce, so target problem must have ≤ ~25 variables + +## Instance Plan + +### 1. Petersen Graph (10 vertices, 15 edges) + +Canonical graph for all graph-based problems. 3-regular, non-bipartite, girth 5. + +**Properties**: MIS=4, VC=6, Matching=5 (perfect), DominatingSet=3, ChromaticNumber=3, Clique=2. + +**Edge list**: `(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)` + +**Used by** (20 examples): +- `mis_to_qubo`, `mis_to_ilp`, `mis_to_mvc`, `mis_to_msp` +- `mvc_to_ilp`, `mvc_to_qubo`, `mvc_to_mis`, `mvc_to_msc` +- `mm_to_ilp`, `mm_to_msp` +- `mds_to_ilp` +- `coloring_to_ilp`, `coloring_to_qubo` +- `maxcut_to_spinglass` +- `spinglass_to_maxcut` (MaxCut on Petersen topology) + +### 2. Octahedron (6 vertices, 12 edges) + +For MaximumClique example. Complete tripartite K_{2,2,2}. Clique number = 3. + +**Used by**: `mclique_to_ilp` + +### 3. Random 3-SAT (5 variables, ~7 clauses) + +Hand-picked instance with ~2-4 satisfying assignments. Ratio ~1.4. Compact enough to display inline in the paper. Target MIS graph has 21 vertices (BruteForce feasible). + +**Used by** (4 examples): +- `sat_to_mis`, `sat_to_coloring`, `sat_to_mds`, `sat_to_ksat` + +### 4. Petersen SpinGlass (10 spins, 15 couplings) + +SpinGlass on Petersen graph topology with random ±1 couplings (frustrated). Shared between SpinGlass ↔ QUBO ↔ MaxCut conversions. + +**Used by** (3 examples): +- `spinglass_to_qubo`, `spinglass_to_maxcut`, `qubo_to_spinglass` + +### 5. Knapsack/Assignment ILP (6-8 variables) + +Proper knapsack or assignment problem with non-trivial constraints and slack variables. + +**Used by**: `ilp_to_qubo` + +### 6. 2-bit Adder Circuit + +Multi-gate circuit (replaces single AND gate). Shows meaningful CircuitSAT structure. + +**Used by**: `circuit_to_spinglass` + +### 7. Factor 35 = 5 x 7 (3-bit x 3-bit) + +Product of two primes, 6 binary variables. BruteForce feasible (2^6 = 64). + +**Used by** (2 examples): +- `factoring_to_circuit`, `factoring_to_ilp` + +### 8. 5-variable 3-SAT (reused from #3) + +Same SAT instance used for kSAT → QUBO. + +**Used by**: `ksatisfiability_to_qubo` + +## Paper Display + +For Petersen-based reductions producing 10x10 QUBO matrices: show as compact figures rather than inline matrices, or show key properties (dimension, sparsity, penalty weight) instead of full matrix. + +## Scope + +Only instance data changes. The example structure (create -> reduce -> solve -> extract -> export JSON) stays the same. No API changes. + +## Verification + +```bash +make test clippy export-graph +``` diff --git a/docs/src/claude.md b/docs/src/claude.md deleted file mode 120000 index 7afdfd5f..00000000 --- a/docs/src/claude.md +++ /dev/null @@ -1 +0,0 @@ -../../.claude/CLAUDE.md \ No newline at end of file diff --git a/docs/src/claude.md b/docs/src/claude.md new file mode 100644 index 00000000..5ec03224 --- /dev/null +++ b/docs/src/claude.md @@ -0,0 +1,99 @@ +# CLAUDE.md + +## Project Overview +Rust library for NP-hard problem reductions. Implements computational problems with reduction rules for transforming between equivalent formulations. + +## Commands +```bash +make help # Show all available targets +make build # Build the project +make test # Run all tests +make fmt # Format code with rustfmt +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 coverage # Generate coverage report (>95% required) +make check # Quick pre-commit check (fmt + clippy + test) +make export-graph # Regenerate reduction graph JSON +make export-schemas # Regenerate problem schemas JSON +make qubo-testdata # Regenerate QUBO ground truth JSON +make clean # Clean build artifacts +``` + +## Verify Changes +```bash +make test clippy export-graph # Must pass before PR +``` + +## Architecture + +### Core Modules +- `src/models/` - Problem implementations (SAT, Graph, Set, Optimization) +- `src/rules/` - Reduction rules + inventory registration +- `src/solvers/` - BruteForce solver, ILP solver (feature-gated) +- `src/traits.rs` - `Problem`, `ConstraintSatisfactionProblem` traits +- `src/rules/traits.rs` - `ReduceTo`, `ReductionResult` traits +- `src/registry/` - Compile-time reduction metadata collection +- `src/unit_tests/` - Unit test files (mirroring `src/` structure, referenced via `#[path]`) +- `tests/main.rs` - Integration tests (modules in `tests/suites/`) +- `tests/data/` - Ground truth JSON for integration tests +- `scripts/` - Python test data generation scripts (managed with `uv`) +- `docs/plans/` - Implementation plans + +### Trait Hierarchy + +``` +Problem (core trait - all problems must implement) +│ +├── const NAME: &'static str // Problem name, e.g., "MaximumIndependentSet" +├── type GraphType: GraphMarker // Graph topology marker +├── type Weight: NumericWeight // Weight type (i32, f64, Unweighted) +├── type Size // Objective value type +│ +├── fn num_variables(&self) -> usize +├── fn num_flavors(&self) -> usize // Usually 2 for binary problems +├── fn problem_size(&self) -> ProblemSize +├── fn energy_mode(&self) -> EnergyMode +├── fn solution_size(&self, config) -> SolutionSize +└── ... (default methods: variables, flavors, is_valid_config) + +ConstraintSatisfactionProblem : Problem (extension for CSPs) +│ +├── fn constraints(&self) -> Vec +├── fn objectives(&self) -> Vec +├── fn weights(&self) -> Vec +├── fn set_weights(&mut self, weights) +├── fn is_weighted(&self) -> bool +└── ... (default methods: is_satisfied, compute_objective) +``` + +### Key Patterns +- Problems parameterized by weight type `W` and graph type `G` +- `ReductionResult` provides `target_problem()` and `extract_solution()` +- Graph types: SimpleGraph, GridGraph, UnitDiskGraph, Hypergraph +- Weight types: `Unweighted` (marker), `i32`, `f64` + +### Problem Variant IDs +Reduction graph nodes use variant IDs: `ProblemName[/GraphType][/Weighted]` +- Base: `MaximumIndependentSet` (SimpleGraph, unweighted) +- Graph variant: `MaximumIndependentSet/GridGraph` +- Weighted variant: `MaximumIndependentSet/Weighted` +- Both: `MaximumIndependentSet/GridGraph/Weighted` + +## Conventions + +### File Naming +- Reduction files: `src/rules/_.rs` +- Model files: `src/models//.rs` +- Test naming: `test__to__closed_loop` + +## Contributing +See `.claude/rules/` for detailed guides: +- `adding-reductions.md` - How to add reduction rules +- `adding-models.md` - How to add problem types +- `testing.md` - Testing requirements and patterns +- `documentation.md` - Paper documentation patterns + +Also see GitHub Issue #3 for coding rules. diff --git a/docs/src/getting-started.md b/docs/src/getting-started.md index fd741e3b..f8731b3b 100644 --- a/docs/src/getting-started.md +++ b/docs/src/getting-started.md @@ -17,10 +17,10 @@ problemreductions = "0.1" use problemreductions::prelude::*; // Independent Set on a path graph -let is = IndependentSet::::new(4, vec![(0, 1), (1, 2), (2, 3)]); +let is = MaximumIndependentSet::::new(4, vec![(0, 1), (1, 2), (2, 3)]); // Vertex Cover on the same graph -let vc = VertexCovering::::new(4, vec![(0, 1), (1, 2), (2, 3)]); +let vc = MinimumVertexCover::::new(4, vec![(0, 1), (1, 2), (2, 3)]); // QUBO problem let qubo = QUBO::from_matrix(vec![ @@ -34,7 +34,7 @@ let qubo = QUBO::from_matrix(vec![ ```rust use problemreductions::prelude::*; -let problem = IndependentSet::::new(4, vec![(0, 1), (1, 2), (2, 3)]); +let problem = MaximumIndependentSet::::new(4, vec![(0, 1), (1, 2), (2, 3)]); let solver = BruteForce::new(); let solutions = solver.find_best(&problem); @@ -50,10 +50,10 @@ for sol in &solutions { use problemreductions::prelude::*; // Create an Independent Set problem -let is = IndependentSet::::new(4, vec![(0, 1), (1, 2)]); +let is = MaximumIndependentSet::::new(4, vec![(0, 1), (1, 2)]); // Reduce to Vertex Cover -let result = ReduceTo::>::reduce_to(&is); +let result = ReduceTo::>::reduce_to(&is); let vc = result.target_problem(); // Solve the reduced problem @@ -69,17 +69,17 @@ let is_solution = result.extract_solution(&vc_solutions[0]); ```rust use problemreductions::prelude::*; -let sp = SetPacking::::new(vec![ +let sp = MaximumSetPacking::::new(vec![ vec![0, 1], vec![1, 2], vec![2, 3], ]); -// SetPacking -> IndependentSet -> VertexCovering -let sp_to_is = ReduceTo::>::reduce_to(&sp); +// MaximumSetPacking -> MaximumIndependentSet -> MinimumVertexCover +let sp_to_is = ReduceTo::>::reduce_to(&sp); let is = sp_to_is.target_problem(); -let is_to_vc = ReduceTo::>::reduce_to(is); +let is_to_vc = ReduceTo::>::reduce_to(is); let vc = is_to_vc.target_problem(); // Solve and extract back through the chain @@ -94,8 +94,8 @@ let sp_solution = sp_to_is.extract_solution(&is_solution); The reduction system is compile-time verified. Invalid reductions won't compile: ```rust,compile_fail -// This won't compile - no reduction from QUBO to SetPacking -let result = ReduceTo::>::reduce_to(&qubo); +// This won't compile - no reduction from QUBO to MaximumSetPacking +let result = ReduceTo::>::reduce_to(&qubo); ``` ## Next Steps diff --git a/docs/src/introduction.md b/docs/src/introduction.md index c7bc7e61..427d166b 100644 --- a/docs/src/introduction.md +++ b/docs/src/introduction.md @@ -4,15 +4,15 @@ A Rust library for reducing NP-hard problems. ## Overview -**problemreductions** provides implementations of various NP-hard computational problems and reduction rules between them. It is designed for algorithm research, education, and quantum optimization studies. +**problemreductions** provides implementations of various computational hard problems and reduction rules between them. It is designed for algorithm research, education, and quantum optimization studies. For theoretical background and correctness proofs, see the [PDF manual](https://codingthrust.github.io/problem-reductions/reductions.pdf). ## Reduction Graph -
+
-
+
Graph Set Optimization @@ -20,14 +20,14 @@ For theoretical background and correctness proofs, see the [PDF manual](https:// Specialized
- Click a node to start path selection + Click a node to start path selection
-
- Click two nodes to find a reduction path. Double-click a node to view its API docs. Scroll to zoom, drag to pan. +
+ Click two variant nodes to find a reduction path. Double-click a node for API docs, double-click an edge for source code. Scroll to zoom, drag to pan.
- +