diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 5cc9c9eb..255f9ec4 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -97,8 +97,9 @@ Reduction graph nodes use variant IDs: `ProblemName[/GraphType][/Weighted]` - 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 +- `problem-def(name)[body]` — defines a problem with auto-generated schema, reductions list, and label ``. Title comes from `display-name` dict. +- `reduction-rule(source, target, example: bool, ...)[rule][proof]` — generates a theorem with label `` and registers in `covered-rules` state. Overhead auto-derived from JSON edge data. +- Every directed reduction needs its own `reduction-rule` entry - Completeness warnings auto-check that all JSON graph nodes/edges are covered in the paper - `display-name` dict maps `ProblemName` to display text diff --git a/.claude/rules/adding-models.md b/.claude/rules/adding-models.md index fd98a957..01a44537 100644 --- a/.claude/rules/adding-models.md +++ b/.claude/rules/adding-models.md @@ -5,55 +5,23 @@ paths: # Adding a Model (Problem Type) -## 1. Define the Model -Create `src/models//.rs`: - -```rust -use serde::{Deserialize, Serialize}; -use crate::traits::{Problem, ProblemSize}; - -#[derive(Clone, Debug, Serialize, Deserialize)] -pub struct MyProblem { - // Problem data fields - pub size: usize, - pub weights: Vec, - // ... -} - -impl Problem for MyProblem { - fn num_variables(&self) -> usize { ... } - fn problem_size(&self) -> ProblemSize { ... } - fn is_valid_solution(&self, solution: &[usize]) -> bool { ... } -} -``` - -## 2. Register in Module -Add to `src/models//mod.rs`: -```rust -mod my_problem; -pub use my_problem::MyProblem; -``` - -## 3. Categories -Place models in appropriate category: -- `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 -- `Serialize`, `Deserialize` - JSON I/O support -- `Clone`, `Debug` - Standard Rust traits -- `Problem` - Core trait with `num_variables()`, `problem_size()`, `is_valid_solution()` -- Consider `ConstraintSatisfactionProblem` if applicable - -## 5. Naming -Use explicit optimization prefixes: `Maximum` for maximization, `Minimum` for minimization (e.g., `MaximumIndependentSet`, `MinimumVertexCover`). +**Reference implementation:** `src/models/graph/kcoloring.rs` + +## Steps + +1. **Create** `src/models//.rs` — follow the reference for struct definition, `Problem` impl, and optionally `ConstraintSatisfactionProblem` impl. +2. **Register** in `src/models//mod.rs`. +3. **Add tests** in `src/unit_tests/models//.rs` (linked via `#[path]`). +4. **Document** in `docs/paper/reductions.typ`: add `display-name` entry and `#problem-def("Name")[definition...]`. -## 6. Documentation -Document in `docs/paper/reductions.typ` using `#problem-def("ProblemName", "Display Title")[...]` +## Categories -## Anti-patterns -- Don't create models without JSON serialization support -- Don't forget to implement `is_valid_solution()` correctly -- Don't use concrete types when generic `W` is appropriate +- `src/models/satisfiability/` — Satisfiability, KSatisfiability, CircuitSAT +- `src/models/graph/` — MaximumIndependentSet, MinimumVertexCover, KColoring, etc. +- `src/models/set/` — MinimumSetCovering, MaximumSetPacking +- `src/models/optimization/` — SpinGlass, QUBO, ILP +- `src/models/specialized/` — Factoring + +## Naming + +Use explicit optimization prefixes: `Maximum` for maximization, `Minimum` for minimization (e.g., `MaximumIndependentSet`, `MinimumVertexCover`). diff --git a/.claude/rules/adding-reductions.md b/.claude/rules/adding-reductions.md index b92664b5..30c59e62 100644 --- a/.claude/rules/adding-reductions.md +++ b/.claude/rules/adding-reductions.md @@ -3,104 +3,45 @@ paths: - "src/rules/**/*.rs" --- -# Adding a Reduction Rule (A → B) +# Adding a Reduction Rule (A -> B) -## 0. Brainstorm & Generate Test Data First +**Reference implementation:** `src/rules/minimumvertexcover_maximumindependentset.rs` +**Reference test:** `src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs` +**Reference example:** `examples/reduction_minimumvertexcover_to_maximumindependentset.rs` +**Reference paper entry:** `docs/paper/reductions.typ` (search for `MinimumVertexCover` `MaximumIndependentSet`) -Before writing any Rust code, follow this workflow: +## 0. Before Writing Code -1. **Brainstorm the reduction** — use `superpowers:brainstorming` to discuss with the user: - - Research the mathematical formulation (paper, textbook, or derive it) - - Understand the variable mapping and constraint encoding - - Discuss implementation approach: penalty values, matrix construction, solution extraction - - Read reference implementations in the codebase (e.g., `src/rules/spinglass_qubo.rs`) to understand conventions - - Agree on scope (weighted vs unweighted, specific graph types, const generics) -2. **Generate ground truth test data** — use an existing library (e.g., Python with qubogen, qubovert, or networkx) to create small instances, reduce them, brute-force solve both sides, and export as JSON to `tests/data//`. It is recommended to download the relevant package and check the existing tests to understand how to construct tests. To generate the test data, you can use the following command: - ```bash - # 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 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. **Brainstorm** — use `superpowers:brainstorming` to discuss with the user: + - The math (variable mapping, constraint encoding, penalty terms) + - Which example instance to use in `examples/` (must be small, human-explainable, and agreed with the user) +2. **Generate ground truth** — use Python scripts in `scripts/` (run with `uv`) to create test data in `tests/data//`. +3. **Write plan** — save to `docs/plans/` using `superpowers:writing-plans`. -## 1. Implementation +## 1. Implement -Create `src/rules/_.rs` following the pattern in `src/rules/spinglass_qubo.rs`: +Create `src/rules/_.rs` following the reference. Key pieces: +- `ReductionResult` struct + impl (`target_problem`, `extract_solution`, `source_size`, `target_size`) +- `#[reduction(...)]` macro on `ReduceTo for Source` impl (auto-generates `inventory::submit!`) +- `#[cfg(test)] #[path = ...]` linking to unit tests -```rust -use crate::reduction; +Register in `src/rules/mod.rs`. -#[derive(Debug, Clone)] -pub struct ReductionSourceToTarget { - target: TargetProblem<...>, - source_size: ProblemSize, - // + any metadata needed for extract_solution -} +## 2. Test -impl ReductionResult for ReductionSourceToTarget { - type Source = SourceProblem<...>; - type Target = TargetProblem<...>; - - fn target_problem(&self) -> &Self::Target { &self.target } - fn extract_solution(&self, target_solution: &[usize]) -> Vec { ... } - fn source_size(&self) -> ProblemSize { self.source_size.clone() } - fn target_size(&self) -> ProblemSize { self.target.problem_size() } -} - -#[reduction( - overhead = { ReductionOverhead::new(vec![...]) } -)] -impl ReduceTo> for SourceProblem<...> { - type Result = ReductionSourceToTarget; - fn reduce_to(&self) -> Self::Result { ... } -} - -#[cfg(test)] -#[path = "../unit_tests/rules/_.rs"] -mod tests; -``` - -The `#[reduction]` macro auto-generates the `inventory::submit!` call. Optional attributes: `source_graph`, `target_graph`, `source_weighted`, `target_weighted`. - -Register module in `src/rules/mod.rs`: -```rust -mod source_target; -pub use source_target::ReductionSourceToTarget; -``` - -## 2. Tests (Required) - -- **Unit tests** in `src/unit_tests/rules/_.rs` — closed-loop + edge cases. See `rules/testing.md`. -- **Integration tests** in `tests/suites/reductions.rs` — compare against JSON ground truth from step 0. -- Test name: `test__to__closed_loop` +- **Unit tests** in `src/unit_tests/rules/_.rs` — closed-loop + edge cases (see reference test). +- **Integration tests** in `tests/suites/reductions.rs` — compare against JSON ground truth. ## 3. Example Program -Add a round-trip demo to `examples/` showing a practical, explainable instance: -1. Create source problem with a real-world story -2. Reduce to target, solve, extract solution -3. Print human-readable explanation +Add `examples/reduction__to_.rs` — create, reduce, solve, extract, verify, export JSON (see reference example). -## 4. Documentation +## 4. Document -Update `docs/paper/reductions.typ` (see `rules/documentation.md` for the pattern): -- Add `reduction-rule("Source", "Target", ...)` theorem with proof sketch -- Add Rust code example from the example program -- Add `display-name` entry if the problem is new +Update `docs/paper/reductions.typ` — add `reduction-rule("Source", "Target", ...)` with proof sketch (see `rules/documentation.md`). -The goal is to 1. prove the correctness of the reduction to human beings. 2. provide a minimal working example to the readers. +## 5. Regenerate Graph -Citations must be verifiable. Use `[Folklore]` or `—` for trivial reductions. - -## 5. Regenerate Reduction Graph ```bash -make export-graph +cargo run --example export_graph ``` - -## Anti-patterns -- Don't write Rust code before understanding the math and having test data -- Don't create reductions without closed-loop tests -- Don't forget `inventory::submit!` registration (reduction graph won't update) -- Don't hardcode weights - use generic `W` parameter -- Don't skip overhead polynomial specification -- Don't skip the example program — every reduction needs an explainable demo diff --git a/.claude/rules/documentation.md b/.claude/rules/documentation.md index d29234c4..07dfd75b 100644 --- a/.claude/rules/documentation.md +++ b/.claude/rules/documentation.md @@ -5,50 +5,32 @@ paths: # Documentation Requirements -The technical paper (`docs/paper/reductions.typ`) must include: - -1. **Problem Definitions** — using `problem-def` wrapper -2. **Reduction Theorems** — using `reduction-rule` function -3. **Reduction Examples** — minimal working example showing reduce → solve → extract +**Reference:** search `docs/paper/reductions.typ` for `MinimumVertexCover` `MaximumIndependentSet` to see a complete problem-def + reduction-rule example. ## Adding a Problem Definition ```typst -#problem-def("MaximumIndependentSet", "Maximum Independent Set (MIS)")[ +#problem-def("ProblemName")[ Mathematical definition... ] ``` -This auto-generates: -- A label `` for cross-references -- The problem's schema (fields from Rust struct) -- The list of available reductions - -Also add an entry to the `display-name` dictionary: +Also add to the `display-name` dictionary: ```typst -"MaximumIndependentSet": "MIS", +"ProblemName": [Problem Name], ``` ## Adding a Reduction Theorem ```typst -#reduction-rule( - "MaximumIndependentSet", "QUBO", - example: "maximumindependentset_to_qubo", - overhead: (n: 0, m: 1), +#reduction-rule("Source", "Target", + example: true, + example-caption: [caption text], )[ + Rule statement... +][ 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` +Every directed reduction in the graph needs its own `reduction-rule` entry. The paper auto-checks completeness against `reduction_graph.json`. diff --git a/.claude/rules/testing.md b/.claude/rules/testing.md index 64bacc30..b8f57a52 100644 --- a/.claude/rules/testing.md +++ b/.claude/rules/testing.md @@ -1,54 +1,18 @@ # Testing Requirements -## Coverage Requirement -New code must have >95% test coverage. +**Reference test:** `src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs` -```bash -# Check coverage for specific module -cargo tarpaulin --features ilp --skip-clean --ignore-tests -- +## Coverage -# Generate full HTML report -make coverage -``` +New code must have >95% test coverage. Run `make coverage` to check. + +## Naming -## Test Naming Conventions - Reduction tests: `test__to__closed_loop` - Model tests: `test__basic`, `test__serialization` - Solver tests: `test__` -## Closed-Loop Test Pattern -Every reduction MUST have a closed-loop test: - -```rust -#[test] -fn test_source_to_target_closed_loop() { - // 1. Create small instance - let problem = SourceProblem::new(...); - - // 2. Reduce - let reduction = problem.reduce_to::(); - let target = reduction.target_problem(); - - // 3. Solve target - let solver = BruteForce::new(); - let solutions = solver.find_best(target); - - // 4. Extract and verify - for sol in solutions { - let extracted = reduction.extract_solution(&sol); - assert!(problem.is_valid_solution(&extracted)); - } -} -``` - -## Before Submitting PR -```bash -make test # All tests pass -make clippy # No warnings -make coverage # >95% for new code -``` - -## Test File Organization +## File Organization Unit tests live in `src/unit_tests/`, mirroring `src/` structure. Source files reference them via `#[path]`: @@ -59,12 +23,10 @@ Unit tests live in `src/unit_tests/`, mirroring `src/` structure. Source files r mod tests; ``` -The `#[path]` is relative to the source file's directory. `use super::*` in the test file resolves to the parent module (same as inline tests). +Integration tests are in `tests/suites/`, consolidated through `tests/main.rs`. -Integration tests are consolidated into a single binary at `tests/main.rs`, with test modules in `tests/suites/`. +## Before PR -## Anti-patterns -- Don't skip closed-loop tests for reductions -- Don't test only happy paths - include edge cases -- Don't ignore clippy warnings -- Don't add inline `mod tests` blocks in `src/` — use `src/unit_tests/` with `#[path]` +```bash +make test clippy +``` diff --git a/docs/paper/reduction_graph.json b/docs/paper/reduction_graph.json index d05d9f2b..cd0cfb57 100644 --- a/docs/paper/reduction_graph.json +++ b/docs/paper/reduction_graph.json @@ -315,7 +315,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_spins", @@ -343,7 +342,6 @@ "weight": "i32" } }, - "bidirectional": false, "overhead": [ { "field": "num_gates", @@ -367,7 +365,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -395,7 +392,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -420,7 +416,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -448,7 +443,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -457,6 +451,33 @@ ], "doc_path": "rules/coloring_qubo/index.html" }, + { + "source": { + "name": "KSatisfiability", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "target": { + "name": "Satisfiability", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "overhead": [ + { + "field": "num_clauses", + "formula": "num_clauses" + }, + { + "field": "num_vars", + "formula": "num_vars" + } + ], + "doc_path": "rules/sat_ksat/index.html" + }, { "source": { "name": "KSatisfiability", @@ -472,7 +493,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -481,6 +501,87 @@ ], "doc_path": "rules/ksatisfiability_qubo/index.html" }, + { + "source": { + "name": "MaxCut", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "target": { + "name": "SpinGlass", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "overhead": [ + { + "field": "num_spins", + "formula": "num_vertices" + }, + { + "field": "num_interactions", + "formula": "num_edges" + } + ], + "doc_path": "rules/spinglass_maxcut/index.html" + }, + { + "source": { + "name": "MaximumIndependentSet", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "target": { + "name": "MaximumSetPacking", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "overhead": [ + { + "field": "num_sets", + "formula": "num_vertices" + }, + { + "field": "num_elements", + "formula": "num_vertices" + } + ], + "doc_path": "rules/maximumindependentset_maximumsetpacking/index.html" + }, + { + "source": { + "name": "MaximumIndependentSet", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "target": { + "name": "MinimumVertexCover", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "overhead": [ + { + "field": "num_vertices", + "formula": "num_vertices" + }, + { + "field": "num_edges", + "formula": "num_edges" + } + ], + "doc_path": "rules/minimumvertexcover_maximumindependentset/index.html" + }, { "source": { "name": "MaximumIndependentSet", @@ -496,7 +597,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -520,7 +620,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_sets", @@ -548,7 +647,6 @@ "weight": "Unweighted" } }, - "bidirectional": true, "overhead": [ { "field": "num_vertices", @@ -576,7 +674,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -600,7 +697,6 @@ "weight": "Unweighted" } }, - "bidirectional": true, "overhead": [ { "field": "num_vertices", @@ -628,7 +724,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_sets", @@ -656,7 +751,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -665,6 +759,29 @@ ], "doc_path": "rules/minimumvertexcover_qubo/index.html" }, + { + "source": { + "name": "QUBO", + "variant": { + "graph": "SimpleGraph", + "weight": "f64" + } + }, + "target": { + "name": "SpinGlass", + "variant": { + "graph": "SimpleGraph", + "weight": "f64" + } + }, + "overhead": [ + { + "field": "num_spins", + "formula": "num_vars" + } + ], + "doc_path": "rules/spinglass_qubo/index.html" + }, { "source": { "name": "Satisfiability", @@ -680,7 +797,6 @@ "weight": "i32" } }, - "bidirectional": false, "overhead": [ { "field": "num_vertices", @@ -708,7 +824,6 @@ "weight": "Unweighted" } }, - "bidirectional": true, "overhead": [ { "field": "num_clauses", @@ -736,7 +851,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_vertices", @@ -764,7 +878,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_vertices", @@ -792,7 +905,6 @@ "weight": "Unweighted" } }, - "bidirectional": true, "overhead": [ { "field": "num_vertices", @@ -820,7 +932,6 @@ "weight": "f64" } }, - "bidirectional": true, "overhead": [ { "field": "num_vars", diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index d83a5fa0..a0d43cf3 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -70,9 +70,12 @@ .dedup(key: e => e.name) } -// Render a single reduction with link +// Render a single reduction with link (uses context to skip broken links gracefully) #let render-reduction-link(r) = { - link(r.lbl)[#r.name] + context { + if query(r.lbl).len() > 0 { link(r.lbl)[#r.name] } + else { r.name } + } } // Render the "Reduces to/from" lines for a problem @@ -407,6 +410,18 @@ Each reduction is presented as a *Rule* (with linked problem names and overhead ($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. ] +#reduction-rule("MaximumIndependentSet", "MinimumVertexCover")[ + The complement $C = V backslash S$ of an independent set is a vertex cover. Same graph and weights; reverse of VC $arrow.r$ IS. +][ + Identical to the reverse direction: $S$ is independent iff $V backslash S$ is a cover, with $|"IS"| + |"VC"| = |V|$. _Solution extraction:_ for VC solution $C$, return $S = V backslash C$. +] + +#reduction-rule("MaximumIndependentSet", "MaximumSetPacking")[ + Each vertex becomes a singleton set of its incident edges; non-adjacent vertices have disjoint edge sets. Reverse of Set Packing $arrow.r$ IS. +][ + _Variable mapping:_ Universe $U = E$ (edges), $S_v = {e in E : v in e}$, $w(S_v) = w(v)$. Independent vertices have no shared edges, so their edge sets are disjoint $arrow.r.double$ packing. _Solution extraction:_ for packing ${S_v : v in P}$, return IS $= P$. +] + #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'$. ][ @@ -425,6 +440,12 @@ Each reduction is presented as a *Rule* (with linked problem names and overhead 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). ] +#reduction-rule("QUBO", "SpinGlass")[ + The inverse substitution $x_i = (s_i + 1)/2$ converts QUBO to Ising. Reverse of SpinGlass $arrow.r$ QUBO. +][ + Expanding $sum_(i,j) Q_(i j) (s_i+1)(s_j+1)/4$ gives $J_(i j) = -Q_(i j)/4$, $h_i = -(Q_(i i) + sum_j Q_(i j))/2$. _Solution extraction:_ $x_i = (s_i + 1)/2$. +] + #reduction-rule("SpinGlass", "QUBO", example: true, example-caption: [2-spin system with coupling $J_(01) = -1$, fields $h = (0.5, -0.5)$], @@ -581,6 +602,12 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ Set $x_i = 1$ if $"pos"_i$ selected; $x_i = 0$ if $"neg"_i$ selected. ] +#reduction-rule("KSatisfiability", "Satisfiability")[ + Every $k$-SAT instance is already a SAT instance (clauses happen to have exactly $k$ literals). The embedding is trivial. +][ + _Variable mapping:_ Identity — variables and clauses unchanged. _Solution extraction:_ identity. +] + #reduction-rule("Satisfiability", "KSatisfiability")[ @cook1971 @garey1979 Any SAT formula converts to $k$-SAT ($k >= 3$) preserving satisfiability. ][ @@ -628,6 +655,12 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ $p = sum_i p_i 2^(i-1)$, $q = sum_j q_j 2^(j-1)$. ] +#reduction-rule("MaxCut", "SpinGlass")[ + @barahona1982 Set $J_(i j) = w_(i j)$, $h_i = 0$. Maximizing cut equals minimizing $-sum J_(i j) s_i s_j$. +][ + Opposite-partition vertices satisfy $s_i s_j = -1$, contributing $-J_(i j)(-1) = J_(i j)$ to the energy. _Variable mapping:_ $J_(i j) = w_(i j)$, $h_i = 0$, spins $s_i = 2 sigma_i - 1$ where $sigma_i in {0, 1}$ is the partition label. _Solution extraction:_ partition $= {i : s_i = +1}$. +] + #reduction-rule("SpinGlass", "MaxCut")[ @barahona1982 @lucas2014 Ground states of Ising models correspond to maximum cuts. ][ @@ -894,10 +927,7 @@ See #link("https://github.com/CodingThrust/problem-reductions/blob/main/examples 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 + covered.find(c => c.at(0) == e.at(0) and c.at(1) == e.at(1)) == none }) if missing.len() > 0 { block(width: 100%, inset: (x: 1em, y: 0.5em), fill: rgb("#fff3cd"), stroke: (left: 3pt + rgb("#ffc107")))[ diff --git a/docs/src/introduction.md b/docs/src/introduction.md index 427d166b..e3b702c9 100644 --- a/docs/src/introduction.md +++ b/docs/src/introduction.md @@ -81,7 +81,7 @@ For theoretical background and correctness proofs, see the [PDF manual](https:// problems[n.name].children.push(n); }); - // Build edges at variant level + // Build edges at variant level, detecting bidirectional pairs var edgeMap = {}; data.edges.forEach(function(e) { var srcId = variantId(e.source.name, e.source.variant); @@ -90,7 +90,7 @@ For theoretical background and correctness proofs, see the [PDF manual](https:// var rev = dstId + '->' + srcId; if (edgeMap[rev]) { edgeMap[rev].bidirectional = true; } else if (!edgeMap[fwd]) { - edgeMap[fwd] = { source: srcId, target: dstId, bidirectional: e.bidirectional || false, overhead: e.overhead || [], doc_path: e.doc_path || '' }; + edgeMap[fwd] = { source: srcId, target: dstId, bidirectional: false, overhead: e.overhead || [], doc_path: e.doc_path || '' }; } }); diff --git a/docs/src/reductions/reduction_graph.json b/docs/src/reductions/reduction_graph.json index d05d9f2b..cd0cfb57 100644 --- a/docs/src/reductions/reduction_graph.json +++ b/docs/src/reductions/reduction_graph.json @@ -315,7 +315,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_spins", @@ -343,7 +342,6 @@ "weight": "i32" } }, - "bidirectional": false, "overhead": [ { "field": "num_gates", @@ -367,7 +365,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -395,7 +392,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -420,7 +416,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -448,7 +443,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -457,6 +451,33 @@ ], "doc_path": "rules/coloring_qubo/index.html" }, + { + "source": { + "name": "KSatisfiability", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "target": { + "name": "Satisfiability", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "overhead": [ + { + "field": "num_clauses", + "formula": "num_clauses" + }, + { + "field": "num_vars", + "formula": "num_vars" + } + ], + "doc_path": "rules/sat_ksat/index.html" + }, { "source": { "name": "KSatisfiability", @@ -472,7 +493,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -481,6 +501,87 @@ ], "doc_path": "rules/ksatisfiability_qubo/index.html" }, + { + "source": { + "name": "MaxCut", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "target": { + "name": "SpinGlass", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "overhead": [ + { + "field": "num_spins", + "formula": "num_vertices" + }, + { + "field": "num_interactions", + "formula": "num_edges" + } + ], + "doc_path": "rules/spinglass_maxcut/index.html" + }, + { + "source": { + "name": "MaximumIndependentSet", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "target": { + "name": "MaximumSetPacking", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "overhead": [ + { + "field": "num_sets", + "formula": "num_vertices" + }, + { + "field": "num_elements", + "formula": "num_vertices" + } + ], + "doc_path": "rules/maximumindependentset_maximumsetpacking/index.html" + }, + { + "source": { + "name": "MaximumIndependentSet", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "target": { + "name": "MinimumVertexCover", + "variant": { + "graph": "SimpleGraph", + "weight": "Unweighted" + } + }, + "overhead": [ + { + "field": "num_vertices", + "formula": "num_vertices" + }, + { + "field": "num_edges", + "formula": "num_edges" + } + ], + "doc_path": "rules/minimumvertexcover_maximumindependentset/index.html" + }, { "source": { "name": "MaximumIndependentSet", @@ -496,7 +597,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -520,7 +620,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_sets", @@ -548,7 +647,6 @@ "weight": "Unweighted" } }, - "bidirectional": true, "overhead": [ { "field": "num_vertices", @@ -576,7 +674,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -600,7 +697,6 @@ "weight": "Unweighted" } }, - "bidirectional": true, "overhead": [ { "field": "num_vertices", @@ -628,7 +724,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_sets", @@ -656,7 +751,6 @@ "weight": "f64" } }, - "bidirectional": false, "overhead": [ { "field": "num_vars", @@ -665,6 +759,29 @@ ], "doc_path": "rules/minimumvertexcover_qubo/index.html" }, + { + "source": { + "name": "QUBO", + "variant": { + "graph": "SimpleGraph", + "weight": "f64" + } + }, + "target": { + "name": "SpinGlass", + "variant": { + "graph": "SimpleGraph", + "weight": "f64" + } + }, + "overhead": [ + { + "field": "num_spins", + "formula": "num_vars" + } + ], + "doc_path": "rules/spinglass_qubo/index.html" + }, { "source": { "name": "Satisfiability", @@ -680,7 +797,6 @@ "weight": "i32" } }, - "bidirectional": false, "overhead": [ { "field": "num_vertices", @@ -708,7 +824,6 @@ "weight": "Unweighted" } }, - "bidirectional": true, "overhead": [ { "field": "num_clauses", @@ -736,7 +851,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_vertices", @@ -764,7 +878,6 @@ "weight": "Unweighted" } }, - "bidirectional": false, "overhead": [ { "field": "num_vertices", @@ -792,7 +905,6 @@ "weight": "Unweighted" } }, - "bidirectional": true, "overhead": [ { "field": "num_vertices", @@ -820,7 +932,6 @@ "weight": "f64" } }, - "bidirectional": true, "overhead": [ { "field": "num_vars", diff --git a/src/rules/graph.rs b/src/rules/graph.rs index a887bf21..447696e9 100644 --- a/src/rules/graph.rs +++ b/src/rules/graph.rs @@ -68,8 +68,6 @@ pub struct EdgeJson { pub source: VariantRef, /// Target problem variant. pub target: VariantRef, - /// Whether the reverse reduction also exists. - pub bidirectional: bool, /// Reduction overhead: output size as polynomials of input size. pub overhead: Vec, /// Relative rustdoc path for the reduction module. @@ -623,31 +621,27 @@ impl ReductionGraph { .collect(); nodes.sort_by(|a, b| (&a.name, &a.variant).cmp(&(&b.name, &b.variant))); - // Collect edges, checking for bidirectionality - let mut edge_set: HashMap<(VariantRef, VariantRef), (bool, ReductionOverhead, String)> = - HashMap::new(); + // Collect edges: each reduction is a separate directed edge + let mut edge_set: HashSet<(VariantRef, VariantRef)> = HashSet::new(); + let mut edge_data: Vec<(VariantRef, VariantRef, ReductionOverhead, String)> = Vec::new(); for entry in inventory::iter:: { let src_ref = Self::make_variant_ref(entry.source_name, entry.source_variant); let dst_ref = Self::make_variant_ref(entry.target_name, entry.target_variant); - let overhead = entry.overhead(); - let doc_path = Self::module_path_to_doc_path(entry.module_path); - - let reverse_key = (dst_ref.clone(), src_ref.clone()); - if let Some(existing) = edge_set.get_mut(&reverse_key) { - existing.0 = true; - } else { - edge_set.insert((src_ref, dst_ref), (false, overhead, doc_path)); + let key = (src_ref.clone(), dst_ref.clone()); + if edge_set.insert(key) { + let overhead = entry.overhead(); + let doc_path = Self::module_path_to_doc_path(entry.module_path); + edge_data.push((src_ref, dst_ref, overhead, doc_path)); } } // Build edges - let mut edges: Vec = edge_set + let mut edges: Vec = edge_data .into_iter() - .map(|((src, dst), (bidirectional, overhead, doc_path))| EdgeJson { + .map(|(src, dst, overhead, doc_path)| EdgeJson { source: src, target: dst, - bidirectional, overhead: overhead .output_size .iter() diff --git a/src/unit_tests/rules/graph.rs b/src/unit_tests/rules/graph.rs index 60eb5d0d..709ce982 100644 --- a/src/unit_tests/rules/graph.rs +++ b/src/unit_tests/rules/graph.rs @@ -135,14 +135,15 @@ fn test_to_json() { // Check edges assert!(json.edges.len() >= 10); - // Check that IS <-> VC is marked bidirectional - let is_vc_edge = json.edges.iter().find(|e| { - (e.source.name.contains("MaximumIndependentSet") && e.target.name.contains("MinimumVertexCover")) - || (e.source.name.contains("MinimumVertexCover") - && e.target.name.contains("MaximumIndependentSet")) + // Check that IS -> VC and VC -> IS both exist as separate directed edges + let is_to_vc = json.edges.iter().any(|e| { + e.source.name == "MaximumIndependentSet" && e.target.name == "MinimumVertexCover" }); - assert!(is_vc_edge.is_some()); - assert!(is_vc_edge.unwrap().bidirectional); + let vc_to_is = json.edges.iter().any(|e| { + e.source.name == "MinimumVertexCover" && e.target.name == "MaximumIndependentSet" + }); + assert!(is_to_vc, "Should have IS -> VC edge"); + assert!(vc_to_is, "Should have VC -> IS edge"); } #[test] @@ -155,7 +156,10 @@ fn test_to_json_string() { assert!(json_string.contains("\"edges\"")); assert!(json_string.contains("MaximumIndependentSet")); assert!(json_string.contains("\"category\"")); - assert!(json_string.contains("\"bidirectional\"")); + assert!(json_string.contains("\"overhead\"")); + + // The legacy "bidirectional" field must not be present + assert!(!json_string.contains("\"bidirectional\""), "JSON should not contain the removed 'bidirectional' field"); } #[test] @@ -402,36 +406,35 @@ fn test_categorize_circuit_as_specialized() { } #[test] -fn test_edge_bidirectionality_detection() { +fn test_directed_edge_pairs() { let graph = ReductionGraph::new(); let json = graph.to_json(); - // Count bidirectional and unidirectional edges - let bidirectional_count = json.edges.iter().filter(|e| e.bidirectional).count(); - let unidirectional_count = json.edges.iter().filter(|e| !e.bidirectional).count(); - - // We should have both types - assert!(bidirectional_count > 0, "Should have bidirectional edges"); - assert!(unidirectional_count > 0, "Should have unidirectional edges"); - - // Verify specific known bidirectional edges - let is_vc_bidir = json.edges.iter().any(|e| { - (e.source.name.contains("MaximumIndependentSet") && e.target.name.contains("MinimumVertexCover") - || e.source.name.contains("MinimumVertexCover") - && e.target.name.contains("MaximumIndependentSet")) - && e.bidirectional - }); - assert!(is_vc_bidir, "IS <-> VC should be bidirectional"); + // IS <-> VC: both directions should exist as separate edges + let is_to_vc = json + .edges + .iter() + .any(|e| e.source.name == "MaximumIndependentSet" && e.target.name == "MinimumVertexCover"); + let vc_to_is = json + .edges + .iter() + .any(|e| e.source.name == "MinimumVertexCover" && e.target.name == "MaximumIndependentSet"); + assert!(is_to_vc, "Should have IS -> VC edge"); + assert!(vc_to_is, "Should have VC -> IS edge"); - // Verify specific known unidirectional edge - let factoring_circuit_unidir = json.edges.iter().any(|e| { - e.source.name.contains("Factoring") - && e.target.name.contains("CircuitSAT") - && !e.bidirectional - }); + // Factoring -> CircuitSAT: only forward direction + let factoring_to_circuit = json + .edges + .iter() + .any(|e| e.source.name == "Factoring" && e.target.name == "CircuitSAT"); + let circuit_to_factoring = json + .edges + .iter() + .any(|e| e.source.name == "CircuitSAT" && e.target.name == "Factoring"); + assert!(factoring_to_circuit, "Should have Factoring -> CircuitSAT"); assert!( - factoring_circuit_unidir, - "Factoring -> CircuitSAT should be unidirectional" + !circuit_to_factoring, + "Should NOT have CircuitSAT -> Factoring" ); }