problemreductions/rules/
subsetsum_integerexpressionmembership.rs

1use crate::models::misc::SubsetSum;
2use crate::models::misc::{IntExpr, IntegerExpressionMembership};
3use crate::reduction;
4use crate::rules::traits::{ReduceTo, ReductionResult};
5use num_traits::ToPrimitive;
6
7#[derive(Debug, Clone)]
8pub struct ReductionSubsetSumToIntegerExpressionMembership {
9    target: IntegerExpressionMembership,
10}
11
12impl ReductionResult for ReductionSubsetSumToIntegerExpressionMembership {
13    type Source = SubsetSum;
14    type Target = IntegerExpressionMembership;
15
16    fn target_problem(&self) -> &Self::Target {
17        &self.target
18    }
19
20    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
21        // Union choice 0 = left = Atom(1) = exclude, choice 1 = right = Atom(s_i+1) = include.
22        // This maps directly to SubsetSum's 0/1 include/exclude encoding.
23        target_solution.to_vec()
24    }
25}
26
27/// Build a left-associative chain of `Sum` nodes over the given union nodes.
28///
29/// For n items with sizes s_0, ..., s_{n-1}, each item becomes
30/// `Union(Atom(1), Atom(s_i + 1))`. The chain is built as:
31/// `Sum(Sum(...Sum(Union_0, Union_1), Union_2), ..., Union_{n-1})`.
32///
33/// DFS order visits Union_0 first, then Union_1, etc., so config[i]
34/// corresponds to item i.
35fn build_expression(sizes: &[u64]) -> IntExpr {
36    assert!(
37        !sizes.is_empty(),
38        "SubsetSum must have at least one element"
39    );
40
41    let make_union = |s: u64| -> IntExpr {
42        IntExpr::Union(Box::new(IntExpr::Atom(1)), Box::new(IntExpr::Atom(s + 1)))
43    };
44
45    let mut expr = make_union(sizes[0]);
46    for &s in &sizes[1..] {
47        expr = IntExpr::Sum(Box::new(expr), Box::new(make_union(s)));
48    }
49    expr
50}
51
52#[reduction(overhead = {
53    num_union_nodes = "num_elements",
54})]
55impl ReduceTo<IntegerExpressionMembership> for SubsetSum {
56    type Result = ReductionSubsetSumToIntegerExpressionMembership;
57
58    fn reduce_to(&self) -> Self::Result {
59        let sizes: Vec<u64> = self
60            .sizes()
61            .iter()
62            .map(|size| size.to_u64().unwrap())
63            .collect();
64
65        let shift = u64::try_from(self.num_elements())
66            .expect("SubsetSum -> IntegerExpressionMembership requires num_elements to fit in u64");
67        let target = self.target().to_u64().unwrap().checked_add(shift).expect(
68            "SubsetSum -> IntegerExpressionMembership requires shifted target to fit in u64",
69        );
70
71        let expr = build_expression(&sizes);
72
73        ReductionSubsetSumToIntegerExpressionMembership {
74            target: IntegerExpressionMembership::new(expr, target),
75        }
76    }
77}
78
79#[cfg(feature = "example-db")]
80pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
81    use crate::export::SolutionPair;
82
83    vec![crate::example_db::specs::RuleExampleSpec {
84        id: "subsetsum_to_integerexpressionmembership",
85        build: || {
86            crate::example_db::specs::rule_example_with_witness::<_, IntegerExpressionMembership>(
87                SubsetSum::new(vec![1u32, 5, 6, 8], 11u32),
88                SolutionPair {
89                    source_config: vec![0, 1, 1, 0],
90                    target_config: vec![0, 1, 1, 0],
91                },
92            )
93        },
94    }]
95}
96
97#[cfg(test)]
98#[path = "../unit_tests/rules/subsetsum_integerexpressionmembership.rs"]
99mod tests;
problemreductions/rules/subsetsum_integerexpressionmembership.rs

problemreductions/rules/
subsetsum_integerexpressionmembership.rs
