problemreductions/rules/
sequencingwithinintervals_ilp.rs

1//! Reduction from SequencingWithinIntervals to `ILP<bool>`.
2//!
3//! Uses a time-indexed binary formulation:
4//! - Variables: Binary x_{j,k} where x_{j,k} = 1 iff task j starts at offset k
5//!   from its release time (actual start = r_j + k), 0 <= k <= d_j - r_j - l_j.
6//! - Variable index: task j at offset k has global index: Σ_{i<j} slot_count_i + k,
7//!   where slot_count_i = max(0, d_i - r_i - l_i + 1) counts valid start offsets.
8//!   For simplicity we use a flat layout: each task j occupies slot_count[j] variables.
9//! - Constraints:
10//!   1. One-hot: Σ_k x_{j,k} = 1 for each task j (0 = 1 for an empty start domain).
11//!   2. Non-overlap: for each pair (i, j), they cannot be active at the same time.
12//!      Active time of task j starting at r_j+k: [r_j+k, r_j+k+l_j).
13//!      Non-overlap: no shared time. Modeled with: for each pair (i,j) with i<j,
14//!      Σ_{(k1,k2): windows overlap} (x_{i,k1} + x_{j,k2}) ≤ 1.
15//! - Objective: Minimize 0 (feasibility)
16//! - Extraction: For task j, find offset k where x_{j,k}=1; config[j] = k.
17
18use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
19use crate::models::misc::SequencingWithinIntervals;
20use crate::reduction;
21use crate::rules::traits::{ReduceTo, ReductionResult};
22
23/// Result of reducing SequencingWithinIntervals to `ILP<bool>`.
24///
25/// Variable layout: task j occupies variables at offsets [base_j, base_j + slot_count_j).
26/// where base_j = Σ_{i<j} slot_count_i and slot_count_j = max(0, d_j - r_j - l_j + 1).
27#[derive(Debug, Clone)]
28pub struct ReductionSWIToILP {
29    target: ILP<bool>,
30    /// For each task: (base variable index, number of start offsets).
31    task_layout: Vec<(usize, usize)>,
32}
33
34impl ReductionResult for ReductionSWIToILP {
35    type Source = SequencingWithinIntervals;
36    type Target = ILP<bool>;
37
38    fn target_problem(&self) -> &ILP<bool> {
39        &self.target
40    }
41
42    /// Extract schedule from ILP solution.
43    ///
44    /// For each task j, find the offset k where x_{j,k} = 1.
45    /// Returns config[j] = k (start time offset from release time).
46    fn extract_solution(
47        &self,
48        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
49    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
50        crate::rules::traits::validate_target_witness(
51            self.target_problem(),
52            target_solution,
53            |value| value.value.is_some(),
54            "target ILP assignment is infeasible",
55        )?;
56
57        self.task_layout
58            .iter()
59            .enumerate()
60            .map(|(task, &(base, count))| {
61                let mut selected = (0..count).filter(|&offset| target_solution[base + offset] == 1);
62                match (selected.next(), selected.next()) {
63                    (Some(offset), None) => Ok(offset),
64                    (None, _) => Err(crate::rules::ExtractionError::invalid(format!(
65                        "task {task} has no selected start time"
66                    ))),
67                    (Some(_), Some(_)) => Err(crate::rules::ExtractionError::invalid(format!(
68                        "task {task} has multiple selected start times"
69                    ))),
70                }
71            })
72            .collect()
73    }
74}
75
76#[crate::aggregate_reduction(ilp_feasibility)]
77impl crate::rules::AggregateReductionResult for ReductionSWIToILP {}
78
79// S start slots contribute S assignment terms; at most S(S-1)/2
80// unordered slot pairs emit two-term conflict rows, giving at most S^2 terms.
81#[reduction(transform = upper_bound {
82    max_constraint_magnitude_bits = "1",
83    num_vars = "num_start_slots",
84    num_constraints = "num_tasks + num_start_slots * (num_start_slots - 1) / 2",
85    num_nonzeros = "num_start_slots^2",
86})]
87impl ReduceTo<ILP<bool>> for SequencingWithinIntervals {
88    type Result = ReductionSWIToILP;
89
90    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
91        let n = self.num_tasks();
92        let release = self.release_times();
93        let lengths = self.lengths();
94
95        // Compute per-task variable layout: how many start slots each task has
96        let overflow = |operation| {
97            crate::rules::ReductionError::integer_overflow::<Self, ILP<bool>>(operation)
98        };
99        let slot_counts: Vec<usize> = self.start_slot_counts().collect();
100
101        let mut bases = vec![0usize; n];
102        for j in 1..n {
103            bases[j] = bases[j - 1]
104                .checked_add(slot_counts[j - 1])
105                .ok_or_else(|| overflow("computing task variable offsets"))?;
106        }
107        let num_vars = bases
108            .last()
109            .copied()
110            .unwrap_or(0)
111            .checked_add(slot_counts.last().copied().unwrap_or(0))
112            .ok_or_else(|| overflow("computing the ILP variable count"))?;
113
114        let task_layout: Vec<(usize, usize)> = (0..n).map(|j| (bases[j], slot_counts[j])).collect();
115
116        let mut constraints = Vec::new();
117
118        // 1. One-hot per task
119        for j in 0..n {
120            let terms: Vec<(usize, i64)> = (0..slot_counts[j]).map(|k| (bases[j] + k, 1)).collect();
121            constraints.push(LinearConstraint::eq(terms, 1));
122        }
123
124        // 2. Non-overlap for each pair (i, j) with i < j
125        // For each (k1, k2) where task i at offset k1 overlaps task j at offset k2:
126        // x_{i,k1} + x_{j,k2} <= 1
127        for i in 0..n {
128            for j in (i + 1)..n {
129                for k1 in 0..slot_counts[i] {
130                    let offset_i = Self::exact_i64(k1, "converting a task start offset to i64")?;
131                    let start_i = release[i]
132                        .checked_add(offset_i)
133                        .ok_or_else(|| overflow("computing a task start time"))?;
134                    let end_i = start_i
135                        .checked_add(lengths[i])
136                        .ok_or_else(|| overflow("computing a task end time"))?;
137                    for k2 in 0..slot_counts[j] {
138                        let offset_j =
139                            Self::exact_i64(k2, "converting a task start offset to i64")?;
140                        let start_j = release[j]
141                            .checked_add(offset_j)
142                            .ok_or_else(|| overflow("computing a task start time"))?;
143                        let end_j = start_j
144                            .checked_add(lengths[j])
145                            .ok_or_else(|| overflow("computing a task end time"))?;
146                        // Overlap if neither ends before the other starts
147                        if !(end_i <= start_j || end_j <= start_i) {
148                            constraints.push(LinearConstraint::le(
149                                vec![(bases[i] + k1, 1), (bases[j] + k2, 1)],
150                                1,
151                            ));
152                        }
153                    }
154                }
155            }
156        }
157
158        Ok(ReductionSWIToILP {
159            target: ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize)
160                .map_err(Self::target_construction)?,
161            task_layout,
162        })
163    }
164}
165
166#[cfg(feature = "example-db")]
167pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
168    use crate::export::SolutionPair;
169
170    vec![crate::example_db::specs::RuleExampleSpec {
171        id: "sequencingwithinintervals_to_ilp",
172        build: || {
173            // 2 tasks: task 0 [r=0, d=3, l=2], task 1 [r=2, d=5, l=2]
174            // Task 0 can start at offset 0 or 1, task 1 can start at offset 0 or 1
175            // No overlap when both at offset 0: [0,2) and [2,4)
176            let source =
177                SequencingWithinIntervals::new(vec![0, 2], vec![3, 5], vec![2, 2]).unwrap();
178            let reduction: ReductionSWIToILP =
179                ReduceTo::<ILP<bool>>::reduce_to(&source).expect("reduction should succeed");
180            let solver = crate::solvers::ILPSolver::new();
181            let target_config = solver
182                .solve(reduction.target_problem())
183                .expect("canonical example should be feasible");
184            let source_config = reduction.extract_solution(&target_config).unwrap();
185            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
186                source,
187                SolutionPair {
188                    source_config: serde_json::to_value(source_config)
189                        .expect("solution serialization must succeed"),
190                    target_config: serde_json::to_value(target_config)
191                        .expect("solution serialization must succeed"),
192                },
193            )
194        },
195    }]
196}
197
198#[cfg(test)]
199#[path = "../unit_tests/rules/sequencingwithinintervals_ilp.rs"]
200mod tests;
problemreductions/rules/sequencingwithinintervals_ilp.rs

problemreductions/rules/
sequencingwithinintervals_ilp.rs
