problemreductions/rules/
registersufficiency_ilp.rs

1//! Reduction from RegisterSufficiency to `ILP<i64>`.
2//!
3//! The formulation uses:
4//! - integer `t_v` variables for evaluation positions
5//! - integer `l_v` variables for latest-use positions
6//! - binary pair-order selectors to force a permutation of `0..n-1`
7//! - binary threshold/live indicators to count how many values are live after
8//!   each evaluation step
9
10use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
11use crate::models::misc::RegisterSufficiency;
12use crate::reduction;
13use crate::rules::traits::{ReduceTo, ReductionResult};
14
15#[derive(Debug, Clone)]
16pub struct ReductionRegisterSufficiencyToILP {
17    target: ILP<i64>,
18    num_vertices: usize,
19}
20
21impl ReductionResult for ReductionRegisterSufficiencyToILP {
22    type Source = RegisterSufficiency;
23    type Target = ILP<i64>;
24
25    fn target_problem(&self) -> &ILP<i64> {
26        &self.target
27    }
28
29    fn extract_solution(
30        &self,
31        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
32    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
33        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
34
35        crate::rules::ilp_helpers::decode_usize_values(&target_solution[..self.num_vertices])
36    }
37}
38
39#[reduction(
40    transform = exact {
41        num_vars = "3 * num_vertices^2 + num_vertices * (num_vertices - 1) / 2 + 2 * num_vertices",
42        num_constraints = "9 * num_vertices^2 + 3 * num_vertices * (num_vertices - 1) / 2 + 3 * num_vertices + 2 * num_arcs + num_sinks",
43    },
44    unavailable = {
45        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
46    }
47)]
48impl ReduceTo<ILP<i64>> for RegisterSufficiency {
49    type Result = ReductionRegisterSufficiencyToILP;
50
51    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
52        let n = self.num_vertices();
53        let pair_list: Vec<(usize, usize)> = (0..n)
54            .flat_map(|u| ((u + 1)..n).map(move |v| (u, v)))
55            .collect();
56        let num_pair_vars = pair_list.len();
57
58        let time_offset = 0;
59        let latest_offset = n;
60        let order_offset = 2 * n;
61        let before_offset = order_offset + num_pair_vars;
62        let after_offset = before_offset + n * n;
63        let live_offset = after_offset + n * n;
64        let num_vars = live_offset + n * n;
65
66        let time_idx = |vertex: usize| -> usize { time_offset + vertex };
67        let latest_idx = |vertex: usize| -> usize { latest_offset + vertex };
68        let order_idx = |pair_idx: usize| -> usize { order_offset + pair_idx };
69        let before_idx =
70            |vertex: usize, step: usize| -> usize { before_offset + vertex * n + step };
71        let after_idx = |vertex: usize, step: usize| -> usize { after_offset + vertex * n + step };
72        let live_idx = |vertex: usize, step: usize| -> usize { live_offset + vertex * n + step };
73
74        let big_m = Self::exact_i64(n, "representing the schedule length in ILP rows")?;
75        let latest_time = big_m;
76        let maximum_time = Self::exact_i64(
77            n.saturating_sub(1),
78            "representing the maximum schedule time in ILP rows",
79        )?;
80        let mut has_dependent = vec![false; n];
81        let mut constraints = Vec::new();
82
83        for vertex in 0..n {
84            constraints.push(LinearConstraint::le(
85                vec![(time_idx(vertex), 1)],
86                maximum_time,
87            ));
88            constraints.push(LinearConstraint::le(
89                vec![(latest_idx(vertex), 1)],
90                latest_time,
91            ));
92        }
93
94        for (pair_idx, &(u, v)) in pair_list.iter().enumerate() {
95            let order_var = order_idx(pair_idx);
96            constraints.push(LinearConstraint::le(vec![(order_var, 1)], 1));
97            constraints.push(LinearConstraint::ge(
98                vec![(time_idx(v), 1), (time_idx(u), -1), (order_var, -big_m)],
99                1 - big_m,
100            ));
101            constraints.push(LinearConstraint::ge(
102                vec![(time_idx(u), 1), (time_idx(v), -1), (order_var, big_m)],
103                1,
104            ));
105        }
106
107        for &(dependent, dependency) in self.arcs() {
108            has_dependent[dependency] = true;
109            constraints.push(LinearConstraint::ge(
110                vec![(time_idx(dependent), 1), (time_idx(dependency), -1)],
111                1,
112            ));
113            constraints.push(LinearConstraint::ge(
114                vec![(latest_idx(dependency), 1), (time_idx(dependent), -1)],
115                0,
116            ));
117        }
118
119        for (vertex, &has_child) in has_dependent.iter().enumerate() {
120            if !has_child {
121                constraints.push(LinearConstraint::eq(
122                    vec![(latest_idx(vertex), 1)],
123                    latest_time,
124                ));
125            }
126        }
127
128        for vertex in 0..n {
129            for step in 0..n {
130                let step_value = Self::exact_i64(step, "representing a schedule step in ILP rows")?;
131                let before_var = before_idx(vertex, step);
132                constraints.push(LinearConstraint::le(vec![(before_var, 1)], 1));
133                constraints.push(LinearConstraint::le(
134                    vec![(time_idx(vertex), 1), (before_var, big_m)],
135                    step_value + big_m,
136                ));
137                constraints.push(LinearConstraint::ge(
138                    vec![(time_idx(vertex), 1), (before_var, big_m)],
139                    step_value + 1,
140                ));
141
142                let after_var = after_idx(vertex, step);
143                constraints.push(LinearConstraint::le(vec![(after_var, 1)], 1));
144                constraints.push(LinearConstraint::ge(
145                    vec![(latest_idx(vertex), 1), (after_var, -big_m)],
146                    step_value + 1 - big_m,
147                ));
148                constraints.push(LinearConstraint::le(
149                    vec![(latest_idx(vertex), 1), (after_var, -big_m)],
150                    step_value,
151                ));
152
153                let live_var = live_idx(vertex, step);
154                constraints.push(LinearConstraint::le(
155                    vec![(live_var, 1), (before_var, -1)],
156                    0,
157                ));
158                constraints.push(LinearConstraint::le(
159                    vec![(live_var, 1), (after_var, -1)],
160                    0,
161                ));
162                constraints.push(LinearConstraint::ge(
163                    vec![(live_var, 1), (before_var, -1), (after_var, -1)],
164                    -1,
165                ));
166            }
167        }
168
169        for step in 0..n {
170            let live_terms: Vec<(usize, i64)> =
171                (0..n).map(|vertex| (live_idx(vertex, step), 1)).collect();
172            constraints.push(LinearConstraint::le(
173                live_terms,
174                Self::exact_i64(
175                    self.bound(),
176                    "representing the register bound in an ILP row",
177                )?,
178            ));
179        }
180
181        Ok(ReductionRegisterSufficiencyToILP {
182            target: ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize)
183                .map_err(Self::target_construction)?,
184            num_vertices: n,
185        })
186    }
187}
188
189#[cfg(feature = "example-db")]
190pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
191    vec![crate::example_db::specs::RuleExampleSpec {
192        id: "registersufficiency_to_ilp",
193        build: || {
194            let source = RegisterSufficiency::new(
195                7,
196                vec![
197                    (2, 0),
198                    (2, 1),
199                    (3, 1),
200                    (4, 2),
201                    (4, 3),
202                    (5, 0),
203                    (6, 4),
204                    (6, 5),
205                ],
206                3,
207            );
208            crate::example_db::specs::rule_example_via_ilp::<_, i64>(source)
209        },
210    }]
211}
212
213#[cfg(test)]
214#[path = "../unit_tests/rules/registersufficiency_ilp.rs"]
215mod tests;
problemreductions/rules/registersufficiency_ilp.rs

problemreductions/rules/
registersufficiency_ilp.rs
