diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 74415bfc..5fbed78a 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -35,6 +35,9 @@ make release V=x.y.z # Tag and push a new release (CI publishes to crates.io) make test clippy # Must pass before PR ``` +## Git Safety +- **NEVER force push** (`git push --force`, `git push -f`, `git push --force-with-lease`). This is an absolute rule with no exceptions. Force push can silently destroy other people's work and stashed changes. + ## Architecture ### Core Modules diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index c69117e3..39fe20b7 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -635,7 +635,18 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ For $v_(j,i) in S$ with literal $x_k$: set $x_k = 1$; for $overline(x_k)$: set $x_k = 0$. ] -#reduction-rule("Satisfiability", "KColoring")[ +#let sat_kc = load-example("satisfiability_to_kcoloring") +#let sat_kc_r = load-results("satisfiability_to_kcoloring") +#let sat_kc_sol = sat_kc_r.solutions.at(0) +#reduction-rule("Satisfiability", "KColoring", + example: true, + example-caption: [5-variable SAT with 3 unit clauses to 3-coloring], + extra: [ + SAT assignment: $(x_1, ..., x_5) = (#sat_kc_sol.source_config.map(str).join(", "))$ \ + Construction: 3 base + $2 times #sat_kc.source.instance.num_vars$ variable gadgets + OR-gadgets $arrow.r$ #sat_kc.target.instance.num_vertices vertices, #sat_kc.target.instance.num_edges edges \ + #sat_kc_r.solutions.len() valid 3-colorings (color symmetry of satisfying assignments) #sym.checkmark + ], +)[ @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. @@ -645,7 +656,18 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ Set $x_i = 1$ iff $"color"("pos"_i) = "color"("TRUE")$. ] -#reduction-rule("Satisfiability", "MinimumDominatingSet")[ +#let sat_ds = load-example("satisfiability_to_minimumdominatingset") +#let sat_ds_r = load-results("satisfiability_to_minimumdominatingset") +#let sat_ds_sol = sat_ds_r.solutions.at(0) +#reduction-rule("Satisfiability", "MinimumDominatingSet", + example: true, + example-caption: [5-variable 7-clause 3-SAT to dominating set], + extra: [ + SAT assignment: $(x_1, ..., x_5) = (#sat_ds_sol.source_config.map(str).join(", "))$ \ + Vertex structure: $#sat_ds.target.instance.num_vertices = 3 times #sat_ds.source.instance.num_vars + #sat_ds.source.instance.num_clauses$ (variable triangles + clause vertices) \ + Dominating set of size $n = #sat_ds.source.instance.num_vars$: one vertex per variable triangle #sym.checkmark + ], +)[ @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$. @@ -661,7 +683,18 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Variable mapping:_ Identity — variables and clauses unchanged. _Solution extraction:_ identity. ] -#reduction-rule("Satisfiability", "KSatisfiability")[ +#let sat_ksat = load-example("satisfiability_to_ksatisfiability") +#let sat_ksat_r = load-results("satisfiability_to_ksatisfiability") +#let sat_ksat_sol = sat_ksat_r.solutions.at(0) +#reduction-rule("Satisfiability", "KSatisfiability", + example: true, + example-caption: [Mixed-size clauses (sizes 1 to 5) to 3-SAT], + extra: [ + Source: #sat_ksat.source.instance.num_vars variables, #sat_ksat.source.instance.num_clauses clauses (sizes 1, 2, 3, 3, 4, 5) \ + Target 3-SAT: $#sat_ksat.target.instance.num_vars = #sat_ksat.source.instance.num_vars + 7$ variables, #sat_ksat.target.instance.num_clauses clauses (small padded, large split) \ + First solution: $(x_1, ..., x_5) = (#sat_ksat_sol.source_config.map(str).join(", "))$, auxiliary vars are don't-cares #sym.checkmark + ], +)[ @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$. @@ -672,7 +705,17 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Correctness._ Original clause true $arrow.l.r$ auxiliary chain can propagate truth through new clauses. ] -#reduction-rule("CircuitSAT", "SpinGlass")[ +#let cs_sg = load-example("circuitsat_to_spinglass") +#let cs_sg_r = load-results("circuitsat_to_spinglass") +#reduction-rule("CircuitSAT", "SpinGlass", + example: true, + example-caption: [1-bit full adder to Ising model], + extra: [ + Circuit: #cs_sg.source.instance.num_gates gates (2 XOR, 2 AND, 1 OR), #cs_sg.source.instance.num_variables variables \ + Target: #cs_sg.target.instance.num_spins spins (each gate allocates I/O + auxiliary spins) \ + #cs_sg_r.solutions.len() ground states ($= 2^3$ valid input combinations for the full adder) #sym.checkmark + ], +)[ @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}$. @@ -694,7 +737,26 @@ where $P$ is a penalty weight large enough that any constraint violation costs m caption: [Ising gadgets for logic gates. Ground states match truth tables.] ) -#reduction-rule("Factoring", "CircuitSAT")[ +#let fact_cs = load-example("factoring_to_circuitsat") +#let fact_cs_r = load-results("factoring_to_circuitsat") +#let fact-decode(config, start, count) = { + let pow2 = (1, 2, 4, 8, 16, 32) + range(count).fold(0, (acc, i) => acc + config.at(start + i) * pow2.at(i)) +} +#let fact-nbf = fact_cs.source.instance.num_bits_first +#let fact-nbs = fact_cs.source.instance.num_bits_second +#reduction-rule("Factoring", "CircuitSAT", + example: true, + example-caption: [Factor $N = #fact_cs.source.instance.number$], + extra: [ + Circuit: $#fact-nbf times #fact-nbs$ array multiplier with #fact_cs.target.instance.num_gates gates, #fact_cs.target.instance.num_variables variables \ + #fact_cs_r.solutions.len() solutions: #fact_cs_r.solutions.map(sol => { + let p = fact-decode(sol.source_config, 0, fact-nbf) + let q = fact-decode(sol.source_config, fact-nbf, fact-nbs) + $#p times #q = #fact_cs.source.instance.number$ + }).join(" and ") #sym.checkmark + ], +)[ 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$: @@ -708,13 +770,36 @@ 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")[ +#let mc_sg = load-example("maxcut_to_spinglass") +#let mc_sg_r = load-results("maxcut_to_spinglass") +#let mc_sg_sol = mc_sg_r.solutions.at(0) +#let mc_sg_cut = mc_sg.source.instance.edges.filter(e => mc_sg_sol.source_config.at(e.at(0)) != mc_sg_sol.source_config.at(e.at(1))).len() +#reduction-rule("MaxCut", "SpinGlass", + example: true, + example-caption: [Petersen graph ($n = 10$, unit weights) to Ising], + extra: [ + Direct 1:1 mapping: vertices $arrow.r$ spins, $J_(i j) = w_(i j) = 1$, $h_i = 0$ \ + Partition: $S = {#mc_sg_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ vs $overline(S) = {#mc_sg_sol.source_config.enumerate().filter(((i, x)) => x == 0).map(((i, x)) => str(i)).join(", ")}$ \ + Cut value $= #mc_sg_cut$ ($#mc_sg_r.solutions.len()$-fold degenerate) #sym.checkmark + ], +)[ @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")[ +#let sg_mc = load-example("spinglass_to_maxcut") +#let sg_mc_r = load-results("spinglass_to_maxcut") +#let sg_mc_sol = sg_mc_r.solutions.at(0) +#reduction-rule("SpinGlass", "MaxCut", + example: true, + example-caption: [10-spin Ising with alternating $J_(i j) in {plus.minus 1}$], + extra: [ + All $h_i = 0$: no ancilla needed, direct 1:1 vertex mapping \ + Edge weights $w_(i j) = J_(i j) in {plus.minus 1}$ (alternating couplings) \ + Ground state ($#sg_mc_r.solutions.len()$-fold degenerate): partition $S = {#sg_mc_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => str(i)).join(", ")}$ #sym.checkmark + ], +)[ @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$. diff --git a/docs/src/getting-started.md b/docs/src/getting-started.md index 2307c3df..42f4f0e7 100644 --- a/docs/src/getting-started.md +++ b/docs/src/getting-started.md @@ -28,66 +28,164 @@ The core workflow is: **create** a problem, **reduce** it to a target, **solve** -### Complete Example +### Example 1: Direct reduction -```rust +Reduce Maximum Independent Set to Minimum Vertex Cover on a 4-vertex path +graph, solve the target, and extract the solution back. + +#### Step 1 — Create the source problem + +A path graph `0–1–2–3` has 4 vertices and 3 edges. + +```rust,ignore use problemreductions::prelude::*; use problemreductions::topology::SimpleGraph; -// 1. Create: Independent Set on a path graph (4 vertices) -let problem = MaximumIndependentSet::new(SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]), vec![1i32; 4]); +let problem = MaximumIndependentSet::new( + SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3)]), + vec![1i32; 4], +); +``` + +#### Step 2 — Reduce to Minimum Vertex Cover + +`ReduceTo` applies a single-step reduction. The result holds the target +problem and knows how to map solutions back. -// 2. Reduce: Transform to Minimum Vertex Cover +```rust,ignore +println!("Source: {} {:?}", MaximumIndependentSet::::NAME, + MaximumIndependentSet::::variant()); let reduction = ReduceTo::>::reduce_to(&problem); let target = reduction.target_problem(); +println!("Target: {} {:?}, {} variables", + MinimumVertexCover::::NAME, + MinimumVertexCover::::variant(), + target.num_variables()); +``` + +```text +Source: MaximumIndependentSet [("graph", "SimpleGraph"), ("weight", "i32")] +Target: MinimumVertexCover [("graph", "SimpleGraph"), ("weight", "i32")], 4 variables +``` + +#### Step 3 — Solve the target problem + +`BruteForce` enumerates all configurations and returns the optimal one. -// 3. Solve: Find optimal solution to the target problem +```rust,ignore let solver = BruteForce::new(); let target_solution = solver.find_best(target).unwrap(); +println!("VC solution: {:?}", target_solution); +``` -// 4. Extract: Map solution back to original problem -let solution = reduction.extract_solution(&target_solution); +```text +VC solution: [1, 0, 1, 0] +``` + +#### Step 4 — Extract and verify + +`extract_solution` maps the Vertex Cover solution back to an Independent Set +solution by complementing the configuration. -// Verify: solution is valid for the original problem +```rust,ignore +let solution = reduction.extract_solution(&target_solution); let metric = problem.evaluate(&solution); +println!("IS solution: {:?} -> size {:?}", solution, metric); assert!(metric.is_valid()); ``` -### Chaining Reductions +```text +IS solution: [0, 1, 0, 1] -> size Valid(2) +``` + +S ⊆ V is an independent set iff V \ S is a vertex cover, so the complement +maps optimality in one direction to optimality in the other. + +### Example 2: Reduction path search — integer factoring to spin glass + +Real-world problems often require **chaining** multiple reductions. Here we factor the integer 6 by reducing `Factoring` through the reduction graph to `SpinGlass`, through automatic reduction path search. + +```rust,ignore +{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:imports}} + +{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:example}} +``` + +Let's walk through each step. -Reductions compose into multi-step chains. The `ReductionGraph` discovers -paths through the variant-level graph. Find a `ReductionPath` first, then -convert it to a typed `ExecutablePath` via `make_executable()`. Call -`reduce()` once and get a `ChainedReduction` with `target_problem()` and -`extract_solution()`, just like a single-step reduction. +#### Step 1 — Discover the reduction path -Here we solve a 3-SAT formula by chaining through Satisfiability -and MaximumIndependentSet: +`ReductionGraph` holds every registered reduction. `find_cheapest_path` +searches for the shortest chain from a source problem variant to a target +variant. ```rust,ignore -{{#include ../../examples/chained_reduction_ksat_to_mis.rs:imports}} +{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:step1}} +``` -{{#include ../../examples/chained_reduction_ksat_to_mis.rs:example}} +```text + Factoring → CircuitSAT → SpinGlass {graph: "SimpleGraph", weight: "i32"} +``` + +#### Step 2 — Create the Factoring problem + +`Factoring::new(m, n, target)` creates a factoring instance: find two factors +`p` (m-bit) and `q` (n-bit) such that `p × q = target`. Here we factor **6** +with two 2-bit factors, expecting **2 × 3** or **3 × 2**. -{{#include ../../examples/chained_reduction_ksat_to_mis.rs:overhead}} +```rust,ignore +{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:step2}} ``` -The `ExecutablePath` handles variant casts (e.g., `K3` → `KN`) and -cross-problem reductions (e.g., SAT → MIS) uniformly. The `ChainedReduction` -extracts solutions back through the entire chain in one call. +#### Step 3 — Solve with ILPSolver -`compose_path_overhead` composes the per-step polynomial overheads into a -symbolic formula mapping source variables to final target variables: +`solve_reduced` reduces the problem to ILP internally and solves it in one +call. It returns a configuration vector for the original problem — no manual +extraction needed. For small instances you can also use `BruteForce`, but +`ILPSolver` scales to much larger problems. + +```rust,ignore +{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:step3}} +``` + +#### Step 4 — Read and verify the factors + +`read_factors` decodes the binary configuration back into the two integer +factors. + +```rust,ignore +{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:step4}} +``` ```text - num_vertices = num_literals - num_edges = num_literals^2 +6 = 3 × 2 ``` -This result comes from composing two steps: KSatisfiability → Satisfiability -is identity (same size fields), then Satisfiability → MIS maps -`num_vertices = num_literals` and `num_edges = num_literals²`. -Substituting the identity through gives the final polynomials above. +#### Step 5 — Inspect the overhead + +Each reduction edge carries a polynomial overhead mapping source problem +sizes to target sizes. `path_overheads` returns the per-edge +polynomials, and `compose_path_overhead` composes them symbolically into a +single end-to-end formula. + +```rust,ignore +{{#include ../../examples/chained_reduction_factoring_to_spinglass.rs:overhead}} +``` + +```text +Factoring → CircuitSAT: + num_variables = num_bits_first * num_bits_second + num_assignments = num_bits_first * num_bits_second +CircuitSAT → SpinGlass {graph: "SimpleGraph", weight: "i32"}: + num_spins = num_assignments + num_interactions = num_assignments +SpinGlass {graph: "SimpleGraph", weight: "i32"} → SpinGlass {graph: "SimpleGraph", weight: "f64"}: + num_spins = num_spins + num_interactions = num_interactions +Composed (source → target): + num_spins = num_bits_first * num_bits_second + num_interactions = num_bits_first * num_bits_second +``` ## Solvers diff --git a/docs/src/reductions/reduction_graph.json b/docs/src/reductions/reduction_graph.json index 01d93b98..7f6e9f68 100644 --- a/docs/src/reductions/reduction_graph.json +++ b/docs/src/reductions/reduction_graph.json @@ -228,7 +228,11 @@ "target": 0, "overhead": [ { - "field": "num_gates", + "field": "num_variables", + "formula": "num_bits_first * num_bits_second" + }, + { + "field": "num_assignments", "formula": "num_bits_first * num_bits_second" } ], @@ -269,8 +273,8 @@ "formula": "num_vertices" }, { - "field": "num_colors", - "formula": "num_colors" + "field": "num_edges", + "formula": "num_edges" } ], "doc_path": "rules/kcoloring_casts/index.html" @@ -281,11 +285,11 @@ "overhead": [ { "field": "num_vars", - "formula": "num_vertices * num_colors" + "formula": "num_vertices^2" }, { "field": "num_constraints", - "formula": "num_vertices + num_edges * num_colors" + "formula": "num_vertices + num_vertices * num_edges" } ], "doc_path": "rules/coloring_ilp/index.html" @@ -296,7 +300,7 @@ "overhead": [ { "field": "num_vars", - "formula": "num_vertices * num_colors" + "formula": "num_vertices^2" } ], "doc_path": "rules/coloring_qubo/index.html" @@ -338,6 +342,10 @@ { "field": "num_vars", "formula": "num_vars" + }, + { + "field": "num_literals", + "formula": "num_literals" } ], "doc_path": "rules/sat_ksat/index.html" @@ -379,6 +387,10 @@ { "field": "num_vars", "formula": "num_vars" + }, + { + "field": "num_literals", + "formula": "num_literals" } ], "doc_path": "rules/sat_ksat/index.html" @@ -394,6 +406,10 @@ { "field": "num_vars", "formula": "num_vars" + }, + { + "field": "num_literals", + "formula": "num_literals" } ], "doc_path": "rules/sat_ksat/index.html" @@ -497,7 +513,7 @@ "formula": "num_vertices" }, { - "field": "num_elements", + "field": "universe_size", "formula": "num_vertices" } ], @@ -598,7 +614,7 @@ "formula": "num_edges" }, { - "field": "num_elements", + "field": "universe_size", "formula": "num_vertices" } ], @@ -654,8 +670,8 @@ "formula": "num_sets" }, { - "field": "num_elements", - "formula": "num_elements" + "field": "universe_size", + "formula": "universe_size" } ], "doc_path": "rules/maximumsetpacking_casts/index.html" @@ -729,7 +745,7 @@ "formula": "num_vertices" }, { - "field": "num_elements", + "field": "universe_size", "formula": "num_edges" } ], @@ -763,7 +779,11 @@ "overhead": [ { "field": "num_variables", - "formula": "num_variables + num_clauses + 1" + "formula": "num_vars + num_clauses + 1" + }, + { + "field": "num_assignments", + "formula": "num_clauses + 2" } ], "doc_path": "rules/sat_circuitsat/index.html" @@ -777,8 +797,8 @@ "formula": "2 * num_vars + 5 * num_literals - 5 * num_clauses + 3" }, { - "field": "num_colors", - "formula": "3" + "field": "num_edges", + "formula": "3 * num_vars + 11 * num_literals - 9 * num_clauses + 3" } ], "doc_path": "rules/sat_coloring/index.html" diff --git a/examples/chained_reduction_factoring_to_spinglass.rs b/examples/chained_reduction_factoring_to_spinglass.rs index a22b7bd7..dadb6a2f 100644 --- a/examples/chained_reduction_factoring_to_spinglass.rs +++ b/examples/chained_reduction_factoring_to_spinglass.rs @@ -14,6 +14,7 @@ use problemreductions::types::ProblemSize; pub fn run() { // ANCHOR: example + // ANCHOR: step1 let graph = ReductionGraph::new(); // Find reduction path: Factoring -> ... -> SpinGlass @@ -29,19 +30,44 @@ pub fn run() { &MinimizeSteps, ) .unwrap(); - println!("Reduction path: {:?}", rpath.type_names()); + println!(" {}", rpath); + // ANCHOR_END: step1 + // ANCHOR: step2 // Create: factor 6 = p × q with 2-bit factors (mirrors Julia's Factoring(2, 2, 6)) let factoring = Factoring::new(2, 2, 6); + // ANCHOR_END: step2 + // ANCHOR: step3 // Solve Factoring via ILP let solver = ILPSolver::new(); let solution = solver.solve_reduced(&factoring).unwrap(); + // ANCHOR_END: step3 + // ANCHOR: step4 // Extract and display the factors let (p, q) = factoring.read_factors(&solution); println!("{} = {} × {}", factoring.target(), p, q); assert_eq!(p * q, 6, "Factors should multiply to 6"); + // ANCHOR_END: step4 + + // ANCHOR: overhead + // Print per-edge overhead polynomials + let edge_overheads = graph.path_overheads(&rpath); + for (i, overhead) in edge_overheads.iter().enumerate() { + println!("{} → {}:", rpath.steps[i], rpath.steps[i + 1]); + for (field, poly) in &overhead.output_size { + println!(" {} = {}", field, poly); + } + } + + // Compose overheads symbolically along the full path + let composed = graph.compose_path_overhead(&rpath); + println!("Composed (source → target):"); + for (field, poly) in &composed.output_size { + println!(" {} = {}", field, poly); + } + // ANCHOR_END: overhead // ANCHOR_END: example } diff --git a/src/rules/graph.rs b/src/rules/graph.rs index 8183ac2c..de998a21 100644 --- a/src/rules/graph.rs +++ b/src/rules/graph.rs @@ -139,6 +139,23 @@ impl ReductionPath { } } +impl std::fmt::Display for ReductionPath { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let mut prev_name = ""; + for step in &self.steps { + if step.name != prev_name { + if prev_name.is_empty() { + write!(f, "{step}")?; + } else { + write!(f, " → {step}")?; + } + prev_name = &step.name; + } + } + Ok(()) + } +} + /// A node in a variant-level reduction path. #[derive(Debug, Clone, Serialize)] pub struct ReductionStep { @@ -148,6 +165,21 @@ pub struct ReductionStep { pub variant: BTreeMap, } +impl std::fmt::Display for ReductionStep { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{}", self.name)?; + if !self.variant.is_empty() { + let vars: Vec<_> = self + .variant + .iter() + .map(|(k, v)| format!("{k}: {v:?}")) + .collect(); + write!(f, " {{{}}}", vars.join(", "))?; + } + Ok(()) + } +} + /// Classify a problem's category from its module path. /// Expected format: "problemreductions::models::::" pub(crate) fn classify_problem_category(module_path: &str) -> &str { @@ -542,15 +574,14 @@ impl ReductionGraph { self.nodes.len() } - /// Compose overheads along a path symbolically. + /// Get the per-edge overhead polynomials along a reduction path. /// - /// Returns a single `ReductionOverhead` whose polynomials map from the - /// source problem's size variables directly to the final target's size variables. + /// Returns one `ReductionOverhead` per edge (i.e., `path.steps.len() - 1` items). /// /// Panics if any step in the path does not correspond to an edge in the graph. - pub fn compose_path_overhead(&self, path: &ReductionPath) -> ReductionOverhead { + pub fn path_overheads(&self, path: &ReductionPath) -> Vec { if path.steps.len() <= 1 { - return ReductionOverhead::default(); + return vec![]; } let node_indices: Vec = path @@ -562,75 +593,36 @@ impl ReductionGraph { }) .collect(); - let mut composed: Option = None; - for pair in node_indices.windows(2) { - let edge_idx = self - .graph - .find_edge(pair[0], pair[1]) - .unwrap_or_else(|| { - let src = &self.nodes[self.graph[pair[0]]]; - let dst = &self.nodes[self.graph[pair[1]]]; - panic!( - "No edge from {} {:?} to {} {:?}", - src.name, src.variant, dst.name, dst.variant - ) - }); - let edge_overhead = &self.graph[edge_idx].overhead; - composed = Some(match composed { - None => edge_overhead.clone(), - Some(prev) => prev.compose(edge_overhead), - }); - } - - composed.unwrap_or_default() + node_indices + .windows(2) + .map(|pair| { + let edge_idx = self + .graph + .find_edge(pair[0], pair[1]) + .unwrap_or_else(|| { + let src = &self.nodes[self.graph[pair[0]]]; + let dst = &self.nodes[self.graph[pair[1]]]; + panic!( + "No edge from {} {:?} to {} {:?}", + src.name, src.variant, dst.name, dst.variant + ) + }); + self.graph[edge_idx].overhead.clone() + }) + .collect() } - /// Evaluate the cumulative overhead along a reduction path. - /// - /// Starting from `input_size`, chains each edge's overhead to compute - /// intermediate and final problem sizes. Returns the sizes at each step - /// (including the initial input size), so the length is `path.steps.len()`. + /// Compose overheads along a path symbolically. /// - /// Panics if any step in the path does not correspond to an edge in the graph. - pub fn evaluate_path_overhead( - &self, - path: &ReductionPath, - input_size: &ProblemSize, - ) -> Vec { - let mut sizes = vec![input_size.clone()]; - if path.steps.len() <= 1 { - return sizes; - } - - let node_indices: Vec = path - .steps - .iter() - .map(|step| { - self.lookup_node(&step.name, &step.variant) - .unwrap_or_else(|| panic!("Node not found: {} {:?}", step.name, step.variant)) - }) - .collect(); - - let mut current_size = input_size.clone(); - for pair in node_indices.windows(2) { - let edge_idx = self - .graph - .find_edge(pair[0], pair[1]) - .unwrap_or_else(|| { - let src = &self.nodes[self.graph[pair[0]]]; - let dst = &self.nodes[self.graph[pair[1]]]; - panic!( - "No edge from {} {:?} to {} {:?}", - src.name, src.variant, dst.name, dst.variant - ) - }); - let overhead = &self.graph[edge_idx].overhead; - current_size = overhead.evaluate_output_size(¤t_size); - sizes.push(current_size.clone()); - } - - sizes + /// Returns a single `ReductionOverhead` whose polynomials map from the + /// source problem's size variables directly to the final target's size variables. + pub fn compose_path_overhead(&self, path: &ReductionPath) -> ReductionOverhead { + self.path_overheads(path) + .into_iter() + .reduce(|acc, oh| acc.compose(&oh)) + .unwrap_or_default() } + } impl Default for ReductionGraph { diff --git a/src/traits.rs b/src/traits.rs index 3f25924a..cba13e44 100644 --- a/src/traits.rs +++ b/src/traits.rs @@ -31,7 +31,7 @@ pub trait Problem: Clone { fn problem_size_values(&self) -> Vec; } -/// Combine type-level names and instance-level values into a [`ProblemSize`]. +/// Combine type-level names and instance-level values into a [`crate::types::ProblemSize`]. pub fn problem_size(p: &P) -> crate::types::ProblemSize { crate::types::ProblemSize::from_names_values(P::problem_size_names(), &p.problem_size_values()) } diff --git a/src/unit_tests/reduction_graph.rs b/src/unit_tests/reduction_graph.rs index 2bc78855..df8ed6c9 100644 --- a/src/unit_tests/reduction_graph.rs +++ b/src/unit_tests/reduction_graph.rs @@ -241,6 +241,41 @@ fn test_bidirectional_paths() { .is_empty()); } +// ---- Display ---- + +#[test] +fn test_reduction_path_display() { + let graph = ReductionGraph::new(); + let src_var = ReductionGraph::variant_to_map(&Factoring::variant()); + let dst_var = ReductionGraph::variant_to_map(&SpinGlass::::variant()); + let path = graph + .find_cheapest_path( + "Factoring", + &src_var, + "SpinGlass", + &dst_var, + &ProblemSize::new(vec![]), + &MinimizeSteps, + ) + .unwrap(); + + let s = format!("{path}"); + // Should contain arrow-separated problem names with variant info + assert!(s.contains("Factoring")); + assert!(s.contains("→")); + assert!(s.contains("SpinGlass")); + + // Step with empty variant + let step = &path.steps[0]; + assert_eq!(format!("{step}"), "Factoring"); + + // Step with non-empty variant + let last = path.steps.last().unwrap(); + let last_s = format!("{last}"); + assert!(last_s.contains("SpinGlass")); + assert!(last_s.contains("{")); +} + // ---- Overhead evaluation along a path ---- #[test] @@ -290,31 +325,22 @@ fn test_3sat_to_mis_triangular_overhead() { ); assert_eq!(path.len(), 3); - // Evaluate overhead at each step - let sizes = graph.evaluate_path_overhead(&path, &input_size); - assert_eq!(sizes.len(), 4); // initial + 3 steps - - // Step 0: K3SAT input (V=3, C=2, L=6) - assert_eq!(sizes[0].get("num_vars"), Some(3)); - assert_eq!(sizes[0].get("num_clauses"), Some(2)); - assert_eq!(sizes[0].get("num_literals"), Some(6)); - - // Step 1: K3SAT → SAT (identity: V=3, C=2, L=6) - assert_eq!(sizes[1].get("num_vars"), Some(3)); - assert_eq!(sizes[1].get("num_clauses"), Some(2)); - assert_eq!(sizes[1].get("num_literals"), Some(6)); - - // Step 2: SAT → MIS{SimpleGraph,i32} - // num_vertices = num_literals = 6 - // num_edges = num_literals² = 36 - assert_eq!(sizes[2].get("num_vertices"), Some(6)); - assert_eq!(sizes[2].get("num_edges"), Some(36)); - - // Step 3: MIS{SimpleGraph,i32} → MIS{TriangularSubgraph,i32} - // num_vertices = num_vertices² = 36 - // num_edges = num_vertices² = 36 - assert_eq!(sizes[3].get("num_vertices"), Some(36)); - assert_eq!(sizes[3].get("num_edges"), Some(36)); + // Per-edge symbolic overheads + let edges = graph.path_overheads(&path); + assert_eq!(edges.len(), 3); + + // Edge 0: K3SAT → SAT (identity) + assert_eq!(edges[0].get("num_vars").unwrap().normalized(), poly!(num_vars)); + assert_eq!(edges[0].get("num_clauses").unwrap().normalized(), poly!(num_clauses)); + assert_eq!(edges[0].get("num_literals").unwrap().normalized(), poly!(num_literals)); + + // Edge 1: SAT → MIS{SimpleGraph,i32} + assert_eq!(edges[1].get("num_vertices").unwrap().normalized(), poly!(num_literals)); + assert_eq!(edges[1].get("num_edges").unwrap().normalized(), poly!(num_literals ^ 2)); + + // Edge 2: MIS{SimpleGraph,i32} → MIS{TriangularSubgraph,i32} + assert_eq!(edges[2].get("num_vertices").unwrap().normalized(), poly!(num_vertices ^ 2)); + assert_eq!(edges[2].get("num_edges").unwrap().normalized(), poly!(num_vertices ^ 2)); // Compose overheads symbolically along the path. // The composed overhead maps 3-SAT input variables to final MIS{Triangular} output.