1use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
19use crate::models::misc::SequencingWithDeadlinesAndSetUpTimes;
20use crate::reduction;
21use crate::rules::ilp_helpers::one_hot_decode;
22use crate::rules::traits::{ReduceTo, ReductionResult};
23
24#[derive(Debug, Clone)]
26pub struct ReductionSWDSTToILP {
27 target: ILP<bool>,
28 num_tasks: usize,
29}
30
31impl ReductionResult for ReductionSWDSTToILP {
32 type Source = SequencingWithDeadlinesAndSetUpTimes;
33 type Target = ILP<bool>;
34
35 fn target_problem(&self) -> &ILP<bool> {
36 &self.target
37 }
38
39 fn extract_solution(
40 &self,
41 target_solution: &<Self::Target as crate::traits::Problem>::Solution,
42 ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
43 crate::rules::traits::validate_target_witness(
44 self.target_problem(),
45 target_solution,
46 |value| value.value.is_some(),
47 "target ILP assignment is infeasible",
48 )?;
49
50 Ok({
51 let n = self.num_tasks;
52 one_hot_decode(target_solution, n, n, 0)?
54 })
55 }
56}
57
58#[crate::aggregate_reduction(ilp_feasibility)]
59impl crate::rules::AggregateReductionResult for ReductionSWDSTToILP {}
60
61#[reduction(
62 transform = upper_bound {
63 max_constraint_magnitude_bits = "max_time_bits + num_tasks + 2",
64 num_vars = "2 * num_tasks^2 + num_tasks",
65 num_constraints = "2 * num_tasks + num_tasks^2 * (num_tasks - 1) + 3 * num_tasks * (num_tasks - 1) + num_tasks * num_tasks",
66 num_nonzeros = "(2 * num_tasks^2 + num_tasks) * (2 * num_tasks + num_tasks^2 * (num_tasks - 1) + 3 * num_tasks * (num_tasks - 1) + num_tasks * num_tasks)",
67 },
68)]
69impl ReduceTo<ILP<bool>> for SequencingWithDeadlinesAndSetUpTimes {
70 type Result = ReductionSWDSTToILP;
71
72 fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
73 let n = self.num_tasks();
74
75 if n == 0 {
77 return Ok(ReductionSWDSTToILP {
78 target: ILP::new(0, vec![], vec![], ObjectiveSense::Minimize)
79 .map_err(Self::target_construction)?,
80 num_tasks: 0,
81 });
82 }
83
84 let num_x = n * n;
90 let sw_offset = num_x;
91 let a_offset = sw_offset + (n - 1);
92 let num_vars = a_offset + n * (n - 1);
93
94 let x_var = |j: usize, p: usize| -> usize { j * n + p };
95 let sw_var = |p: usize| -> usize { sw_offset + (p - 1) }; let a_var = |j: usize, p: usize| -> usize { a_offset + j * (n - 1) + (p - 1) }; let lengths = self.lengths();
99 let deadlines = self.deadlines();
100 let compilers = self.compilers();
101 let setup_times = self.setup_times();
102
103 let total_length = lengths.iter().try_fold(0_i64, |total, &length| {
105 total.checked_add(length).ok_or_else(|| {
106 crate::rules::ReductionError::integer_overflow::<
107 SequencingWithDeadlinesAndSetUpTimes,
108 ILP<bool>,
109 >("summing task lengths")
110 })
111 })?;
112 let max_setup: i64 = setup_times.iter().copied().max().unwrap_or(0);
113 let transition_count = Self::exact_i64(
114 n - 1,
115 "converting the number of compiler transitions to i64",
116 )?;
117 let big_m = max_setup
118 .checked_mul(transition_count)
119 .and_then(|setup_total| total_length.checked_add(setup_total))
120 .ok_or_else(|| {
121 crate::rules::ReductionError::integer_overflow::<
122 SequencingWithDeadlinesAndSetUpTimes,
123 ILP<bool>,
124 >("computing the scheduling big-M bound")
125 })?;
126 let mut constraints = Vec::new();
127
128 for j in 0..n {
130 let terms: Vec<(usize, i64)> = (0..n).map(|p| (x_var(j, p), 1)).collect();
131 constraints.push(LinearConstraint::eq(terms, 1));
132 }
133
134 for p in 0..n {
136 let terms: Vec<(usize, i64)> = (0..n).map(|j| (x_var(j, p), 1)).collect();
137 constraints.push(LinearConstraint::eq(terms, 1));
138 }
139
140 for p in 1..n {
142 for j in 0..n {
146 for j_prev in 0..n {
147 if compilers[j] != compilers[j_prev] {
148 constraints.push(LinearConstraint::le(
151 vec![(x_var(j, p), 1), (x_var(j_prev, p - 1), 1), (sw_var(p), -1)],
152 1,
153 ));
154 }
155 }
156 }
157
158 for j in 0..n {
163 constraints.push(LinearConstraint::le(
165 vec![(a_var(j, p), 1), (x_var(j, p), -1)],
166 0,
167 ));
168 constraints.push(LinearConstraint::le(
170 vec![(a_var(j, p), 1), (sw_var(p), -1)],
171 0,
172 ));
173 constraints.push(LinearConstraint::le(
176 vec![(x_var(j, p), 1), (sw_var(p), 1), (a_var(j, p), -1)],
177 1,
178 ));
179 }
180 }
181
182 for j in 0..n {
209 for p in 0..n {
210 let mut terms: Vec<(usize, i64)> = Vec::new();
211 terms.push((x_var(j, p), big_m));
213 for pp in 0..p {
215 for (jj, &length) in lengths.iter().enumerate() {
216 terms.push((x_var(jj, pp), length));
217 }
218 }
219 for pp in 1..=p {
221 for jj in 0..n {
222 let s = setup_times[compilers[jj]];
223 if s > 0 {
224 terms.push((a_var(jj, pp), s));
225 }
226 }
227 }
228 let rhs = deadlines[j]
229 .checked_sub(lengths[j])
230 .and_then(|value| value.checked_add(big_m))
231 .ok_or_else(|| {
232 crate::rules::ReductionError::integer_overflow::<
233 SequencingWithDeadlinesAndSetUpTimes,
234 ILP<bool>,
235 >("computing a deadline constraint bound")
236 })?;
237 constraints.push(LinearConstraint::le(terms, rhs));
238 }
239 }
240
241 Ok(ReductionSWDSTToILP {
242 target: ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize)
243 .map_err(Self::target_construction)?,
244 num_tasks: n,
245 })
246 }
247}
248
249#[cfg(feature = "example-db")]
250pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
251 vec![crate::example_db::specs::RuleExampleSpec {
252 id: "sequencingwithdeadlinesandsetuptimes_to_ilp",
253 build: || {
254 let source = SequencingWithDeadlinesAndSetUpTimes::new(
255 vec![2, 3, 1, 2, 2],
256 vec![4, 11, 3, 16, 7],
257 vec![0, 1, 0, 1, 0],
258 vec![1, 2],
259 );
260 crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
261 },
262 }]
263}
264
265#[cfg(test)]
266#[path = "../unit_tests/rules/sequencingwithdeadlinesandsetuptimes_ilp.rs"]
267mod tests;