disjunctive_scheduling/
disjunctive_scheduling.rs

1//! A simple model for disjunctive scheduling using reified constraints
2//! Given a set of tasks and their processing times, it finds a schedule such that none of the jobs
3//! overlap. The optimal schedule is thus all tasks scheduled right after each other.
4//!
5//! For two tasks x and y, either x ends before y starts, or y ends before x starts. So if s_i is
6//! the start time of task i and p_i is then we can express the condition that x ends before y
7//! starts as s_x + p_x <= s_y, and that y ends before x starts as s_y + p_y <= s_x.
8//!
9//! To ensure that one of these occurs, we create two Boolean variables, l_xy and l_yx, to signify
10//! the two possibilities, and then post the constraint (l_xy \/ l_yx).
11
12use pumpkin_solver::constraints;
13use pumpkin_solver::constraints::NegatableConstraint;
14use pumpkin_solver::results::ProblemSolution;
15use pumpkin_solver::results::SatisfactionResult;
16use pumpkin_solver::termination::Indefinite;
17use pumpkin_solver::variables::TransformableVariable;
18use pumpkin_solver::Solver;
19
20fn main() {
21    let mut args = std::env::args();
22
23    let n_tasks = args
24        .nth(1)
25        .expect("Please provide a number of tasks")
26        .parse::<usize>()
27        .expect("Not a valid usized");
28    let processing_times = args
29        .take(n_tasks)
30        .map(|arg| arg.parse::<usize>())
31        .collect::<Result<Vec<_>, _>>()
32        .expect("The provided processing times are not valid unsigned integers");
33    assert_eq!(
34        processing_times.len(),
35        n_tasks,
36        "Provided fewer than `n_tasks` processing times."
37    );
38
39    let horizon = processing_times.iter().sum::<usize>();
40
41    let mut solver = Solver::default();
42
43    // Creates a dummy constraint tag; since this example does not support proof logging the
44    // constraint tag does not matter.
45    let constraint_tag = solver.new_constraint_tag();
46
47    let start_variables = (0..n_tasks)
48        .map(|i| solver.new_bounded_integer(0, (horizon - processing_times[i]) as i32))
49        .collect::<Vec<_>>();
50
51    // Literal which indicates precedence (i.e. precedence_literals[x][y] <=> x ends before y
52    // starts)
53    let precedence_literals = (0..n_tasks)
54        .map(|_| {
55            (0..n_tasks)
56                .map(|_| solver.new_literal())
57                .collect::<Vec<_>>()
58        })
59        .collect::<Vec<_>>();
60
61    for x in 0..n_tasks {
62        for y in 0..n_tasks {
63            if x == y {
64                continue;
65            }
66            // precedence_literals[x][y] <=> x ends before y starts
67            let literal = precedence_literals[x][y];
68            // literal <=> (s_x + p_x <= s_y)
69            // equivelent to literal <=> (s_x - s_y <= -p_x)
70            // So the variables are -s_y and s_x, and the rhs is -p_x
71            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
72            let _ = constraints::less_than_or_equals(
73                variables,
74                -(processing_times[x] as i32),
75                constraint_tag,
76            )
77            .reify(&mut solver, literal);
78
79            // Either x starts before y or y start before x
80            let _ = solver.add_clause(
81                [
82                    literal.get_true_predicate(),
83                    precedence_literals[y][x].get_true_predicate(),
84                ],
85                constraint_tag,
86            );
87        }
88    }
89
90    let mut brancher = solver.default_brancher();
91    if matches!(
92        solver.satisfy(&mut brancher, &mut Indefinite),
93        SatisfactionResult::Unsatisfiable(_, _),
94    ) {
95        panic!("Infeasibility Detected")
96    }
97    match solver.satisfy(&mut brancher, &mut Indefinite) {
98        SatisfactionResult::Satisfiable(satisfiable) => {
99            let solution = satisfiable.solution();
100
101            let mut start_variables_and_processing_times = start_variables
102                .iter()
103                .zip(processing_times)
104                .collect::<Vec<_>>();
105            start_variables_and_processing_times.sort_by(|(s1, _), (s2, _)| {
106                solution
107                    .get_integer_value(**s1)
108                    .cmp(&solution.get_integer_value(**s2))
109            });
110
111            println!(
112                "{}",
113                start_variables_and_processing_times
114                    .iter()
115                    .map(|(var, processing_time)| format!(
116                        "[{}, {}]",
117                        solution.get_integer_value(**var),
118                        solution.get_integer_value(**var) + *processing_time as i32
119                    ))
120                    .collect::<Vec<_>>()
121                    .join(" - ")
122            );
123        }
124        SatisfactionResult::Unsatisfiable(_, _) => panic!("Infeasibility Detected"),
125        SatisfactionResult::Unknown(_, _) => println!("Timeout."),
126    };
127}
disjunctive_scheduling/disjunctive_scheduling.rs

disjunctive_scheduling/
disjunctive_scheduling.rs
