Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 42 additions & 0 deletions docs/paper/reductions.typ
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
2 changes: 2 additions & 0 deletions src/rules/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -114,6 +115,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
specs.extend(maximummatching_maximumsetpacking::canonical_rule_example_specs());
specs.extend(maximumsetpacking_qubo::canonical_rule_example_specs());
specs.extend(minimummultiwaycut_qubo::canonical_rule_example_specs());
specs.extend(partition_knapsack::canonical_rule_example_specs());
specs.extend(minimumvertexcover_maximumindependentset::canonical_rule_example_specs());
specs.extend(minimumvertexcover_minimumfeedbackvertexset::canonical_rule_example_specs());
specs.extend(minimumvertexcover_minimumsetcovering::canonical_rule_example_specs());
Expand Down
73 changes: 73 additions & 0 deletions src/rules/partition_knapsack.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
//! Reduction from Partition to Knapsack.

use crate::models::misc::{Knapsack, Partition};
use crate::reduction;
use crate::rules::traits::{ReduceTo, ReductionResult};

/// Result of reducing Partition to Knapsack.
#[derive(Debug, Clone)]
pub struct ReductionPartitionToKnapsack {
target: Knapsack,
}

impl ReductionResult for ReductionPartitionToKnapsack {
type Source = Partition;
type Target = Knapsack;

fn target_problem(&self) -> &Self::Target {
&self.target
}

fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
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<Knapsack> for Partition {
type Result = ReductionPartitionToKnapsack;

fn reduce_to(&self) -> Self::Result {
let weights: Vec<i64> = 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<crate::example_db::specs::RuleExampleSpec> {
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;
54 changes: 54 additions & 0 deletions src/unit_tests/rules/partition_knapsack.rs
Original file line number Diff line number Diff line change
@@ -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::<Knapsack>::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::<Knapsack>::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::<Knapsack>::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::<Knapsack>::reduce_to(&source);
}
Loading