Skip to main content

problemreductions/rules/
registersufficiency_ilp.rs

1//! Binary cumulative evaluation and live-value indicators for register sufficiency.
2
3use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
4use crate::models::misc::RegisterSufficiency;
5use crate::reduction;
6use crate::rules::traits::{ReduceTo, ReductionResult};
7
8#[derive(Debug, Clone)]
9pub struct ReductionRegisterSufficiencyToILP {
10    target: ILP<bool>,
11    num_vertices: usize,
12}
13
14impl ReductionResult for ReductionRegisterSufficiencyToILP {
15    type Source = RegisterSufficiency;
16    type Target = ILP<bool>;
17
18    fn target_problem(&self) -> &ILP<bool> {
19        &self.target
20    }
21
22    fn extract_solution(
23        &self,
24        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
25    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
26        crate::rules::traits::validate_target_witness(
27            self.target_problem(),
28            target_solution,
29            |value| value.value.is_some(),
30            "target ILP assignment is infeasible",
31        )?;
32
33        let n = self.num_vertices;
34        (0..n)
35            .map(|v| {
36                target_solution[v * n..(v + 1) * n]
37                    .iter()
38                    .position(|&computed| computed != 0)
39                    .ok_or_else(|| {
40                        crate::rules::ExtractionError::invalid("vertex is never computed")
41                    })
42            })
43            .collect()
44    }
45}
46
47#[crate::aggregate_reduction(ilp_feasibility)]
48impl crate::rules::AggregateReductionResult for ReductionRegisterSufficiencyToILP {}
49
50#[reduction(transform = {
51    exact {
52        num_vars = "2 * num_vertices^2 - num_vertices * num_sinks",
53        num_constraints = "num_vertices^2 + 2 * num_vertices * num_arcs + num_vertices",
54        num_nonzeros = "4 * num_vertices^2 - 2 * num_vertices + 5 * num_vertices * num_arcs - num_arcs",
55    },
56    upper_bound {
57        max_constraint_magnitude_bits = "num_vertices + 1",
58    },
59})]
60impl ReduceTo<ILP<bool>> for RegisterSufficiency {
61    type Result = ReductionRegisterSufficiencyToILP;
62
63    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
64        let n = self.num_vertices();
65        let overflow = || {
66            crate::rules::ReductionError::integer_overflow::<Self, ILP<bool>>(
67                "counting cumulative scheduling variables",
68            )
69        };
70        let square = n.checked_mul(n).ok_or_else(overflow)?;
71        let mut has_dependent = vec![false; n];
72        for &(_, u) in self.arcs() {
73            has_dependent[u] = true;
74        }
75        let non_sinks = has_dependent.iter().filter(|&&value| value).count();
76        let num_vars = n
77            .checked_mul(non_sinks)
78            .and_then(|count| square.checked_add(count))
79            .ok_or_else(overflow)?;
80        let horizon = Self::exact_i64(n, "bounding schedule row sums")?;
81        let bound = Self::exact_i64(self.bound(), "representing the register bound")?.min(horizon);
82        let computed = |v: usize, t: usize| v * n + t;
83        let mut live_offset: Vec<_> = (0..n).map(|v| v * n).collect();
84        let mut next = square;
85        for (v, &needed) in has_dependent.iter().enumerate() {
86            if needed {
87                live_offset[v] = next;
88                next += n;
89            }
90        }
91        let mut constraints = Vec::new();
92        for v in 0..n {
93            for t in 0..n.saturating_sub(1) {
94                constraints.push(LinearConstraint::le(
95                    vec![(computed(v, t), 1), (computed(v, t + 1), -1)],
96                    0,
97                ));
98            }
99        }
100        for t in 0..n {
101            constraints.push(LinearConstraint::eq(
102                (0..n).map(|v| (computed(v, t), 1)).collect(),
103                Self::exact_i64(t + 1, "counting completed vertices")?,
104            ));
105        }
106        for &(w, u) in self.arcs() {
107            for t in 0..n {
108                let mut precedence = vec![(computed(w, t), 1)];
109                if t > 0 {
110                    precedence.push((computed(u, t - 1), -1));
111                }
112                constraints.push(LinearConstraint::le(precedence, 0));
113                constraints.push(LinearConstraint::ge(
114                    vec![
115                        (live_offset[u] + t, 1),
116                        (computed(u, t), -1),
117                        (computed(w, t), 1),
118                    ],
119                    0,
120                ));
121            }
122        }
123        for t in 0..n {
124            // For sinks, computed bits are also their exact live indicators.
125            constraints.push(LinearConstraint::le(
126                live_offset.iter().map(|&offset| (offset + t, 1)).collect(),
127                bound,
128            ));
129        }
130
131        Ok(ReductionRegisterSufficiencyToILP {
132            target: ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize)
133                .map_err(Self::target_construction)?,
134            num_vertices: n,
135        })
136    }
137}
138
139#[cfg(feature = "example-db")]
140pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
141    vec![crate::example_db::specs::RuleExampleSpec {
142        id: "registersufficiency_to_ilp",
143        build: || {
144            let source = RegisterSufficiency::new(
145                7,
146                vec![
147                    (2, 0),
148                    (2, 1),
149                    (3, 1),
150                    (4, 2),
151                    (4, 3),
152                    (5, 0),
153                    (6, 4),
154                    (6, 5),
155                ],
156                3,
157            );
158            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
159        },
160    }]
161}
162
163#[cfg(test)]
164#[path = "../unit_tests/rules/registersufficiency_ilp.rs"]
165mod tests;