feat: adding edge-finding for disjunctive

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.

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);

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]

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<bool, FlatZincError> {
+    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],

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<StartTimes, Durations>(
+    start_times: StartTimes,
+    durations: Durations,
+) -> impl Constraint
+where
+    StartTimes: IntoIterator,
+    StartTimes::Item: IntegerVariable + Debug + 'static,
+    StartTimes::IntoIter: ExactSizeIterator,
+    Durations: IntoIterator<Item = i32>,
+    Durations::IntoIter: ExactSizeIterator,
+{
+    Disjunctive::new(
+        start_times
+            .into_iter()
+            .zip(durations)
+            .map(|(start_time, duration)| ArgDisjunctiveTask {
+                start_variable: start_time,
+                processing_time: duration,
+            }),
+    )
+}

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;

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)

pumpkin-solver/src/propagators/cumulative/time_table/time_table_over_interval.rs

@@ -54,7 +54,6 @@ pub(crate) struct Event<Var> {
 /// \[1\] A. Schutt, Improving scheduling by learning. University of Melbourne, Department of
 /// Computer Science and Software Engineering, 2011.
 #[derive(Debug)]
-
 pub(crate) struct TimeTableOverIntervalPropagator<Var> {
     /// Stores whether the time-table is empty
     is_time_table_empty: bool,