From 71bfc3e4d1a95c60adc59b1485f2f580ef4f04ab Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sun, 22 Mar 2026 07:51:32 +0800 Subject: [PATCH 1/3] Add plan for #202: [Rule] Partition to Knapsack --- .../plans/2026-03-22-partition-to-knapsack.md | 119 ++++++++++++++++++ 1 file changed, 119 insertions(+) create mode 100644 docs/plans/2026-03-22-partition-to-knapsack.md diff --git a/docs/plans/2026-03-22-partition-to-knapsack.md b/docs/plans/2026-03-22-partition-to-knapsack.md new file mode 100644 index 000000000..dffdad973 --- /dev/null +++ b/docs/plans/2026-03-22-partition-to-knapsack.md @@ -0,0 +1,119 @@ +# Plan: Add Partition -> Knapsack Reduction + +**Issue:** #202 — [Rule] Partition to Knapsack +**Skill:** add-rule + +## Information Checklist + +| # | Item | Value | +|---|------|-------| +| 1 | Source problem | `Partition` | +| 2 | Target problem | `Knapsack` | +| 3 | Reduction algorithm | Map each Partition element `s_i` to one Knapsack item with `weight_i = value_i = s_i`, cast from `u64` to `i64`, and set capacity to `floor(total_sum / 2)` | +| 4 | Solution extraction | Identity on the binary configuration vector: selected knapsack items are exactly the chosen partition subset | +| 5 | Correctness argument | A balanced partition exists iff the constructed knapsack optimum reaches `total_sum / 2`; when `weight = value`, maximizing value under capacity `floor(total_sum / 2)` is equivalent to finding the largest achievable subset sum up to that bound | +| 6 | Size overhead | `num_items = "num_elements"` | +| 7 | Concrete example | Partition sizes `[3, 1, 1, 2, 2, 1]` map to a Knapsack instance with identical weights/values and capacity `5`; witness config `[1, 0, 0, 1, 0, 0]` works on both sides | +| 8 | Solving strategy | Solve the target with `BruteForce::find_all_best()` / `find_best()`; use `assert_satisfaction_round_trip_from_optimization_target` on satisfiable instances | +| 9 | Reference | Garey & Johnson, *Computers and Intractability* (1979), Appendix A6 / MP9 (“Transformation from PARTITION”) | + +## Design Decisions + +### Problem-type bridge + +`Partition` is a satisfaction problem while `Knapsack` is an optimization problem in this codebase. The rule will therefore interpret the target optimum semantically: a source instance is satisfiable exactly when the best knapsack value is `total_sum / 2`. The reduction itself still stores only the target instance plus the identity config mapping. + +### Numeric conversion + +`Partition` stores sizes as `u64`, but `Knapsack` uses `i64`. The reduction should use explicit checked casts (`i64::try_from`) with a rule-specific panic message so overflow is caught deterministically instead of silently truncating. + +### Overhead scope + +Keep the `#[reduction(overhead = ...)]` metadata to the stable target getter that matters here: `num_items = "num_elements"`. `Knapsack::num_slack_bits()` depends on capacity with a zero-capacity special case, so forcing it into the symbolic overhead expression would complicate the rule without improving the reduction graph. + +### Repo-specific example registration + +Although the generic `add-rule` skill mentions `src/example_db/rule_builders.rs`, this repo’s current pattern is to place `canonical_rule_example_specs()` in the rule module itself and aggregate it from `src/rules/mod.rs`. Follow the in-repo pattern, not the older wording. + +## Execution Batches + +### Batch 1: Implement the rule and regenerate exported data + +#### Step 1: Add the rule module (`src/rules/partition_knapsack.rs`) + +1. Create `ReductionPartitionToKnapsack` with a `target: Knapsack` field. +2. Add a small checked-cast helper for `u64 -> i64` with an explicit panic string such as `"Partition -> Knapsack requires all sizes and total_sum / 2 to fit in i64"`. +3. Implement `ReductionResult`: + - `target_problem()` returns the stored `Knapsack`. + - `extract_solution()` returns `target_solution.to_vec()` because both problems use the same binary selection vector. +4. Implement `ReduceTo for Partition` with: + - `weights = sizes.map(cast)` + - `values = weights.clone()` + - `capacity = cast(total_sum / 2)` + - `#[reduction(overhead = { num_items = "num_elements" })]` +5. Add `#[cfg(feature = "example-db")] canonical_rule_example_specs()` in this file using the issue example and a single canonical witness. +6. Link the unit tests with `#[cfg(test)] #[path = "../unit_tests/rules/partition_knapsack.rs"] mod tests;` + +#### Step 2: Register the rule (`src/rules/mod.rs`) + +1. Add `pub(crate) mod partition_knapsack;` +2. Extend `canonical_rule_example_specs()` with `partition_knapsack::canonical_rule_example_specs()` + +#### Step 3: Add unit tests (`src/unit_tests/rules/partition_knapsack.rs`) + +1. Add a satisfiable closed-loop test using `Partition::new(vec![3, 1, 1, 2, 2, 1])` and `assert_satisfaction_round_trip_from_optimization_target(...)`. +2. Add a structure test that checks: + - target weights equal `[3, 1, 1, 2, 2, 1]` + - target values equal `[3, 1, 1, 2, 2, 1]` + - target capacity equals `5` + - `num_items()` matches `num_elements()` +3. Add an unsatisfiable/odd-total test (for example `[2, 4, 5]`) that: + - solves the target with `BruteForce::find_best()` + - extracts the source config + - asserts `source.evaluate(&extracted)` is `false` +4. Add a checked-cast panic test with a value larger than `i64::MAX`. + +#### Step 4: Regenerate the exports needed by the paper + +Run these after the rule and canonical example compile: + +```bash +cargo run --features "example-db" --example export_examples +cargo run --example export_graph +cargo run --example export_schemas +``` + +These commands must succeed before the paper step so `load-example("Partition", "Knapsack")` has backing JSON data. + +### Batch 2: Write the paper entry and run final verification + +#### Step 5: Document the rule in `docs/paper/reductions.typ` + +1. Add a `#let partition_knapsack = load-example("Partition", "Knapsack")` block near the other reduction examples. +2. Add a `#reduction-rule("Partition", "Knapsack", ...)` entry that: + - cites Garey & Johnson for the textbook reduction + - states that the reduction uses one knapsack item per partition element + - explains the satisfaction-to-optimization interpretation explicitly +3. In the proof body, include: + - `_Construction._` with `w_i = v_i = s_i` and `C = floor(sum_i s_i / 2)` + - `_Correctness._` proving `Partition` is satisfiable iff the optimum knapsack value is exactly `sum_i s_i / 2` + - `_Solution extraction._` explaining the identity mapping back to the partition subset +4. In the `extra:` tutorial block, use the canonical example JSON data rather than hardcoded values: + - `pred create --example Partition -o partition.json` + - `pred reduce partition.json --to "Knapsack" -o bundle.json` + - `pred solve bundle.json` + - `pred evaluate partition.json --config ...` +5. Note witness semantics clearly: the fixture stores one canonical balanced subset even if multiple optimal knapsack witnesses exist. + +#### Step 6: Verify the full change + +Run: + +```bash +make fmt-check +make clippy +make test +make paper +``` + +If `make paper` regenerates ignored outputs, leave ignored/generated files unstaged unless the repo already tracks them. The required committed changes are the rule/test/source files plus any tracked export fixture updates produced by the commands above. From 1d6e0971a77fb2c9942d493ba739f65c001b4768 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sun, 22 Mar 2026 07:59:24 +0800 Subject: [PATCH 2/3] Implement #202: [Rule] Partition to Knapsack --- docs/paper/reductions.typ | 42 +++++++++++++ src/rules/mod.rs | 2 + src/rules/partition_knapsack.rs | 73 ++++++++++++++++++++++ src/unit_tests/rules/partition_knapsack.rs | 54 ++++++++++++++++ 4 files changed, 171 insertions(+) create mode 100644 src/rules/partition_knapsack.rs create mode 100644 src/unit_tests/rules/partition_knapsack.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 9167a0c15..1ae122994 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -5929,6 +5929,48 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ Discard slack variables: return $bold(x)' [0..n]$. ] +#let part_ks = load-example("Partition", "Knapsack") +#let part_ks_sol = part_ks.solutions.at(0) +#let part_ks_sizes = part_ks.source.instance.sizes +#let part_ks_n = part_ks_sizes.len() +#let part_ks_total = part_ks_sizes.fold(0, (a, b) => a + b) +#let part_ks_capacity = part_ks.target.instance.capacity +#let part_ks_selected = part_ks_sol.source_config.enumerate().filter(((i, x)) => x == 1).map(((i, x)) => i) +#let part_ks_selected_sizes = part_ks_selected.map(i => part_ks_sizes.at(i)) +#let part_ks_selected_sum = part_ks_selected_sizes.fold(0, (a, b) => a + b) +#reduction-rule("Partition", "Knapsack", + example: true, + example-caption: [#part_ks_n elements, total sum $S = #part_ks_total$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(part_ks.source) + " -o partition.json", + "pred reduce partition.json --to " + target-spec(part_ks) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate partition.json --config " + part_ks_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Source instance.* The canonical Partition instance has sizes $(#part_ks_sizes.map(str).join(", "))$ with total sum $S = #part_ks_total$, so a balanced witness must hit exactly $S / 2 = #part_ks_capacity$. + + *Step 2 -- Build the knapsack instance.* The reduction copies each size into both the weight and the value list, producing weights $(#part_ks.target.instance.weights.map(str).join(", "))$, values $(#part_ks.target.instance.values.map(str).join(", "))$, and capacity $C = #part_ks_capacity$. No auxiliary variables are introduced, so the target has the same $#part_ks_n$ binary coordinates as the source. + + *Step 3 -- Verify the canonical witness.* The serialized witness uses the same binary vector on both sides, $bold(x) = (#part_ks_sol.source_config.map(str).join(", "))$. It selects elements at indices $\{#part_ks_selected.map(str).join(", ")\}$ with sizes $(#part_ks_selected_sizes.map(str).join(", "))$, so the chosen subset has total weight and value $#part_ks_selected_sum = #part_ks_capacity$. Hence the knapsack solution saturates the capacity and certifies a balanced partition. + + *Witness semantics.* The example DB stores one canonical balanced subset. This instance has multiple balanced partitions because several different subsets sum to $#part_ks_capacity$, but one witness is enough to demonstrate the reduction. + ], +)[ + This $O(n)$ reduction#footnote[The linear-time bound follows from a single pass that copies the source sizes into item weights and values.] @garey1979[MP9] constructs a 0-1 Knapsack instance by copying each Partition size into both the item weight and item value and setting the capacity to half the total size sum. For $n$ source elements it produces $n$ knapsack items. +][ + _Construction._ Given positive sizes $s_0, dots, s_(n-1)$ with total sum $S = sum_(i=0)^(n-1) s_i$, create one knapsack item per element and set + $ w_i = s_i, quad v_i = s_i $ + for every $i in {0, dots, n-1}$. Set the knapsack capacity to + $ C = floor(S / 2). $ + Every feasible knapsack solution is therefore a subset of the original elements, and because $w_i = v_i$, its objective value equals the same subset sum. + + _Correctness._ ($arrow.r.double$) If the Partition instance is satisfiable, some subset $A'$ has sum $S / 2$. In particular $S$ is even, so $C = S / 2$, and selecting exactly the corresponding knapsack items is feasible with value $S / 2$. No feasible knapsack solution can have value larger than $C$, because value equals weight for every item and total weight is bounded by $C$. Thus the knapsack optimum is exactly $S / 2$. ($arrow.l.double$) If the knapsack optimum is $S / 2$, then the optimum is an integer and hence $S$ must be even. The selected items have total value $S / 2$, so they also have total weight $S / 2$ because $w_i = v_i$ itemwise. Those items therefore form a subset of the original multiset whose complement has the same sum, giving a valid balanced partition. + + _Solution extraction._ Return the same binary selection vector on the original elements: item $i$ is selected in the knapsack witness if and only if element $i$ belongs to the extracted partition subset. +] + #let ks_qubo = load-example("Knapsack", "QUBO") #let ks_qubo_sol = ks_qubo.solutions.at(0) #let ks_qubo_num_items = ks_qubo.source.instance.weights.len() diff --git a/src/rules/mod.rs b/src/rules/mod.rs index d7929687b..cc19e32b8 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -31,6 +31,7 @@ pub(crate) mod minimummultiwaycut_qubo; pub(crate) mod minimumvertexcover_maximumindependentset; pub(crate) mod minimumvertexcover_minimumfeedbackvertexset; pub(crate) mod minimumvertexcover_minimumsetcovering; +pub(crate) mod partition_knapsack; pub(crate) mod sat_circuitsat; pub(crate) mod sat_coloring; pub(crate) mod sat_ksat; @@ -114,6 +115,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +fn partition_size_to_i64(value: u64) -> i64 { + i64::try_from(value) + .expect("Partition -> Knapsack requires all sizes and total_sum / 2 to fit in i64") +} + +#[reduction(overhead = { + num_items = "num_elements", +})] +impl ReduceTo for Partition { + type Result = ReductionPartitionToKnapsack; + + fn reduce_to(&self) -> Self::Result { + let weights: Vec = self + .sizes() + .iter() + .copied() + .map(partition_size_to_i64) + .collect(); + let values = weights.clone(); + let capacity = partition_size_to_i64(self.total_sum() / 2); + + ReductionPartitionToKnapsack { + target: Knapsack::new(weights, values, capacity), + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "partition_to_knapsack", + build: || { + crate::example_db::specs::rule_example_with_witness::<_, Knapsack>( + Partition::new(vec![3, 1, 1, 2, 2, 1]), + SolutionPair { + source_config: vec![1, 0, 0, 1, 0, 0], + target_config: vec![1, 0, 0, 1, 0, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/partition_knapsack.rs"] +mod tests; diff --git a/src/unit_tests/rules/partition_knapsack.rs b/src/unit_tests/rules/partition_knapsack.rs new file mode 100644 index 000000000..127247788 --- /dev/null +++ b/src/unit_tests/rules/partition_knapsack.rs @@ -0,0 +1,54 @@ +use super::*; +use crate::models::misc::Partition; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_optimization_target; +use crate::solvers::{BruteForce, Solver}; +use crate::traits::Problem; +use crate::types::SolutionSize; + +#[test] +fn test_partition_to_knapsack_closed_loop() { + let source = Partition::new(vec![3, 1, 1, 2, 2, 1]); + let reduction = ReduceTo::::reduce_to(&source); + + assert_satisfaction_round_trip_from_optimization_target( + &source, + &reduction, + "Partition -> Knapsack closed loop", + ); +} + +#[test] +fn test_partition_to_knapsack_structure() { + let source = Partition::new(vec![3, 1, 1, 2, 2, 1]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.weights(), &[3, 1, 1, 2, 2, 1]); + assert_eq!(target.values(), &[3, 1, 1, 2, 2, 1]); + assert_eq!(target.capacity(), 5); + assert_eq!(target.num_items(), source.num_elements()); +} + +#[test] +fn test_partition_to_knapsack_odd_total_is_not_satisfying() { + let source = Partition::new(vec![2, 4, 5]); + let reduction = ReduceTo::::reduce_to(&source); + let target = reduction.target_problem(); + let best = BruteForce::new() + .find_best(target) + .expect("Knapsack target should always have an optimal solution"); + + assert_eq!(target.evaluate(&best), SolutionSize::Valid(5)); + + let extracted = reduction.extract_solution(&best); + assert!(!source.evaluate(&extracted)); +} + +#[test] +#[should_panic( + expected = "Partition -> Knapsack requires all sizes and total_sum / 2 to fit in i64" +)] +fn test_partition_to_knapsack_panics_on_large_coefficients() { + let source = Partition::new(vec![(i64::MAX as u64) + 1]); + let _ = ReduceTo::::reduce_to(&source); +} From 72971e596e4aec0178b429e8bd4fc2d3d03ebaf0 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sun, 22 Mar 2026 07:59:24 +0800 Subject: [PATCH 3/3] chore: remove plan file after implementation --- .../plans/2026-03-22-partition-to-knapsack.md | 119 ------------------ 1 file changed, 119 deletions(-) delete mode 100644 docs/plans/2026-03-22-partition-to-knapsack.md diff --git a/docs/plans/2026-03-22-partition-to-knapsack.md b/docs/plans/2026-03-22-partition-to-knapsack.md deleted file mode 100644 index dffdad973..000000000 --- a/docs/plans/2026-03-22-partition-to-knapsack.md +++ /dev/null @@ -1,119 +0,0 @@ -# Plan: Add Partition -> Knapsack Reduction - -**Issue:** #202 — [Rule] Partition to Knapsack -**Skill:** add-rule - -## Information Checklist - -| # | Item | Value | -|---|------|-------| -| 1 | Source problem | `Partition` | -| 2 | Target problem | `Knapsack` | -| 3 | Reduction algorithm | Map each Partition element `s_i` to one Knapsack item with `weight_i = value_i = s_i`, cast from `u64` to `i64`, and set capacity to `floor(total_sum / 2)` | -| 4 | Solution extraction | Identity on the binary configuration vector: selected knapsack items are exactly the chosen partition subset | -| 5 | Correctness argument | A balanced partition exists iff the constructed knapsack optimum reaches `total_sum / 2`; when `weight = value`, maximizing value under capacity `floor(total_sum / 2)` is equivalent to finding the largest achievable subset sum up to that bound | -| 6 | Size overhead | `num_items = "num_elements"` | -| 7 | Concrete example | Partition sizes `[3, 1, 1, 2, 2, 1]` map to a Knapsack instance with identical weights/values and capacity `5`; witness config `[1, 0, 0, 1, 0, 0]` works on both sides | -| 8 | Solving strategy | Solve the target with `BruteForce::find_all_best()` / `find_best()`; use `assert_satisfaction_round_trip_from_optimization_target` on satisfiable instances | -| 9 | Reference | Garey & Johnson, *Computers and Intractability* (1979), Appendix A6 / MP9 (“Transformation from PARTITION”) | - -## Design Decisions - -### Problem-type bridge - -`Partition` is a satisfaction problem while `Knapsack` is an optimization problem in this codebase. The rule will therefore interpret the target optimum semantically: a source instance is satisfiable exactly when the best knapsack value is `total_sum / 2`. The reduction itself still stores only the target instance plus the identity config mapping. - -### Numeric conversion - -`Partition` stores sizes as `u64`, but `Knapsack` uses `i64`. The reduction should use explicit checked casts (`i64::try_from`) with a rule-specific panic message so overflow is caught deterministically instead of silently truncating. - -### Overhead scope - -Keep the `#[reduction(overhead = ...)]` metadata to the stable target getter that matters here: `num_items = "num_elements"`. `Knapsack::num_slack_bits()` depends on capacity with a zero-capacity special case, so forcing it into the symbolic overhead expression would complicate the rule without improving the reduction graph. - -### Repo-specific example registration - -Although the generic `add-rule` skill mentions `src/example_db/rule_builders.rs`, this repo’s current pattern is to place `canonical_rule_example_specs()` in the rule module itself and aggregate it from `src/rules/mod.rs`. Follow the in-repo pattern, not the older wording. - -## Execution Batches - -### Batch 1: Implement the rule and regenerate exported data - -#### Step 1: Add the rule module (`src/rules/partition_knapsack.rs`) - -1. Create `ReductionPartitionToKnapsack` with a `target: Knapsack` field. -2. Add a small checked-cast helper for `u64 -> i64` with an explicit panic string such as `"Partition -> Knapsack requires all sizes and total_sum / 2 to fit in i64"`. -3. Implement `ReductionResult`: - - `target_problem()` returns the stored `Knapsack`. - - `extract_solution()` returns `target_solution.to_vec()` because both problems use the same binary selection vector. -4. Implement `ReduceTo for Partition` with: - - `weights = sizes.map(cast)` - - `values = weights.clone()` - - `capacity = cast(total_sum / 2)` - - `#[reduction(overhead = { num_items = "num_elements" })]` -5. Add `#[cfg(feature = "example-db")] canonical_rule_example_specs()` in this file using the issue example and a single canonical witness. -6. Link the unit tests with `#[cfg(test)] #[path = "../unit_tests/rules/partition_knapsack.rs"] mod tests;` - -#### Step 2: Register the rule (`src/rules/mod.rs`) - -1. Add `pub(crate) mod partition_knapsack;` -2. Extend `canonical_rule_example_specs()` with `partition_knapsack::canonical_rule_example_specs()` - -#### Step 3: Add unit tests (`src/unit_tests/rules/partition_knapsack.rs`) - -1. Add a satisfiable closed-loop test using `Partition::new(vec![3, 1, 1, 2, 2, 1])` and `assert_satisfaction_round_trip_from_optimization_target(...)`. -2. Add a structure test that checks: - - target weights equal `[3, 1, 1, 2, 2, 1]` - - target values equal `[3, 1, 1, 2, 2, 1]` - - target capacity equals `5` - - `num_items()` matches `num_elements()` -3. Add an unsatisfiable/odd-total test (for example `[2, 4, 5]`) that: - - solves the target with `BruteForce::find_best()` - - extracts the source config - - asserts `source.evaluate(&extracted)` is `false` -4. Add a checked-cast panic test with a value larger than `i64::MAX`. - -#### Step 4: Regenerate the exports needed by the paper - -Run these after the rule and canonical example compile: - -```bash -cargo run --features "example-db" --example export_examples -cargo run --example export_graph -cargo run --example export_schemas -``` - -These commands must succeed before the paper step so `load-example("Partition", "Knapsack")` has backing JSON data. - -### Batch 2: Write the paper entry and run final verification - -#### Step 5: Document the rule in `docs/paper/reductions.typ` - -1. Add a `#let partition_knapsack = load-example("Partition", "Knapsack")` block near the other reduction examples. -2. Add a `#reduction-rule("Partition", "Knapsack", ...)` entry that: - - cites Garey & Johnson for the textbook reduction - - states that the reduction uses one knapsack item per partition element - - explains the satisfaction-to-optimization interpretation explicitly -3. In the proof body, include: - - `_Construction._` with `w_i = v_i = s_i` and `C = floor(sum_i s_i / 2)` - - `_Correctness._` proving `Partition` is satisfiable iff the optimum knapsack value is exactly `sum_i s_i / 2` - - `_Solution extraction._` explaining the identity mapping back to the partition subset -4. In the `extra:` tutorial block, use the canonical example JSON data rather than hardcoded values: - - `pred create --example Partition -o partition.json` - - `pred reduce partition.json --to "Knapsack" -o bundle.json` - - `pred solve bundle.json` - - `pred evaluate partition.json --config ...` -5. Note witness semantics clearly: the fixture stores one canonical balanced subset even if multiple optimal knapsack witnesses exist. - -#### Step 6: Verify the full change - -Run: - -```bash -make fmt-check -make clippy -make test -make paper -``` - -If `make paper` regenerates ignored outputs, leave ignored/generated files unstaged unless the repo already tracks them. The required committed changes are the rule/test/source files plus any tracked export fixture updates produced by the commands above.