diff --git a/Cargo.lock b/Cargo.lock index 09ff64ce..5351d7f0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -277,6 +277,12 @@ dependencies = [ "termcolor", ] +[[package]] +name = "fixedbitset" +version = "0.5.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1d674e81391d1e1ab681a28d99df07927c6d4aa5b027d7da16ba32d1d21ecd99" + [[package]] name = "flatzinc" version = "0.3.21" @@ -544,6 +550,7 @@ dependencies = [ "enum-map", "enumset", "env_logger", + "fixedbitset", "flatzinc", "fnv", "itertools", diff --git a/README.md b/README.md index d6a51801..c5aa7879 100644 --- a/README.md +++ b/README.md @@ -22,6 +22,7 @@ A unique feature of Pumpkin is that it can produce a certificate of unsatisfiabi The solver currently supports integer variables and a number of (global) constraints: - [Cumulative global constraint](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-solver/src/propagators/cumulative). +- [Disjunctive global constraint](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-solver/src/propagators/disjunctive). - [Element global constraint](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-solver/src/propagators/element.rs). - [Arithmetic constraints](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-solver/src/propagators/arithmetic): [linear integer (in)equalities](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-solver/src/propagators/arithmetic/linear_less_or_equal.rs), [integer division](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-solver/src/propagators/arithmetic/division.rs), [integer multiplication](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-solver/src/propagators/arithmetic/integer_multiplication.rs), [maximum](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-solver/src/propagators/arithmetic/maximum.rs), [absolute value](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-solver/src/propagators/arithmetic/absolute_value.rs). - Clausal constraints. diff --git a/minizinc/lib/fzn_disjunctive_strict.mzn b/minizinc/lib/fzn_disjunctive_strict.mzn new file mode 100644 index 00000000..1822ddd4 --- /dev/null +++ b/minizinc/lib/fzn_disjunctive_strict.mzn @@ -0,0 +1,25 @@ +% Taken from https://github.com/chuffed/chuffed/blob/develop/chuffed/flatzinc/mznlib/fzn_disjunctive_strict.mzn +%------------------------------------------------------------------------------% +% Requires that a set of tasks given by start times s and durations d +% do not overlap in time. Tasks with duration 0 CANNOT be scheduled at any time, +% but only when no other task is running. +% +% Assumptions: +% - forall i, d[i] >= 0 +%------------------------------------------------------------------------------% + +predicate fzn_disjunctive_strict(array[int] of var int: s, + array[int] of var int: d) = + forall(i in index_set(d))(d[i] >= 0) + /\ if is_fixed(d) then + pumpkin_disjunctive_strict(s, fix(d)) + else + forall(i, j in index_set(d) where i < j) ( + s[i] + d[i] <= s[j] \/ s[j] + d[j] <= s[i] + ) + endif + ; + + % Global disjunctive propagator + % +predicate pumpkin_disjunctive_strict(array[int] of var int: s, array[int] of int: d); diff --git a/pumpkin-solver/Cargo.toml b/pumpkin-solver/Cargo.toml index cae2025c..3e28f090 100644 --- a/pumpkin-solver/Cargo.toml +++ b/pumpkin-solver/Cargo.toml @@ -26,6 +26,7 @@ clap = { version = "4.5.17", features = ["derive"] } env_logger = "0.10.0" bitfield-struct = "0.9.2" num = "0.4.3" +fixedbitset = "0.5.7" enum-map = "2.7.3" [dev-dependencies] diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs index e8a8c8b2..d53f4772 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs @@ -201,6 +201,7 @@ pub(crate) fn run( "pumpkin_cumulative" => compile_cumulative(context, exprs, &options)?, "pumpkin_cumulative_var" => todo!("The `cumulative` constraint with variable duration/resource consumption/bound is not implemented yet!"), + "pumpkin_disjunctive_strict" => compile_disjunctive_strict(context, exprs)?, unknown => todo!("unsupported constraint {unknown}"), }; @@ -247,6 +248,21 @@ fn compile_cumulative( Ok(post_result.is_ok()) } +fn compile_disjunctive_strict( + context: &mut CompilationContext<'_>, + exprs: &[flatzinc::Expr], +) -> Result { + check_parameters!(exprs, 2, "pumpkin_disjunctive_strict"); + + let start_times = context.resolve_integer_variable_array(&exprs[0])?; + let durations = context.resolve_array_integer_constants(&exprs[1])?; + + let post_result = + constraints::disjunctive(start_times.iter().copied(), durations.iter().copied()) + .post(context.solver, None); + Ok(post_result.is_ok()) +} + fn compile_array_int_maximum( context: &mut CompilationContext<'_>, exprs: &[flatzinc::Expr], diff --git a/pumpkin-solver/src/constraints/disjunctive.rs b/pumpkin-solver/src/constraints/disjunctive.rs new file mode 100644 index 00000000..404e1f85 --- /dev/null +++ b/pumpkin-solver/src/constraints/disjunctive.rs @@ -0,0 +1,40 @@ +use std::fmt::Debug; + +use super::Constraint; +use crate::propagators::disjunctive_propagator::Disjunctive; +use crate::propagators::disjunctive_task::ArgDisjunctiveTask; +use crate::variables::IntegerVariable; + +/// Creates the [Disjunctive](https://sofdem.github.io/gccat/gccat/Cdisjunctive.html) [`Constraint`]. +/// +/// This constraint ensures that at no point in time the provided task can overlap. This can be +/// seen as a special case of the `cumulative` constraint with capacity 1. +/// +/// The implementation uses the edge-finding as described in \[1\]. +/// +/// The length of `start_times` and `durations` should be the same; if +/// this is not the case then this method will panic. +/// +/// # Bibliography +/// \[1\] P. Vilím, ‘Global constraints in scheduling’, 2007. +pub fn disjunctive( + start_times: StartTimes, + durations: Durations, +) -> impl Constraint +where + StartTimes: IntoIterator, + StartTimes::Item: IntegerVariable + Debug + 'static, + StartTimes::IntoIter: ExactSizeIterator, + Durations: IntoIterator, + Durations::IntoIter: ExactSizeIterator, +{ + Disjunctive::new( + start_times + .into_iter() + .zip(durations) + .map(|(start_time, duration)| ArgDisjunctiveTask { + start_variable: start_time, + processing_time: duration, + }), + ) +} diff --git a/pumpkin-solver/src/constraints/mod.rs b/pumpkin-solver/src/constraints/mod.rs index 98100b32..6026f9b2 100644 --- a/pumpkin-solver/src/constraints/mod.rs +++ b/pumpkin-solver/src/constraints/mod.rs @@ -28,6 +28,7 @@ mod boolean; mod clause; mod constraint_poster; mod cumulative; +mod disjunctive; mod element; use std::num::NonZero; @@ -38,6 +39,7 @@ pub use boolean::*; pub use clause::*; pub use constraint_poster::*; pub use cumulative::*; +pub use disjunctive::*; pub use element::*; use crate::engine::propagation::Propagator; diff --git a/pumpkin-solver/src/engine/cp/propagation/local_id.rs b/pumpkin-solver/src/engine/cp/propagation/local_id.rs index fe644e76..94f80589 100644 --- a/pumpkin-solver/src/engine/cp/propagation/local_id.rs +++ b/pumpkin-solver/src/engine/cp/propagation/local_id.rs @@ -1,3 +1,5 @@ +use crate::containers::StorageKey; + /// A local id uniquely identifies a variable within a specific propagator. A local id can be /// thought of as the index of the variable in the propagator. #[derive(Clone, Copy, Debug, Hash, PartialEq, Eq, PartialOrd, Ord)] @@ -13,6 +15,16 @@ impl LocalId { } } +impl StorageKey for LocalId { + fn index(&self) -> usize { + self.0 as usize + } + + fn create_from_index(index: usize) -> Self { + Self::from(index as u32) + } +} + impl std::fmt::Display for LocalId { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!(f, "{}", self.0) diff --git a/pumpkin-solver/src/propagators/cumulative/time_table/time_table_over_interval.rs b/pumpkin-solver/src/propagators/cumulative/time_table/time_table_over_interval.rs index f43baa55..b94fd7bf 100644 --- a/pumpkin-solver/src/propagators/cumulative/time_table/time_table_over_interval.rs +++ b/pumpkin-solver/src/propagators/cumulative/time_table/time_table_over_interval.rs @@ -54,7 +54,6 @@ pub(crate) struct Event { /// \[1\] A. Schutt, Improving scheduling by learning. University of Melbourne, Department of /// Computer Science and Software Engineering, 2011. #[derive(Debug)] - pub(crate) struct TimeTableOverIntervalPropagator { /// Stores whether the time-table is empty is_time_table_empty: bool, diff --git a/pumpkin-solver/src/propagators/disjunctive/disjunctive_propagator.rs b/pumpkin-solver/src/propagators/disjunctive/disjunctive_propagator.rs new file mode 100644 index 00000000..2c4267fc --- /dev/null +++ b/pumpkin-solver/src/propagators/disjunctive/disjunctive_propagator.rs @@ -0,0 +1,439 @@ +use std::cmp::Reverse; + +use fixedbitset::FixedBitSet; + +use super::disjunctive_task::ArgDisjunctiveTask; +use super::disjunctive_task::DisjunctiveTask; +use super::theta_lambda_tree::ThetaLambdaTree; +use crate::basic_types::Inconsistency; +use crate::basic_types::PropagationStatusCP; +use crate::containers::StorageKey; +use crate::engine::cp::propagation::ReadDomains; +use crate::engine::propagation::LocalId; +use crate::engine::propagation::PropagationContextMut; +use crate::engine::propagation::Propagator; +use crate::engine::propagation::PropagatorInitialisationContext; +use crate::engine::DomainEvents; +use crate::predicate; +use crate::predicates::PropositionalConjunction; +use crate::pumpkin_assert_moderate; +use crate::pumpkin_assert_simple; +use crate::variables::IntegerVariable; +use crate::variables::TransformableVariable; + +/// [`Propagator`] responsible for using disjunctive reasoning to propagate the [Disjunctive](https://sofdem.github.io/gccat/gccat/Cdisjunctive.html) constraint. +/// +/// Currently, this propagator only implements edge-finding as specified in \[1\]. The reasoning of +/// this approach is based on finding a task i and a subset of tasks for which it holds that if we +/// were to schedule i at its earliest start time then it would overflow the resource capacity and +/// thus i should be scheduled after all activities from this set. +/// +/// # Bibliography +/// \[1\] P. Vilím, ‘Filtering algorithms for the unary resource constraint’, Archives of Control +/// Sciences, vol. 18, no. 2, pp. 159–202, 2008. +pub(crate) struct Disjunctive { + /// The tasks which serve as the input to the disjunctive constraint + tasks: Box<[DisjunctiveTask]>, + /// An additional list of tasks which allows us to sort them (we require [`Disjunctive::tasks`] + /// to keep track of the right indices). + sorted_tasks: Vec>, + /// The tasks which are used to propagate the upper-bounds; these are the same as + /// [`Disjunctive::tasks`] but reversed (i.e. instead of being from [EST, LCT] these tasks go + /// from [-LCT, -EST]) + reverse_tasks: Box< + [DisjunctiveTask<<::AffineView as IntegerVariable>::AffineView>], + >, + /// An additional list of tasks which allows us to sort them (we require + /// [`Disjunctive::reverse_tasks`] + /// to keep track of the right indices). + sorted_reverse_tasks: + Vec::AffineView as IntegerVariable>::AffineView>>, + + /// The elements which are currently present in the set Theta used for edge-finding. + elements_in_theta: FixedBitSet, +} + +impl Disjunctive { + pub(crate) fn new(tasks: impl IntoIterator>) -> Self { + let tasks = tasks + .into_iter() + .enumerate() + .map(|(index, task)| DisjunctiveTask { + start_variable: task.start_variable.clone(), + processing_time: task.processing_time, + id: LocalId::from(index as u32), + }) + .collect::>(); + let reverse_tasks = tasks + .iter() + .map(|task| DisjunctiveTask { + start_variable: task.start_variable.offset(task.processing_time).scaled(-1), + processing_time: task.processing_time, + id: task.id, + }) + .collect::>(); + + let num_tasks = tasks.len(); + + Self { + tasks: tasks.clone().into_boxed_slice(), + sorted_tasks: tasks, + reverse_tasks: reverse_tasks.clone().into_boxed_slice(), + sorted_reverse_tasks: reverse_tasks, + elements_in_theta: FixedBitSet::with_capacity(num_tasks), + } + } +} + +/// Creates an explanation consisting of the tasks in the theta-lambda tree which were responsible +/// for the conflict based on \[1\]. +/// +/// # Bibliography +/// \[1\] P. Vilím, ‘Computing explanations for the unary resource constraint’, in International +/// Conference on Integration of Artificial Intelligence (AI) and Operations Research (OR) +/// Techniques in Constraint Programming, 2005, pp. 396–409. +fn create_conflict_explanation<'a, Var: IntegerVariable>( + tasks: &'a [DisjunctiveTask], + theta_lambda_tree: &mut ThetaLambdaTree, + context: &'a PropagationContextMut, +) -> PropositionalConjunction { + // First we calculate some data about the set of tasks that caused the overflow + let mut est_theta = i32::MAX; + let mut lct_theta = i32::MIN; + let mut p_theta = 0; + + let reponsible_tasks = theta_lambda_tree + .all_responsible_ect() + .inspect(|element| { + let task = &tasks[element.index()]; + est_theta = est_theta.min(context.lower_bound(&task.start_variable)); + lct_theta = + lct_theta.max(context.upper_bound(&task.start_variable) + task.processing_time); + p_theta += task.processing_time; + }) + .collect::>(); + + // We check whether we indeed overflow the interval + pumpkin_assert_simple!(p_theta > lct_theta - est_theta); + + // Then we calculate the amount by which we can lift the interval; i.e. how much does the + // processing time of theta overflow the interval + let delta = p_theta - (lct_theta - est_theta) - 1; + + let mut explanation = Vec::new(); + + // Then for each element in the responsible tasks, we add that they need to be in this interval + // together + for element in reponsible_tasks.iter() { + let task = &tasks[element.index()]; + + pumpkin_assert_moderate!(context + .is_predicate_satisfied(predicate!(task.start_variable >= est_theta - delta / 2))); + pumpkin_assert_moderate!(context.is_predicate_satisfied(predicate!( + task.start_variable + <= lct_theta + (delta as f64 / 2.0).ceil() as i32 - task.processing_time + )),); + + explanation.push(predicate!(task.start_variable >= est_theta - delta / 2)); + explanation.push(predicate!( + task.start_variable + <= lct_theta + (delta as f64 / 2.0).ceil() as i32 - task.processing_time + )) + } + + explanation.into() +} + +/// Creates an explanation consisting of the tasks in the theta-lambda tree which were responsible +/// for the propagation of `propagated_task` based on \[1\]. +/// +/// # Bibliography +/// \[1\] P. Vilím, ‘Computing explanations for the unary resource constraint’, in International +/// Conference on Integration of Artificial Intelligence (AI) and Operations Research (OR) +/// Techniques in Constraint Programming, 2005, pp. 396–409. +fn create_propagation_explanation<'a, Var: IntegerVariable>( + tasks: &'a [DisjunctiveTask], + propagated_task_id: LocalId, + new_bound: i32, + theta_lambda_tree: &mut ThetaLambdaTree, + context: &'a PropagationContextMut, +) -> PropositionalConjunction { + let propagated_task = &tasks[propagated_task_id.index()]; + + // First we calculate the required information for the explanations of all tasks in theta + let mut earliest_release_time = context.lower_bound(&propagated_task.start_variable); + let mut p_theta = 0; + + // First we get the tasks which caused the relation to be detected + let theta = theta_lambda_tree + .all_responsible_ect_bar() + .filter(|index| *index != propagated_task_id) + .inspect(|theta_element| { + let task = &tasks[theta_element.index()]; + p_theta += task.processing_time; + earliest_release_time = + earliest_release_time.min(context.lower_bound(&task.start_variable)); + }) + .collect::>(); + pumpkin_assert_simple!(!theta.is_empty()); + + // Then we look at the tasks which propagated the bound + let mut p_theta_prime = 0; + let theta_prime = theta_lambda_tree + .all_responsible_ect() + .inspect(|theta_prime_element| { + let task = &tasks[theta_prime_element.index()]; + p_theta_prime += task.processing_time; + }) + .collect::>(); + + pumpkin_assert_simple!(!theta.is_empty()); + + let mut explanation = Vec::new(); + + // Now we go over each element in theta prime and explain it using lifted intervals + for j in theta_prime.iter() { + let task = &tasks[j.index()]; + + pumpkin_assert_moderate!(context + .is_predicate_satisfied(predicate!(task.start_variable >= new_bound - p_theta_prime)),); + pumpkin_assert_moderate!(context.is_predicate_satisfied(predicate!( + task.start_variable + <= earliest_release_time + p_theta + propagated_task.processing_time + - task.processing_time + - 1 + )),); + + explanation.push(predicate!(task.start_variable >= new_bound - p_theta_prime)); + explanation.push(predicate!( + task.start_variable + <= earliest_release_time + p_theta + propagated_task.processing_time + - 1 + - task.processing_time + )); + } + + // Then we go over element in theta and explain it using lifted intervals + for j in theta.iter() { + // We skip it if it was already explained in theta prime + if theta_prime.contains(j) { + continue; + } + let task = &tasks[j.index()]; + + pumpkin_assert_moderate!(context + .is_predicate_satisfied(predicate!(task.start_variable >= earliest_release_time)),); + pumpkin_assert_moderate!(context.is_predicate_satisfied(predicate!( + task.start_variable + <= earliest_release_time + p_theta + propagated_task.processing_time + - task.processing_time + - 1 + )),); + + explanation.push(predicate!(task.start_variable >= earliest_release_time)); + explanation.push(predicate!( + task.start_variable + <= earliest_release_time + p_theta + propagated_task.processing_time + - 1 + - task.processing_time + )); + } + + // Finally, we add the bound on the propagated task since this is required to entail the + // propagation + explanation.push(predicate!( + propagated_task.start_variable >= earliest_release_time + )); + + explanation.into() +} + +/// Performs the edge-finding algorithm (see [`Disjunctive`] for an intuition and the work on which +/// this implementation is based). +fn edge_finding( + context: &mut PropagationContextMut, + tasks: &[DisjunctiveTask], + sorted_tasks: &mut [DisjunctiveTask], + elements_in_theta: &mut FixedBitSet, +) -> PropagationStatusCP { + // First we create our Theta-Lambda tree and add all of the tasks to Theta (Lambda is empty at + // this point) + let mut theta_lambda_tree = ThetaLambdaTree::new(tasks, context.as_readonly()); + for task in tasks.iter() { + elements_in_theta.insert(task.id.index()); + theta_lambda_tree.add_to_theta(task, context.as_readonly()); + } + + // Then sort in non-increasing order of latest completion time (LCT) + sorted_tasks.sort_by_key(|task| { + Reverse(context.upper_bound(&task.start_variable) + task.processing_time) + }); + + // Then we get the first element from the lambda tree with the highest value of LCT + let mut index = 0; + let mut j = &sorted_tasks[index]; + let mut lct_j = context.upper_bound(&j.start_variable) + j.processing_time; + + // While we have elements in theta, we keep iterating the algorithm + while index < tasks.len() - 1 { + // We know that `j` represents the element in Theta with the highest LCT, if the ECT + // (which takes into account `j`) is larger than the LCT of `j` then we can report an + // overflow + if theta_lambda_tree.ect() > lct_j { + return Err(Inconsistency::Conflict(create_conflict_explanation( + tasks, + &mut theta_lambda_tree, + context, + ))); + } + + // If there was no overflow then we continue by checking whether we can find a propagation + // from the tasks + + // To do this, we first remove the task from Theta + theta_lambda_tree.remove_from_theta(j); + elements_in_theta.remove(j.id.index()); + // And then add it to Lambda (i.e. we are checking whether we can find a task i in Lambda + // such that the element in Theta would cause an overflow) + theta_lambda_tree.add_to_lambda(j, context.as_readonly()); + + // Then we go to the next task which represents the latest completion time of the set Theta + index += 1; + j = &sorted_tasks[index]; + lct_j = context.upper_bound(&j.start_variable) + j.processing_time; + + // Then we try to find tasks in Lambda such that the edge-finding condition holds + // + // i.e. Find an element such that `ECT_{i union Theta} > lct_j` + while theta_lambda_tree.ect_bar() > lct_j { + // We know that the condition holds and now we need to retrieve the element in Lambda + // which was responsible for the condition holding + if let Some(i) = theta_lambda_tree.responsible_ect_bar() { + // We calculate the new bound + let new_bound = theta_lambda_tree.ect(); + + // Then we check whether we can update; if this is the case then we set the new + // lower-bound to be after `ECT_{Theta}` + if new_bound > context.lower_bound(&tasks[i.index()].start_variable) { + // Propagate + context.set_lower_bound( + &tasks[i.index()].start_variable, + new_bound, + create_propagation_explanation( + tasks, + i, + new_bound, + &mut theta_lambda_tree, + context, + ), + )?; + } + + // Then we remove the element from consideration entirely by removing it from Lambda + // and continue to see if there are other elements from Lambda which could be + // updated + theta_lambda_tree.remove_from_lambda(&tasks[i.index()]); + } else { + break; + } + } + } + + Ok(()) +} + +impl Propagator for Disjunctive { + fn name(&self) -> &str { + "Disjunctive" + } + + fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { + // First we perform a "regular" round of edge-finding updating the lower-bounds + edge_finding( + &mut context, + &self.tasks, + &mut self.sorted_tasks, + &mut self.elements_in_theta, + )?; + + // Now we want to also update the upper-bounds + // + // We do this by "reversing" the tasks to make the LCT be represented as the EST of a task + edge_finding( + &mut context, + &self.reverse_tasks, + &mut self.sorted_reverse_tasks, + &mut self.elements_in_theta, + ) + } + + fn debug_propagate_from_scratch( + &self, + mut context: PropagationContextMut, + ) -> PropagationStatusCP { + let mut sorted_tasks = self.sorted_tasks.clone(); + let mut elements_in_theta = self.elements_in_theta.clone(); + edge_finding( + &mut context, + &self.tasks, + &mut sorted_tasks, + &mut elements_in_theta, + )?; + + let mut sorted_reverse_tasks = self.sorted_reverse_tasks.clone(); + edge_finding( + &mut context, + &self.reverse_tasks, + &mut sorted_reverse_tasks, + &mut elements_in_theta, + ) + } + + fn initialise_at_root( + &mut self, + context: &mut PropagatorInitialisationContext, + ) -> Result<(), PropositionalConjunction> { + self.tasks.iter().for_each(|task| { + let _ = context.register(task.start_variable.clone(), DomainEvents::BOUNDS, task.id); + }); + Ok(()) + } +} + +#[cfg(test)] +mod tests { + use crate::engine::test_solver::TestSolver; + use crate::propagators::disjunctive::disjunctive_propagator::Disjunctive; + use crate::propagators::disjunctive_task::ArgDisjunctiveTask; + + #[test] + fn propagator_propagates_lower_bound() { + let mut solver = TestSolver::default(); + let c = solver.new_variable(4, 26); + let d = solver.new_variable(13, 13); + let e = solver.new_variable(5, 10); + let f = solver.new_variable(5, 10); + + let _ = solver + .new_propagator(Disjunctive::new([ + ArgDisjunctiveTask { + start_variable: c, + processing_time: 4, + }, + ArgDisjunctiveTask { + start_variable: d, + processing_time: 5, + }, + ArgDisjunctiveTask { + start_variable: e, + processing_time: 3, + }, + ArgDisjunctiveTask { + start_variable: f, + processing_time: 3, + }, + ])) + .expect("No conflict"); + assert_eq!(solver.lower_bound(c), 18); + } +} diff --git a/pumpkin-solver/src/propagators/disjunctive/disjunctive_task.rs b/pumpkin-solver/src/propagators/disjunctive/disjunctive_task.rs new file mode 100644 index 00000000..a4dac8e3 --- /dev/null +++ b/pumpkin-solver/src/propagators/disjunctive/disjunctive_task.rs @@ -0,0 +1,24 @@ +use std::fmt::Debug; + +use crate::engine::propagation::LocalId; + +pub(crate) struct ArgDisjunctiveTask { + pub(crate) start_variable: Var, + pub(crate) processing_time: i32, +} + +#[derive(Clone)] +pub(super) struct DisjunctiveTask { + pub(crate) start_variable: Var, + pub(crate) processing_time: i32, + pub(crate) id: LocalId, +} + +impl Debug for DisjunctiveTask { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("DisjunctiveTask") + .field("d", &self.processing_time) + .field("id", &self.id) + .finish() + } +} diff --git a/pumpkin-solver/src/propagators/disjunctive/mod.rs b/pumpkin-solver/src/propagators/disjunctive/mod.rs new file mode 100644 index 00000000..40504e86 --- /dev/null +++ b/pumpkin-solver/src/propagators/disjunctive/mod.rs @@ -0,0 +1,4 @@ +pub(crate) mod disjunctive_propagator; +pub(crate) mod disjunctive_task; +mod theta_lambda_tree; +mod theta_tree; diff --git a/pumpkin-solver/src/propagators/disjunctive/theta_lambda_tree.rs b/pumpkin-solver/src/propagators/disjunctive/theta_lambda_tree.rs new file mode 100644 index 00000000..7a84fc93 --- /dev/null +++ b/pumpkin-solver/src/propagators/disjunctive/theta_lambda_tree.rs @@ -0,0 +1,572 @@ +use std::cmp::max; + +use super::disjunctive_task::DisjunctiveTask; +use crate::containers::KeyedVec; +use crate::containers::StorageKey; +use crate::engine::propagation::LocalId; +use crate::engine::propagation::PropagationContext; +use crate::engine::propagation::ReadDomains; +use crate::pumpkin_assert_simple; +use crate::variables::IntegerVariable; + +// A node in the [`ThetaTree`] which keeps track of the ECT and sum of processing times of its +// children +// +// As opposed to the nodes in a Theta tree, the nodes in a ThetaLambdaTree also keep track of the +// ECT and sum of processing times if a single element from the Lambda set can be added +#[derive(Debug, Clone, PartialEq, Eq)] +pub(super) struct Node { + ect: i32, + sum_of_processing_times: i32, + ect_bar: i32, + sum_of_processing_times_bar: i32, +} + +impl Node { + // Constructs an empty node + fn empty() -> Self { + Self { + ect: i32::MIN, + sum_of_processing_times: 0, + ect_bar: i32::MIN, + sum_of_processing_times_bar: 0, + } + } + + // Construct a new white node with the provided value + fn new_white_node(ect: i32, sum_of_processing_times: i32) -> Self { + Self { + ect, + sum_of_processing_times, + ect_bar: ect, + sum_of_processing_times_bar: sum_of_processing_times, + } + } + + // Construct a new gray node with the provided value + fn new_gray_node(ect: i32, sum_of_processing_times: i32) -> Self { + Self { + ect: i32::MIN, + sum_of_processing_times: 0, + ect_bar: ect, + sum_of_processing_times_bar: sum_of_processing_times, + } + } +} + +/// A structure for efficiently calculating the ECT of a set of tasks while only allowing one +/// element from another (non-overlapping) set. +/// +/// The implementation is based on \[1\]. The idea is to have a complete binary tree where the leaf +/// nodes represent the tasks. These leaf nodes are sorted by EST and this allows the values of the +/// inner nodes to be calculated using a recursive formula. +/// +/// # Bibliography +/// \[1\] P. Vilím, ‘Filtering algorithms for the unary resource constraint’, Archives of Control +/// Sciences, vol. 18, no. 2, pp. 159–202, 2008. +#[derive(Debug)] +pub(super) struct ThetaLambdaTree { + pub(super) nodes: Vec, + /// Then we keep track of a mapping from the [`LocalId`] to its position in the tree since the + /// methods take as input tasks with [`LocalId`]s. + mapping: KeyedVec, + /// Then we keep track of a mapping from the position in the tree to its corresponding + /// [`LocalId`] since [`ThetaLambdaTree`] requires us to return the responsible [`LocalId`]. + reverse_mapping: KeyedVec, + /// The number of internal nodes in the tree; used to calculate the leaf node index based on + /// the index in the tree + number_of_internal_nodes: usize, + + /// Used to calculate the reason for the ECT + indices: Vec, +} + +impl ThetaLambdaTree { + pub(super) fn new( + tasks: &[DisjunctiveTask], + context: PropagationContext, + ) -> Self { + // First we sort the tasks by lower-bound + let mut sorted_tasks = tasks.to_vec(); + sorted_tasks.sort_by_key(|task| context.lower_bound(&task.start_variable)); + + // Then we keep track of a mapping from the [`LocalId`] to its position in the tree and a + // reverse mapping + let mut mapping = KeyedVec::default(); + let mut reverse_mapping = KeyedVec::default(); + for (index, task) in sorted_tasks.iter().enumerate() { + while mapping.len() <= task.id.index() { + let _ = mapping.push(usize::MAX); + } + mapping[task.id] = index; + let _ = reverse_mapping.push(task.id); + } + + // Calculate the number of internal nodes which are required to create the binary tree + let mut number_of_internal_nodes = 1; + while number_of_internal_nodes < tasks.len() { + number_of_internal_nodes <<= 1; + } + + let nodes = vec![Node::empty(); 2 * number_of_internal_nodes - 1]; + + ThetaLambdaTree { + nodes, + mapping, + reverse_mapping, + number_of_internal_nodes: number_of_internal_nodes - 1, + indices: Default::default(), + } + } + + /// Returns the ECT of Theta + pub(super) fn ect(&self) -> i32 { + pumpkin_assert_simple!(!self.nodes.is_empty()); + self.nodes[0].ect + } + + /// Returns the ECT of Theta while allowing 1 element of Lambda to be added + pub(super) fn ect_bar(&self) -> i32 { + self.nodes[0].ect_bar + } + + /// Returns the index in the tree of the `index`th node + fn get_leaf_node_index(&self, index: usize) -> usize { + pumpkin_assert_simple!( + index >= self.number_of_internal_nodes, + "Provided index was not a leaf node" + ); + index - self.number_of_internal_nodes + } + + /// Returns all [`LocalId`]s of the tasks responsible for the value of `ect` + pub(super) fn all_responsible_ect(&mut self) -> impl Iterator + '_ { + self.indices.clear(); + self.responsible_index_ect_internal(0); + self.indices + .iter() + .copied() + .map(|index| self.reverse_mapping[self.get_leaf_node_index(index)]) + } + + /// Returns all [`LocalId`]s of the tasks responsible for the value of `ect_bar` + pub(super) fn all_responsible_ect_bar(&mut self) -> impl Iterator + '_ { + self.indices.clear(); + self.all_responsible_index_ect_bar_internal(0); + self.indices + .iter() + .copied() + .map(|index| self.reverse_mapping[self.get_leaf_node_index(index)]) + } + + fn all_responsible_index_ect_bar_internal(&mut self, position: usize) { + if self.is_leaf(position) { + // Assuming that all tasks have non-zero processing time + if self.nodes[position] != Node::empty() + && self.nodes[position].sum_of_processing_times > 0 + { + // If we have reached a leaf then we add it + self.indices.push(position) + } + } else { + let left_child = Self::get_left_child_index(position); + let right_child = Self::get_right_child_index(position); + + if self.nodes[right_child] != Node::empty() + && self.nodes[position].ect_bar == self.nodes[right_child].ect_bar + { + self.all_responsible_index_ect_bar_internal(right_child) + } else if self.nodes[right_child] != Node::empty() + && self.nodes[position].ect_bar + == self.nodes[left_child].ect + + self.nodes[right_child].sum_of_processing_times_bar + { + self.responsible_index_ect_internal(left_child); + self.all_responsible_index_p_internal(right_child) + } else if self.nodes[left_child] != Node::empty() + && self.nodes[position].ect_bar + == self.nodes[left_child].ect_bar + + self.nodes[right_child].sum_of_processing_times + { + self.all_responsible_index_ect_bar_internal(left_child); + self.get_all_leaf_nodes_rooted_at_index(right_child); + } + } + } + + fn all_responsible_index_p_internal(&mut self, position: usize) { + if self.is_leaf(position) { + // Assuming that all tasks have non-zero processing time + if self.nodes[position] != Node::empty() + && self.nodes[position].sum_of_processing_times > 0 + { + // If we have reached a leaf then we add it + self.indices.push(position) + } + } else { + let left_child = Self::get_left_child_index(position); + let right_child = Self::get_right_child_index(position); + + if self.nodes[left_child] != Node::empty() + && self.nodes[position].sum_of_processing_times_bar + == self.nodes[left_child].sum_of_processing_times_bar + + self.nodes[right_child].sum_of_processing_times + { + self.all_responsible_index_p_internal(left_child) + } else if self.nodes[right_child] != Node::empty() + && self.nodes[position].sum_of_processing_times_bar + == self.nodes[left_child].sum_of_processing_times + + self.nodes[right_child].sum_of_processing_times_bar + { + self.all_responsible_index_p_internal(right_child) + } + } + } + + fn responsible_index_ect_internal(&mut self, position: usize) { + if self.is_leaf(position) { + if self.nodes[position] != Node::empty() + && self.nodes[position].sum_of_processing_times > 0 + { + // If we have reached a leaf then we add it + self.indices.push(position) + } + } else { + let left_child = Self::get_left_child_index(position); + let right_child = Self::get_right_child_index(position); + + // We know that the ECT in the current node is fully due to the right child + if self.nodes[right_child] != Node::empty() + && self.nodes[position].ect == self.nodes[right_child].ect + { + self.responsible_index_ect_internal(right_child) + } else { + // Otherwise, it is due to a combination of the left child and the right child + pumpkin_assert_simple!( + self.nodes[left_child] != Node::empty() + && self.nodes[position].ect + == self.nodes[left_child].ect + + self.nodes[right_child].sum_of_processing_times + ); + // We get the leaves reponsible for the left child + self.responsible_index_ect_internal(left_child); + + if self.nodes[right_child].sum_of_processing_times != 0 { + // And the leaves of the right side + self.get_all_leaf_nodes_rooted_at_index(right_child); + } + } + } + } + + fn get_all_leaf_nodes_rooted_at_index(&mut self, position: usize) { + if self.is_leaf(position) { + if self.nodes[position] != Node::empty() + && self.nodes[position].sum_of_processing_times > 0 + { + self.indices.push(position); + } + } else { + let left_child = Self::get_left_child_index(position); + let right_child = Self::get_right_child_index(position); + + if self.nodes[left_child] != Node::empty() && self.nodes[right_child] != Node::empty() { + self.get_all_leaf_nodes_rooted_at_index(left_child); + self.get_all_leaf_nodes_rooted_at_index(right_child); + } else if self.nodes[left_child] != Node::empty() { + self.get_all_leaf_nodes_rooted_at_index(left_child) + } else if self.nodes[right_child] != Node::empty() { + self.get_all_leaf_nodes_rooted_at_index(right_child) + } + } + } + + /// Returns the [`LocalId`] for the task corresponding with the task in Lambda which was + /// responsible for the value of `ect_bar` + /// + /// This can be [`None`] if an overflow occurs and there are no elements in lambda + pub(super) fn responsible_ect_bar(&self) -> Option { + self.responsible_index_ect_bar_internal(0) + .map(|index| self.reverse_mapping[self.get_leaf_node_index(index)]) + } + + fn responsible_index_ect_bar_internal(&self, position: usize) -> Option { + // See \[1\] for the implementation + if self.is_leaf(position) { + // Assuming that all tasks have non-zero processing time + (self.nodes[position].sum_of_processing_times_bar > 0 + && self.nodes[position].sum_of_processing_times == 0) + .then_some(position) + } else { + let left_child = Self::get_left_child_index(position); + let right_child = Self::get_right_child_index(position); + + if self.nodes[right_child] != Node::empty() + && self.nodes[position].ect_bar == self.nodes[right_child].ect_bar + { + self.responsible_index_ect_bar_internal(right_child) + } else if self.nodes[right_child] != Node::empty() + && self.nodes[position].ect_bar + == self.nodes[left_child].ect + + self.nodes[right_child].sum_of_processing_times_bar + { + self.responsible_index_p_internal(right_child) + } else if self.nodes[left_child] != Node::empty() + && self.nodes[position].ect_bar + == self.nodes[left_child].ect_bar + + self.nodes[right_child].sum_of_processing_times + { + self.responsible_index_ect_bar_internal(left_child) + } else { + None + } + } + } + + fn responsible_index_p_internal(&self, position: usize) -> Option { + if self.is_leaf(position) { + // Assuming that all tasks have non-zero processing time + (self.nodes[position].sum_of_processing_times_bar > 0 + && self.nodes[position].sum_of_processing_times == 0) + .then_some(position) + } else { + let left_child = Self::get_left_child_index(position); + let right_child = Self::get_right_child_index(position); + + if self.nodes[left_child] != Node::empty() + && self.nodes[position].sum_of_processing_times_bar + == self.nodes[left_child].sum_of_processing_times_bar + + self.nodes[right_child].sum_of_processing_times + { + self.responsible_index_p_internal(left_child) + } else if self.nodes[right_child] != Node::empty() + && self.nodes[position].sum_of_processing_times_bar + == self.nodes[left_child].sum_of_processing_times + + self.nodes[right_child].sum_of_processing_times_bar + { + self.responsible_index_p_internal(right_child) + } else { + None + } + } + } + + /// Add the provided task to Lambda + pub(super) fn add_to_lambda( + &mut self, + task: &DisjunctiveTask, + context: PropagationContext, + ) { + // We need to find the leaf node index; note that there are |nodes| / 2 leaves + let position = self.nodes.len() / 2 + self.mapping[task.id]; + let ect = context.lower_bound(&task.start_variable) + task.processing_time; + + self.nodes[position] = Node::new_gray_node(ect, task.processing_time); + self.upheap(position); + } + + /// Remove the provided task from Lambda (this method assumes that the element is already not a + /// part of Theta at this point) + pub(super) fn remove_from_lambda(&mut self, task: &DisjunctiveTask) { + // We need to find the leaf node index; note that there are |nodes| / 2 leaves + let position = self.nodes.len() / 2 + self.mapping[task.id]; + pumpkin_assert_simple!(self.nodes[position].sum_of_processing_times == 0); + self.nodes[position] = Node::empty(); + self.upheap(position) + } + + /// Add the provided task to Theta + pub(super) fn add_to_theta( + &mut self, + task: &DisjunctiveTask, + context: PropagationContext, + ) { + // We need to find the leaf node index; note that there are |nodes| / 2 leaves + let position = self.nodes.len() / 2 + self.mapping[task.id]; + let ect = context.lower_bound(&task.start_variable) + task.processing_time; + + self.nodes[position] = Node::new_white_node(ect, task.processing_time); + self.upheap(position) + } + + /// Remove the provided task from Theta + pub(super) fn remove_from_theta(&mut self, task: &DisjunctiveTask) { + // We need to find the leaf node index; note that there are |nodes| / 2 leaves + let position = self.nodes.len() / 2 + self.mapping[task.id]; + self.nodes[position] = Node::empty(); + self.upheap(position) + } + + /// Returns the index of the left child of the provided index + fn get_left_child_index(index: usize) -> usize { + 2 * index + 1 + } + + /// Returns the index of the right child of the provided index + fn get_right_child_index(index: usize) -> usize { + 2 * index + 2 + } + + /// Returns the index of the parent of the provided index + fn get_parent(index: usize) -> usize { + pumpkin_assert_simple!(index > 0); + (index - 1) / 2 + } + + /// Returns whether the provided index is a leaf node by checking whether its left child is + /// outside of the range of the number of nodes + fn is_leaf(&self, index: usize) -> bool { + pumpkin_assert_simple!(index < self.nodes.len()); + Self::get_left_child_index(index) >= self.nodes.len() + } + + /// Calculate the new values for the ancestors of the provided index + pub(super) fn upheap(&mut self, mut index: usize) { + while index != 0 { + let parent = Self::get_parent(index); + let left_child_parent = Self::get_left_child_index(parent); + let right_child_parent = Self::get_right_child_index(parent); + pumpkin_assert_simple!(left_child_parent == index || right_child_parent == index); + + self.nodes[parent].sum_of_processing_times = self.nodes[left_child_parent] + .sum_of_processing_times + + self.nodes[right_child_parent].sum_of_processing_times; + self.nodes[parent].ect = max( + self.nodes[right_child_parent].ect, + self.nodes[left_child_parent].ect + + self.nodes[right_child_parent].sum_of_processing_times, + ); + + self.nodes[parent].sum_of_processing_times_bar = max( + self.nodes[left_child_parent].sum_of_processing_times_bar + + self.nodes[right_child_parent].sum_of_processing_times, + self.nodes[left_child_parent].sum_of_processing_times + + self.nodes[right_child_parent].sum_of_processing_times_bar, + ); + self.nodes[parent].ect_bar = max( + self.nodes[right_child_parent].ect_bar, + max( + self.nodes[left_child_parent].ect + + self.nodes[right_child_parent].sum_of_processing_times_bar, + self.nodes[left_child_parent].ect_bar + + self.nodes[right_child_parent].sum_of_processing_times, + ), + ); + + index = parent; + } + } +} + +#[cfg(test)] +mod tests { + use crate::engine::propagation::LocalId; + use crate::engine::propagation::PropagationContext; + use crate::engine::test_solver::TestSolver; + use crate::propagators::disjunctive::theta_lambda_tree::Node; + use crate::propagators::disjunctive::theta_lambda_tree::ThetaLambdaTree; + use crate::propagators::disjunctive_task::DisjunctiveTask; + + #[test] + fn tree_built_correctly() { + let mut solver = TestSolver::default(); + let a = solver.new_variable(0, 0); + let b = solver.new_variable(25, 25); + let c = solver.new_variable(30, 30); + let d = solver.new_variable(32, 32); + let tasks = [ + DisjunctiveTask { + start_variable: a, + processing_time: 5, + id: LocalId::from(0), + }, + DisjunctiveTask { + start_variable: b, + processing_time: 9, + id: LocalId::from(1), + }, + DisjunctiveTask { + start_variable: c, + processing_time: 5, + id: LocalId::from(2), + }, + DisjunctiveTask { + start_variable: d, + processing_time: 10, + id: LocalId::from(3), + }, + ]; + + let mut tree = ThetaLambdaTree::new(&tasks, PropagationContext::new(&solver.assignments)); + + for task in tasks.iter() { + tree.add_to_theta(task, PropagationContext::new(&solver.assignments)); + } + tree.remove_from_theta(&tasks[2]); + tree.add_to_lambda(&tasks[2], PropagationContext::new(&solver.assignments)); + + assert_eq!( + tree.nodes[6], + Node { + ect: 42, + sum_of_processing_times: 10, + ect_bar: 42, + sum_of_processing_times_bar: 10 + } + ); + assert_eq!( + tree.nodes[5], + Node { + ect: i32::MIN, + sum_of_processing_times: 0, + ect_bar: 35, + sum_of_processing_times_bar: 5 + } + ); + assert_eq!( + tree.nodes[4], + Node { + ect: 34, + sum_of_processing_times: 9, + ect_bar: 34, + sum_of_processing_times_bar: 9 + } + ); + assert_eq!( + tree.nodes[3], + Node { + ect: 5, + sum_of_processing_times: 5, + ect_bar: 5, + sum_of_processing_times_bar: 5 + } + ); + assert_eq!( + tree.nodes[2], + Node { + ect: 42, + sum_of_processing_times: 10, + ect_bar: 45, + sum_of_processing_times_bar: 15 + } + ); + assert_eq!( + tree.nodes[1], + Node { + ect: 34, + sum_of_processing_times: 14, + ect_bar: 34, + sum_of_processing_times_bar: 14 + } + ); + assert_eq!( + tree.nodes[0], + Node { + ect: 44, + sum_of_processing_times: 24, + ect_bar: 49, + sum_of_processing_times_bar: 29 + } + ); + } +} diff --git a/pumpkin-solver/src/propagators/disjunctive/theta_tree.rs b/pumpkin-solver/src/propagators/disjunctive/theta_tree.rs new file mode 100644 index 00000000..7caa22a4 --- /dev/null +++ b/pumpkin-solver/src/propagators/disjunctive/theta_tree.rs @@ -0,0 +1,160 @@ +use std::cmp::max; + +use super::disjunctive_task::DisjunctiveTask; +use crate::containers::KeyedVec; +use crate::containers::StorageKey; +use crate::engine::propagation::LocalId; +use crate::engine::propagation::PropagationContext; +use crate::engine::propagation::ReadDomains; +use crate::pumpkin_assert_simple; +use crate::variables::IntegerVariable; + +// A node in the [`ThetaTree`] which keeps track of the ECT and sum of processing times of its +// children +#[derive(Debug, Clone)] +struct Node { + ect: i32, + sum_of_processing_times: i32, +} + +impl Node { + // Constructs an empty node + fn empty() -> Self { + Self { + ect: i32::MIN, + sum_of_processing_times: 0, + } + } + + // Construct a new node with the provided value + fn new(ect: i32, sum_of_processing_times: i32) -> Self { + Self { + ect, + sum_of_processing_times, + } + } +} + +/// A structure for efficiently calculating the ECT of a set of tasks. +/// +/// The implementation is based on \[1\]. The idea is to have a complete binary tree where the leaf +/// nodes represent the tasks. These leaf nodes are sorted by EST and this allows the values of the +/// inner nodes to be calculated using a recursive formula. +/// +/// # Bibliography +/// \[1\] P. Vilím, ‘Filtering algorithms for the unary resource constraint’, Archives of Control +/// Sciences, vol. 18, no. 2, pp. 159–202, 2008. +#[allow(dead_code, reason = "Will be part of the public API")] +#[derive(Debug)] +pub(super) struct ThetaTree { + nodes: Vec, + /// Then we keep track of a mapping from the [`LocalId`] to its position in the tree since the + /// methods take as input tasks with [`LocalId`]s. + mapping: KeyedVec, +} + +#[allow(dead_code, reason = "Will be part of the public API")] +impl ThetaTree { + pub(super) fn new( + tasks: &[DisjunctiveTask], + context: PropagationContext, + ) -> Self { + // First we sort the tasks by lower-bound + let mut sorted_tasks = tasks.to_vec(); + sorted_tasks.sort_by_key(|task| context.lower_bound(&task.start_variable)); + + // Then we keep track of a mapping from the [`LocalId`] to its position in the tree + let mut mapping = KeyedVec::default(); + for (index, task) in sorted_tasks.iter().enumerate() { + while mapping.len() <= task.id.index() { + let _ = mapping.push(usize::MAX); + } + mapping[task.id] = index + } + + // Calculate the number of internal nodes which are required to create the binary tree + let mut number_of_internal_nodes = 1; + while number_of_internal_nodes < tasks.len() { + number_of_internal_nodes <<= 1; + } + let nodes = vec![Node::empty(); 2 * number_of_internal_nodes - 1]; + ThetaTree { nodes, mapping } + } + + /// Returns the ECT of Theta + pub(super) fn ect(&self) -> i32 { + pumpkin_assert_simple!(!self.nodes.is_empty()); + self.nodes[0].ect + } + + /// Returns the sum of processing times of Theta + pub(super) fn sum_of_processing_times(&self) -> i32 { + pumpkin_assert_simple!(!self.nodes.is_empty()); + self.nodes[0].sum_of_processing_times + } + + /// Add the provided task to Theta + pub(super) fn add( + &mut self, + task: &DisjunctiveTask, + context: PropagationContext, + ) { + // We need to find the leaf node index; note that there are |nodes| / 2 leaves + let position = self.nodes.len() / 2 + self.mapping[task.id]; + let ect = context.lower_bound(&task.start_variable) + task.processing_time; + + self.nodes[position] = Node::new(ect, task.processing_time); + self.upheap(position) + } + + /// Remove the provided task from Theta + pub(super) fn remove(&mut self, task: &DisjunctiveTask) { + // We need to find the leaf node index; note that there are |nodes| / 2 leaves + let position = self.nodes.len() / 2 + self.mapping[task.id]; + self.nodes[position] = Node::empty(); + self.upheap(position) + } + + /// Returns the index of the left child of the provided index + fn get_left_child_index(index: usize) -> usize { + 2 * index + 1 + } + + /// Returns the index of the right child of the provided index + fn get_right_child_index(index: usize) -> usize { + 2 * index + 2 + } + + /// Returns the index of the parent of the provided index + fn get_parent(index: usize) -> usize { + pumpkin_assert_simple!(index > 0); + (index - 1) / 2 + } + + /// Calculate the new values for the ancestors of the provided index + pub(super) fn upheap(&mut self, mut index: usize) { + while index != 0 { + // First we get the parent of the current index + let parent = Self::get_parent(index); + // Then we get the children of this parent + let left_child_parent = Self::get_left_child_index(parent); + let right_child_parent = Self::get_right_child_index(parent); + pumpkin_assert_simple!( + left_child_parent == index || right_child_parent == index, + "Either the left or the right child should be equal to the provided index" + ); + + // Then we update the values according to the formula + self.nodes[parent].sum_of_processing_times = self.nodes[left_child_parent] + .sum_of_processing_times + + self.nodes[right_child_parent].sum_of_processing_times; + self.nodes[parent].ect = max( + self.nodes[right_child_parent].ect, + self.nodes[left_child_parent].ect + + self.nodes[right_child_parent].sum_of_processing_times, + ); + + index = parent; + } + } +} diff --git a/pumpkin-solver/src/propagators/mod.rs b/pumpkin-solver/src/propagators/mod.rs index 384fac78..92c44ee7 100644 --- a/pumpkin-solver/src/propagators/mod.rs +++ b/pumpkin-solver/src/propagators/mod.rs @@ -8,8 +8,10 @@ pub(crate) mod element; pub(crate) mod nogoods; mod reified_propagator; pub(crate) use arithmetic::*; +mod disjunctive; pub use cumulative::CumulativeExplanationType; pub use cumulative::CumulativeOptions; pub use cumulative::CumulativePropagationMethod; pub(crate) use cumulative::*; +pub(crate) use disjunctive::*; pub(crate) use reified_propagator::*; diff --git a/pumpkin-solver/tests/mzn_constraint_test.rs b/pumpkin-solver/tests/mzn_constraint_test.rs index 329aae8a..bd018b69 100644 --- a/pumpkin-solver/tests/mzn_constraint_test.rs +++ b/pumpkin-solver/tests/mzn_constraint_test.rs @@ -63,6 +63,8 @@ mzn_test!(bool_lin_eq); mzn_test!(bool_lin_le); mzn_test!(bool_clause); +mzn_test!(disjunctive_strict); + cumulative!(time_table_per_point); cumulative!(time_table_per_point_incremental); cumulative!(time_table_per_point_incremental_synchronised); diff --git a/pumpkin-solver/tests/mzn_constraints/disjunctive_strict.expected b/pumpkin-solver/tests/mzn_constraints/disjunctive_strict.expected new file mode 100644 index 00000000..de60482b --- /dev/null +++ b/pumpkin-solver/tests/mzn_constraints/disjunctive_strict.expected @@ -0,0 +1,201 @@ +x = 8; +y = 5; +z = 0; +---------- +x = 5; +y = 7; +z = 0; +---------- +x = 5; +y = 8; +z = 0; +---------- +x = 6; +y = 8; +z = 0; +---------- +x = 6; +y = 8; +z = 1; +---------- +x = 0; +y = 7; +z = 2; +---------- +x = 0; +y = 8; +z = 2; +---------- +x = 8; +y = 0; +z = 3; +---------- +x = 0; +y = 8; +z = 3; +---------- +x = 1; +y = 8; +z = 3; +---------- +x = 3; +y = 0; +z = 5; +---------- +x = 0; +y = 2; +z = 5; +---------- +x = 3; +y = 0; +z = 6; +---------- +x = 4; +y = 0; +z = 6; +---------- +x = 4; +y = 1; +z = 6; +---------- +x = 0; +y = 2; +z = 6; +---------- +x = 0; +y = 3; +z = 6; +---------- +x = 1; +y = 3; +z = 6; +---------- +x = 3; +y = 0; +z = 7; +---------- +x = 4; +y = 0; +z = 7; +---------- +x = 5; +y = 0; +z = 7; +---------- +x = 4; +y = 1; +z = 7; +---------- +x = 5; +y = 1; +z = 7; +---------- +x = 0; +y = 2; +z = 7; +---------- +x = 5; +y = 2; +z = 7; +---------- +x = 0; +y = 3; +z = 7; +---------- +x = 1; +y = 3; +z = 7; +---------- +x = 0; +y = 4; +z = 7; +---------- +x = 1; +y = 4; +z = 7; +---------- +x = 2; +y = 4; +z = 7; +---------- +x = 3; +y = 0; +z = 8; +---------- +x = 4; +y = 0; +z = 8; +---------- +x = 5; +y = 0; +z = 8; +---------- +x = 6; +y = 0; +z = 8; +---------- +x = 4; +y = 1; +z = 8; +---------- +x = 5; +y = 1; +z = 8; +---------- +x = 6; +y = 1; +z = 8; +---------- +x = 0; +y = 2; +z = 8; +---------- +x = 5; +y = 2; +z = 8; +---------- +x = 6; +y = 2; +z = 8; +---------- +x = 0; +y = 3; +z = 8; +---------- +x = 1; +y = 3; +z = 8; +---------- +x = 6; +y = 3; +z = 8; +---------- +x = 0; +y = 4; +z = 8; +---------- +x = 1; +y = 4; +z = 8; +---------- +x = 2; +y = 4; +z = 8; +---------- +x = 0; +y = 5; +z = 8; +---------- +x = 1; +y = 5; +z = 8; +---------- +x = 2; +y = 5; +z = 8; +---------- +x = 3; +y = 5; +z = 8; +---------- +========== diff --git a/pumpkin-solver/tests/mzn_constraints/disjunctive_strict.fzn b/pumpkin-solver/tests/mzn_constraints/disjunctive_strict.fzn new file mode 100644 index 00000000..7ce327a4 --- /dev/null +++ b/pumpkin-solver/tests/mzn_constraints/disjunctive_strict.fzn @@ -0,0 +1,7 @@ +var 0..8: x :: output_var; +var 0..8: y :: output_var; +var 0..8: z :: output_var; + +constraint pumpkin_disjunctive_strict([x, y, z], [2, 3, 5]); + +solve satisfy; diff --git a/pumpkin-solver/tests/mzn_constraints/disjunctive_strict.template b/pumpkin-solver/tests/mzn_constraints/disjunctive_strict.template new file mode 100644 index 00000000..98caf5a6 --- /dev/null +++ b/pumpkin-solver/tests/mzn_constraints/disjunctive_strict.template @@ -0,0 +1,9 @@ +predicate gecode_schedule_unary(array [int] of var int: x,array [int] of int: p); + +var 0..8: x :: output_var; +var 0..8: y :: output_var; +var 0..8: z :: output_var; + +constraint gecode_schedule_unary([x, y, z], [2, 3, 5]); + +solve satisfy;