problemreductions/rules/
subsetsum_closestvectorproblem.rs

1//! Reduction from Subset Sum to CVP using binary carry equations.
2
3use crate::models::algebraic::ClosestVectorProblem;
4use crate::models::decision::Decision;
5use crate::models::misc::SubsetSum;
6use crate::reduction;
7use crate::rules::traits::{ReduceTo, ReductionResult};
8
9/// Result of reducing SubsetSum to ClosestVectorProblem.
10#[derive(Debug, Clone)]
11pub struct ReductionSubsetSumToClosestVectorProblem {
12    target: Decision<ClosestVectorProblem>,
13    num_elements: usize,
14}
15
16impl ReductionResult for ReductionSubsetSumToClosestVectorProblem {
17    type Source = SubsetSum;
18    type Target = Decision<ClosestVectorProblem>;
19
20    fn target_problem(&self) -> &Self::Target {
21        &self.target
22    }
23
24    fn extract_solution(
25        &self,
26        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
27    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
28        crate::rules::traits::validate_target_witness(
29            self.target_problem(),
30            target_solution,
31            |value| value.0,
32            "target lattice vector does not certify a subset sum",
33        )?;
34        Ok(target_solution[..self.num_elements]
35            .iter()
36            .map(|&value| value == 1)
37            .collect())
38    }
39}
40
41#[crate::aggregate_reduction(identity)]
42impl crate::rules::AggregateReductionResult for ReductionSubsetSumToClosestVectorProblem {}
43
44impl ReductionSubsetSumToClosestVectorProblem {
45    /// Check the dense representation before allocating its columns.
46    fn dimensions(
47        num_elements: usize,
48        bit_width: u64,
49    ) -> Result<(usize, usize, usize), crate::rules::ReductionError> {
50        let overflow = || {
51            crate::rules::ReductionError::integer_overflow::<
52                SubsetSum,
53                Decision<ClosestVectorProblem>,
54            >("sizing the binary-carry lattice")
55        };
56        let bits = usize::try_from(bit_width).map_err(|_| overflow())?;
57        let carries = bits.checked_sub(1).ok_or_else(overflow)?;
58        let columns = num_elements.checked_add(carries).ok_or_else(overflow)?;
59        let rows = columns
60            .checked_add(num_elements)
61            .and_then(|value| value.checked_add(1))
62            .ok_or_else(overflow)?;
63        rows.checked_mul(columns)
64            .and_then(|entries| entries.checked_mul(std::mem::size_of::<i64>()))
65            .ok_or_else(overflow)?;
66        Ok((bits, rows, columns))
67    }
68}
69
70// For r=n+k-1 columns, the selected determinant is one. Element column
71// squared norms are <=k+2, carry norms are five, and target squared norm
72// is <=n+k=r+1. For r>=1, k+4<=2^(k+2) and r+1<=2^r, so width
73// <=2^(((r-1)(k+2)+r)/2+1). Its bit length is <=r(k+3)/2+2.
74// Sum the per-coordinate bound over r columns. The empty basis has zero bits.
75#[reduction(transform = {
76    exact {
77        ambient_dimension = "2 * num_elements + max_numeric_magnitude_bits",
78        num_basis_vectors = "num_elements + max_numeric_magnitude_bits - 1",
79    },
80    upper_bound {
81        max_numeric_magnitude_bits = "2",
82        coefficient_box_bits = "(num_elements + max_numeric_magnitude_bits - 1) * ((num_elements + max_numeric_magnitude_bits - 1) * (max_numeric_magnitude_bits + 3) / 2 + 2)",
83    }
84})]
85impl ReduceTo<Decision<ClosestVectorProblem>> for SubsetSum {
86    type Result = ReductionSubsetSumToClosestVectorProblem;
87
88    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
89        let n = self.num_elements();
90        let bit_width = self.max_numeric_magnitude_bits();
91        let (bits, rows, columns) =
92            ReductionSubsetSumToClosestVectorProblem::dimensions(n, bit_width)?;
93        let mut basis = Vec::with_capacity(columns);
94        // Paired residuals x_i and x_i-1 have minimum squared contribution one,
95        // attained exactly at 0 and 1. Their leading identity gives unit pivots.
96        for (i, size) in self.sizes().iter().enumerate() {
97            let mut column = vec![0_i64; rows];
98            column[i] = 1;
99            column[n + i] = 1;
100            for bit in 0..bits {
101                column[rows - 1 - bit] = i64::from(size.bit(bit as u64));
102            }
103            basis.push(column);
104        }
105        // Carry c_k occurs with +1 in bit k and -2 in bit k-1.
106        // Descending bit rows and carry columns give unit pivots.
107        for bit in (1..bits).rev() {
108            let mut column = vec![0_i64; rows];
109            column[rows - 1 - bit] = 1;
110            column[rows - bit] = -2;
111            basis.push(column);
112        }
113        let mut target = vec![0_i64; rows];
114        target[n..2 * n].fill(1);
115        for bit in 0..bits {
116            target[rows - 1 - bit] = i64::from(self.target().bit(bit as u64));
117        }
118        let target_squared_distance =
119            <Self as ReduceTo<Decision<ClosestVectorProblem>>>::exact_i64(
120                n,
121                "representing the subset-sum squared-distance threshold",
122            )?;
123        let target = ClosestVectorProblem::new(basis, target)
124            .map_err(<Self as ReduceTo<Decision<ClosestVectorProblem>>>::target_construction)?;
125        Ok(ReductionSubsetSumToClosestVectorProblem {
126            target: Decision::new(target, target_squared_distance),
127            num_elements: n,
128        })
129    }
130}
131
132#[cfg(feature = "example-db")]
133pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
134    use crate::export::SolutionPair;
135
136    vec![crate::example_db::specs::RuleExampleSpec {
137        id: "subsetsum_to_closestvectorproblem",
138        build: || {
139            crate::example_db::specs::rule_example_with_witness::<_, Decision<ClosestVectorProblem>>(
140                SubsetSum::new(vec![3u32, 7, 1, 8], 11u32),
141                SolutionPair {
142                    source_config: serde_json::json!(vec![true, false, false, true]),
143                    target_config: serde_json::json!(vec![1, 0, 0, 1, 0, 0, 0]),
144                },
145            )
146        },
147    }]
148}
149
150#[cfg(test)]
151#[path = "../unit_tests/rules/subsetsum_closestvectorproblem.rs"]
152mod tests;
problemreductions/rules/subsetsum_closestvectorproblem.rs

problemreductions/rules/
subsetsum_closestvectorproblem.rs
