problemreductions/rules/
registersufficiency_ilp.rs

1//! Reduction from RegisterSufficiency to ILP<i32>.
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<i32>,
18    num_vertices: usize,
19}
20
21impl ReductionResult for ReductionRegisterSufficiencyToILP {
22    type Source = RegisterSufficiency;
23    type Target = ILP<i32>;
24
25    fn target_problem(&self) -> &ILP<i32> {
26        &self.target
27    }
28
29    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
30        target_solution[..self.num_vertices].to_vec()
31    }
32}
33
34#[reduction(overhead = {
35    num_vars = "3 * num_vertices^2 + num_vertices * (num_vertices - 1) / 2 + 2 * num_vertices",
36    num_constraints = "9 * num_vertices^2 + 3 * num_vertices * (num_vertices - 1) / 2 + 3 * num_vertices + 2 * num_arcs + num_sinks",
37})]
38impl ReduceTo<ILP<i32>> for RegisterSufficiency {
39    type Result = ReductionRegisterSufficiencyToILP;
40
41    fn reduce_to(&self) -> Self::Result {
42        let n = self.num_vertices();
43        let pair_list: Vec<(usize, usize)> = (0..n)
44            .flat_map(|u| ((u + 1)..n).map(move |v| (u, v)))
45            .collect();
46        let num_pair_vars = pair_list.len();
47
48        let time_offset = 0;
49        let latest_offset = n;
50        let order_offset = 2 * n;
51        let before_offset = order_offset + num_pair_vars;
52        let after_offset = before_offset + n * n;
53        let live_offset = after_offset + n * n;
54        let num_vars = live_offset + n * n;
55
56        let time_idx = |vertex: usize| -> usize { time_offset + vertex };
57        let latest_idx = |vertex: usize| -> usize { latest_offset + vertex };
58        let order_idx = |pair_idx: usize| -> usize { order_offset + pair_idx };
59        let before_idx =
60            |vertex: usize, step: usize| -> usize { before_offset + vertex * n + step };
61        let after_idx = |vertex: usize, step: usize| -> usize { after_offset + vertex * n + step };
62        let live_idx = |vertex: usize, step: usize| -> usize { live_offset + vertex * n + step };
63
64        let big_m = n as f64;
65        let mut has_dependent = vec![false; n];
66        let mut constraints = Vec::new();
67
68        for vertex in 0..n {
69            constraints.push(LinearConstraint::le(
70                vec![(time_idx(vertex), 1.0)],
71                (n.saturating_sub(1)) as f64,
72            ));
73            constraints.push(LinearConstraint::le(
74                vec![(latest_idx(vertex), 1.0)],
75                n as f64,
76            ));
77        }
78
79        for (pair_idx, &(u, v)) in pair_list.iter().enumerate() {
80            let order_var = order_idx(pair_idx);
81            constraints.push(LinearConstraint::le(vec![(order_var, 1.0)], 1.0));
82            constraints.push(LinearConstraint::ge(
83                vec![(time_idx(v), 1.0), (time_idx(u), -1.0), (order_var, -big_m)],
84                1.0 - big_m,
85            ));
86            constraints.push(LinearConstraint::ge(
87                vec![(time_idx(u), 1.0), (time_idx(v), -1.0), (order_var, big_m)],
88                1.0,
89            ));
90        }
91
92        for &(dependent, dependency) in self.arcs() {
93            has_dependent[dependency] = true;
94            constraints.push(LinearConstraint::ge(
95                vec![(time_idx(dependent), 1.0), (time_idx(dependency), -1.0)],
96                1.0,
97            ));
98            constraints.push(LinearConstraint::ge(
99                vec![(latest_idx(dependency), 1.0), (time_idx(dependent), -1.0)],
100                0.0,
101            ));
102        }
103
104        for (vertex, &has_child) in has_dependent.iter().enumerate() {
105            if !has_child {
106                constraints.push(LinearConstraint::eq(
107                    vec![(latest_idx(vertex), 1.0)],
108                    n as f64,
109                ));
110            }
111        }
112
113        for vertex in 0..n {
114            for step in 0..n {
115                let before_var = before_idx(vertex, step);
116                constraints.push(LinearConstraint::le(vec![(before_var, 1.0)], 1.0));
117                constraints.push(LinearConstraint::le(
118                    vec![(time_idx(vertex), 1.0), (before_var, big_m)],
119                    step as f64 + big_m,
120                ));
121                constraints.push(LinearConstraint::ge(
122                    vec![(time_idx(vertex), 1.0), (before_var, big_m)],
123                    (step + 1) as f64,
124                ));
125
126                let after_var = after_idx(vertex, step);
127                constraints.push(LinearConstraint::le(vec![(after_var, 1.0)], 1.0));
128                constraints.push(LinearConstraint::ge(
129                    vec![(latest_idx(vertex), 1.0), (after_var, -big_m)],
130                    (step + 1) as f64 - big_m,
131                ));
132                constraints.push(LinearConstraint::le(
133                    vec![(latest_idx(vertex), 1.0), (after_var, -big_m)],
134                    step as f64,
135                ));
136
137                let live_var = live_idx(vertex, step);
138                constraints.push(LinearConstraint::le(
139                    vec![(live_var, 1.0), (before_var, -1.0)],
140                    0.0,
141                ));
142                constraints.push(LinearConstraint::le(
143                    vec![(live_var, 1.0), (after_var, -1.0)],
144                    0.0,
145                ));
146                constraints.push(LinearConstraint::ge(
147                    vec![(live_var, 1.0), (before_var, -1.0), (after_var, -1.0)],
148                    -1.0,
149                ));
150            }
151        }
152
153        for step in 0..n {
154            let live_terms: Vec<(usize, f64)> =
155                (0..n).map(|vertex| (live_idx(vertex, step), 1.0)).collect();
156            constraints.push(LinearConstraint::le(live_terms, self.bound() as f64));
157        }
158
159        ReductionRegisterSufficiencyToILP {
160            target: ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize),
161            num_vertices: n,
162        }
163    }
164}
165
166#[cfg(feature = "example-db")]
167pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
168    vec![crate::example_db::specs::RuleExampleSpec {
169        id: "registersufficiency_to_ilp",
170        build: || {
171            let source = RegisterSufficiency::new(
172                7,
173                vec![
174                    (2, 0),
175                    (2, 1),
176                    (3, 1),
177                    (4, 2),
178                    (4, 3),
179                    (5, 0),
180                    (6, 4),
181                    (6, 5),
182                ],
183                3,
184            );
185            crate::example_db::specs::rule_example_via_ilp::<_, i32>(source)
186        },
187    }]
188}
189
190#[cfg(test)]
191#[path = "../unit_tests/rules/registersufficiency_ilp.rs"]
192mod tests;
problemreductions/rules/registersufficiency_ilp.rs

problemreductions/rules/
registersufficiency_ilp.rs
