problemreductions/rules/
ilp_i64_ilp_bool.rs

1//! Encode finitely bounded integer ILP variables as binary variables.
2
3use crate::models::algebraic::{Bounded, Comparison, LinearConstraint, ILP};
4use crate::reduction;
5use crate::rules::traits::{ReduceTo, ReductionResult};
6use crate::rules::ReductionError;
7
8#[derive(Debug, Clone)]
9struct VarEncoding {
10    lower_bound: i64,
11    start: usize,
12    weights: Vec<i64>,
13}
14
15fn overflow(operation: impl Into<String>) -> ReductionError {
16    ReductionError::integer_overflow::<ILP<i64, i64, Bounded>, ILP<bool>>(operation)
17}
18
19fn binary_weights(width: i64) -> Vec<i64> {
20    if width == 0 {
21        return Vec::new();
22    }
23    let num_bits = 64 - width.leading_zeros() as usize;
24    let mut weights = Vec::with_capacity(num_bits);
25    for bit in 0..num_bits - 1 {
26        weights.push(1_i64 << bit);
27    }
28    weights.push(width - ((1_i64 << (num_bits - 1)) - 1));
29    weights
30}
31
32fn encoded_constraint(
33    constraint: &LinearConstraint,
34    encodings: &[VarEncoding],
35) -> Result<LinearConstraint, ReductionError> {
36    let mut terms = Vec::new();
37    let mut constant = 0_i64;
38    for &(variable, coefficient) in constraint.terms() {
39        let encoding = &encodings[variable];
40        constant = constant
41            .checked_add(
42                coefficient
43                    .checked_mul(encoding.lower_bound)
44                    .ok_or_else(|| {
45                        overflow("multiplying an ILP row coefficient by a lower bound")
46                    })?,
47            )
48            .ok_or_else(|| overflow("summing the lower-bound shift of an ILP row"))?;
49        for (offset, &weight) in encoding.weights.iter().enumerate() {
50            terms.push((
51                encoding.start + offset,
52                coefficient
53                    .checked_mul(weight)
54                    .ok_or_else(|| overflow("encoding an integer ILP row coefficient"))?,
55            ));
56        }
57    }
58    let rhs = constraint
59        .rhs()
60        .checked_sub(constant)
61        .ok_or_else(|| overflow("shifting an integer ILP right-hand side"))?;
62    Ok(match constraint.comparison() {
63        Comparison::Le => LinearConstraint::le(terms, rhs),
64        Comparison::Ge => LinearConstraint::ge(terms, rhs),
65        Comparison::Eq => LinearConstraint::eq(terms, rhs),
66    })
67}
68
69#[derive(Debug, Clone)]
70pub struct ReductionIntILPToBinaryILP {
71    target: ILP<bool>,
72    encodings: Vec<VarEncoding>,
73}
74
75impl ReductionResult for ReductionIntILPToBinaryILP {
76    type Source = ILP<i64, i64, Bounded>;
77    type Target = ILP<bool>;
78
79    fn target_problem(&self) -> &ILP<bool> {
80        &self.target
81    }
82
83    fn extract_solution(
84        &self,
85        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
86    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
87        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
88        self.encodings
89            .iter()
90            .map(|encoding| {
91                encoding.weights.iter().enumerate().try_fold(
92                    encoding.lower_bound,
93                    |value, (offset, &weight)| {
94                        let term = weight
95                            .checked_mul(target_solution[encoding.start + offset])
96                            .ok_or_else(|| {
97                                crate::rules::ExtractionError::invalid(
98                                    "binary ILP decoding multiplication overflowed i64",
99                                )
100                            })?;
101                        value.checked_add(term).ok_or_else(|| {
102                            crate::rules::ExtractionError::invalid(
103                                "binary ILP decoding sum overflowed i64",
104                            )
105                        })
106                    },
107                )
108            })
109            .collect()
110    }
111}
112
113// If all finite endpoints and row entries have magnitude below 2^h, widths
114// need at most h+1 bits. Encoded coefficients are below 2^(2h+1), and the
115// lower-bound shift gives |b'| < 2^h + n*2^(2h) < 2^(2h+n+1).
116#[reduction(
117    transform = {
118        exact {
119            num_constraints = "num_constraints",
120        },
121        upper_bound {
122            num_vars = "num_vars * (max_constraint_magnitude_bits + 1)",
123            num_nonzeros = "num_nonzeros * (max_constraint_magnitude_bits + 1)",
124            max_constraint_magnitude_bits = "2 * max_constraint_magnitude_bits + num_vars + 1",
125        },
126    },
127)]
128impl ReduceTo<ILP<bool>> for ILP<i64, i64, Bounded> {
129    type Result = ReductionIntILPToBinaryILP;
130
131    fn reduce_to(&self) -> Result<Self::Result, ReductionError> {
132        let mut encodings = Vec::with_capacity(self.num_vars());
133        let mut num_binary_variables = 0_usize;
134        for variable in self.variables() {
135            let lower_bound = variable.lower_bound().expect("bounded ILP lower bound");
136            let upper_bound = variable.upper_bound().expect("bounded ILP upper bound");
137            let width = upper_bound
138                .checked_sub(lower_bound)
139                .ok_or_else(|| overflow("computing an integer variable interval width"))?;
140            let weights = binary_weights(width);
141            let num_weights = weights.len();
142            encodings.push(VarEncoding {
143                lower_bound,
144                start: num_binary_variables,
145                weights,
146            });
147            num_binary_variables = num_binary_variables
148                .checked_add(num_weights)
149                .ok_or_else(|| overflow("counting binary encoding variables"))?;
150        }
151
152        let constraints = self
153            .constraints()
154            .iter()
155            .map(|constraint| encoded_constraint(constraint, &encodings))
156            .collect::<Result<Vec<_>, _>>()?;
157
158        let mut objective = Vec::new();
159        for &(variable, coefficient) in self.objective() {
160            let encoding = &encodings[variable];
161            for (offset, &weight) in encoding.weights.iter().enumerate() {
162                let encoded_coefficient = coefficient
163                    .checked_mul(weight)
164                    .ok_or_else(|| overflow("encoding an integer ILP objective coefficient"))?;
165                objective.push((encoding.start + offset, encoded_coefficient));
166            }
167        }
168
169        Ok(ReductionIntILPToBinaryILP {
170            target: ILP::<bool>::new(num_binary_variables, constraints, objective, self.sense())
171                .map_err(<Self as ReduceTo<ILP<bool>>>::target_construction)?,
172            encodings,
173        })
174    }
175}
176
177#[cfg(test)]
178#[path = "../unit_tests/rules/ilp_i64_ilp_bool.rs"]
179mod tests;
problemreductions/rules/ilp_i64_ilp_bool.rs

problemreductions/rules/
ilp_i64_ilp_bool.rs
