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(
21        &self,
22        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
23    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
24        crate::rules::traits::validate_target_witness(
25            self.target_problem(),
26            target_solution,
27            |value| value.0,
28            "target witness does not satisfy the target problem",
29        )?;
30
31        Ok({
32            // Union choice 0 = left = Atom(1) = exclude, choice 1 = right = Atom(s_i+1) = include.
33            // This maps directly to SubsetSum's 0/1 include/exclude encoding.
34            target_solution.to_vec()
35        })
36    }
37}
38
39/// Build a left-associative chain of `Sum` nodes over the given union nodes.
40///
41/// For n items with sizes s_0, ..., s_{n-1}, each item becomes
42/// `Union(Atom(1), Atom(s_i + 1))`. The chain is built as:
43/// `Sum(Sum(...Sum(Union_0, Union_1), Union_2), ..., Union_{n-1})`.
44///
45/// DFS order visits Union_0 first, then Union_1, etc., so config[i]
46/// corresponds to item i.
47fn build_expression(sizes: &[i64]) -> Result<IntExpr, &'static str> {
48    let make_union = |size: i64| -> Result<IntExpr, &'static str> {
49        let included = size
50            .checked_add(1)
51            .ok_or("an item size cannot be shifted into the target expression domain")?;
52        Ok(IntExpr::Union(
53            Box::new(IntExpr::Atom(1)),
54            Box::new(IntExpr::Atom(included)),
55        ))
56    };
57
58    let mut sizes = sizes.iter().copied();
59    let first = sizes
60        .next()
61        .ok_or("the target expression requires at least one source item")?;
62    let mut expr = make_union(first)?;
63    for size in sizes {
64        expr = IntExpr::Sum(Box::new(expr), Box::new(make_union(size)?));
65    }
66    Ok(expr)
67}
68
69#[crate::aggregate_reduction(identity)]
70impl crate::rules::AggregateReductionResult for ReductionSubsetSumToIntegerExpressionMembership {}
71
72#[reduction(
73    transform = exact {
74        num_union_nodes = "num_elements",
75    })]
76impl ReduceTo<IntegerExpressionMembership> for SubsetSum {
77    type Result = ReductionSubsetSumToIntegerExpressionMembership;
78
79    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
80        let sizes: Vec<i64> = self
81            .sizes()
82            .iter()
83            .map(|size| {
84                size.to_i64().ok_or_else(|| {
85                    crate::rules::ReductionError::invalid_target::<
86                        SubsetSum,
87                        IntegerExpressionMembership,
88                    >("subset size does not fit the target i64 domain")
89                })
90            })
91            .collect::<Result<_, _>>()?;
92
93        let shift =
94            i64::try_from(self.num_elements()).map_err(|_| {
95                crate::rules::ReductionError::integer_overflow::<
96                    SubsetSum,
97                    IntegerExpressionMembership,
98                >("converting the number of elements to i64")
99            })?;
100        let source_target = self.target().to_i64().ok_or_else(|| {
101            crate::rules::ReductionError::invalid_target::<SubsetSum, IntegerExpressionMembership>(
102                "subset target does not fit the target i64 domain",
103            )
104        })?;
105        let target =
106            source_target.checked_add(shift).ok_or_else(|| {
107                crate::rules::ReductionError::integer_overflow::<
108                    SubsetSum,
109                    IntegerExpressionMembership,
110                >("computing the shifted target")
111            })?;
112
113        let expr = build_expression(&sizes).map_err(|message| {
114            crate::rules::ReductionError::invalid_target::<SubsetSum, IntegerExpressionMembership>(
115                message,
116            )
117        })?;
118
119        Ok(ReductionSubsetSumToIntegerExpressionMembership {
120            target: IntegerExpressionMembership::new(expr, target),
121        })
122    }
123}
124
125#[cfg(feature = "example-db")]
126pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
127    use crate::export::SolutionPair;
128
129    vec![crate::example_db::specs::RuleExampleSpec {
130        id: "subsetsum_to_integerexpressionmembership",
131        build: || {
132            crate::example_db::specs::rule_example_with_witness::<_, IntegerExpressionMembership>(
133                SubsetSum::new(vec![1u32, 5, 6, 8], 11u32),
134                SolutionPair {
135                    source_config: serde_json::json!(vec![false, true, true, false]),
136                    target_config: serde_json::json!(vec![false, true, true, false]),
137                },
138            )
139        },
140    }]
141}
142
143#[cfg(test)]
144#[path = "../unit_tests/rules/subsetsum_integerexpressionmembership.rs"]
145mod tests;
problemreductions/rules/subsetsum_integerexpressionmembership.rs

problemreductions/rules/
subsetsum_integerexpressionmembership.rs
