Skip to main content

problemreductions/rules/
sequencingwithdeadlinesandsetuptimes_ilp.rs

1//! Reduction from SequencingWithDeadlinesAndSetUpTimes to `ILP<bool>`.
2//!
3//! Position-assignment ILP with compiler-switch detection.
4//!
5//! Variables:
6//! - `x_{j,p}` binary: task j occupies position p  (n*n variables)
7//! - `sw_p`    binary: a compiler switch occurs before position p (n-1 variables, p >= 1)
8//! - `a_{j,p}` binary: x_{j,p} = 1 AND sw_p = 1   (n*(n-1) variables, p >= 1)
9//!
10//! The completion time of task j at position p equals the sum of all task
11//! lengths up to and including position p, plus the setup times for switches
12//! at each position 1..=p. Using the `a_{j,p}` linearisation, the setup
13//! contribution at position p is `sum_j s[k(j)] * a_{j,p}`.
14//!
15//! Deadline enforcement uses the standard big-M trick: for each (j, p),
16//! if `x_{j,p}=1` then the completion time at p must not exceed `d[j]`.
17
18use 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/// Result of reducing SequencingWithDeadlinesAndSetUpTimes to `ILP<bool>`.
25#[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            // x_{j,p} occupies the first n*n variables: decode the permutation.
53            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        // Handle empty case.
76        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        // Variable layout:
85        //   x_{j,p}   = j*n + p          for j,p in 0..n        → indices 0..n*n
86        //   sw_p       = n*n + (p-1)      for p in 1..n          → indices n*n .. n*n+(n-1)
87        //   a_{j,p}    = n*n+(n-1)+j*(n-1)+(p-1)  for j in 0..n, p in 1..n
88        //                                           → indices n*n+(n-1) .. n*n+(n-1)+n*(n-1)
89        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) }; // p >= 1
96        let a_var = |j: usize, p: usize| -> usize { a_offset + j * (n - 1) + (p - 1) }; // p >= 1
97
98        let lengths = self.lengths();
99        let deadlines = self.deadlines();
100        let compilers = self.compilers();
101        let setup_times = self.setup_times();
102
103        // Big-M: total processing time + worst-case total setup overhead.
104        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        // 1. Each task assigned to exactly one position: sum_p x_{j,p} = 1 for all j.
129        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        // 2. Each position has exactly one task: sum_j x_{j,p} = 1 for all p.
135        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 each position p >= 1:
141        for p in 1..n {
142            // 3. Switch detection: sw_p >= x_{j,p} + x_{j',p-1} - 1
143            //    whenever k(j) != k(j').
144            //    This forces sw_p = 1 whenever the tasks at p-1 and p differ.
145            for j in 0..n {
146                for j_prev in 0..n {
147                    if compilers[j] != compilers[j_prev] {
148                        // sw_p - x_{j,p} - x_{j',p-1} >= -1
149                        // i.e., x_{j,p} + x_{j',p-1} - sw_p <= 1
150                        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            // 4. Linearisation of a_{j,p} = x_{j,p} * sw_p for each j:
159            //    a_{j,p} <= x_{j,p}
160            //    a_{j,p} <= sw_p
161            //    a_{j,p} >= x_{j,p} + sw_p - 1
162            for j in 0..n {
163                // a_{j,p} <= x_{j,p}
164                constraints.push(LinearConstraint::le(
165                    vec![(a_var(j, p), 1), (x_var(j, p), -1)],
166                    0,
167                ));
168                // a_{j,p} <= sw_p
169                constraints.push(LinearConstraint::le(
170                    vec![(a_var(j, p), 1), (sw_var(p), -1)],
171                    0,
172                ));
173                // a_{j,p} >= x_{j,p} + sw_p - 1
174                // i.e. x_{j,p} + sw_p - a_{j,p} <= 1
175                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        // 5. Deadline constraints: for each (j, p), if x_{j,p}=1, then
183        //    the completion time at position p must be <= d[j].
184        //
185        //    Completion time at position p =
186        //      sum_{p'<=p} sum_{j''} l_{j''} * x_{j'',p'}
187        //      + sum_{p'=1..=p} sum_{j''} s[k(j'')] * a_{j'',p'}
188        //
189        //    Big-M form (only active when x_{j,p}=1):
190        //    M * x_{j,p}
191        //      + sum_{p'<p} sum_{j''} l_{j''} * x_{j'',p'}
192        //      + sum_{p'=1..=p} sum_{j''} s[k(j'')] * a_{j'',p'}
193        //      - M * x_{j,p}   (cancels the activation term)
194        //      <= d[j] - l[j] + M
195        //
196        //    Simplifying (M * x_{j,p} - M * x_{j,p} vanishes):
197        //      sum_{p'<p} sum_{j''} l_{j''} * x_{j'',p'}
198        //      + sum_{p'=1..=p} sum_{j''} s[k(j'')] * a_{j'',p'}
199        //      + M * x_{j,p}
200        //      - M
201        //      <= d[j] - l[j]
202        //
203        //    i.e.:
204        //      M * x_{j,p}
205        //      + sum_{p'<p} sum_{j''} l_{j''} * x_{j'',p'}
206        //      + sum_{p'=1..=p} sum_{j''} s[k(j'')] * a_{j'',p'}
207        //      <= d[j] - l[j] + M
208        for j in 0..n {
209            for p in 0..n {
210                let mut terms: Vec<(usize, i64)> = Vec::new();
211                // Big-M activation term
212                terms.push((x_var(j, p), big_m));
213                // Processing time for positions 0..p (not including p itself)
214                for pp in 0..p {
215                    for (jj, &length) in lengths.iter().enumerate() {
216                        terms.push((x_var(jj, pp), length));
217                    }
218                }
219                // Setup time for positions 1..=p
220                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;