Closed dreinon closed 3 years ago
I'm not sure the second point is an optimization problem. I would say it is a constraint.
I don't understand the first sentence of the first point.
The formula itself can be implemented using an Indicator and a MaximizeObjective or a MinimizeObjective
Let me explain the first sentence of the first point better:
w
be the number of tasks worker A
wants to do in a week.w
optional tasks to our problem, assign these tasks to worker A and supervisor, and the same for all other workers.We try to maximize supervisor's workload, so "the bussiness" is always working, but since a working week is 40 hours long, then some workers probably won't be able to do as many tasks as they wanted.
Since we want workers to be happy, the more similar the number of tasks assigned to each worker is with respect to the number of tasks desired by this worker, the better the schedule will be.
This first point is achieved simply by maximizing workload of supervisor, but to implement the formula as indicator, is there a way to express the number of tasks a resource will be sheduled?
Hi! I succeeded on the first point.
For the tasks distance, I would like to filter tasks that a worker will be scheduled to get only the ones that fit between certain timepoints. I'm getting worker tasks by calling worker.get_busy_intervals()
, which returns a list of ArithRef
intervals each of which represents a task.
Then, I use filter
function as follows:
from z3 import And
import processscheduler as ps
worker = ps.Worker('example_worker')
worker_tasks = worker.get_busy_intervals()
interval_to_fit_in = [0, 10] # For example
filtered_tasks = list(filter(lambda task: And(task[0] >= interval_to_fit_in[0], task[1] <= interval_to_fit_in[1]), worker_tasks))
but I get the following error:
z3.z3types.Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values.
I understand why the error, but I don't know how to solve it.
Have you experienced something similar before? Thanks!
@dreinon I cannot duplicate the issue given the code snippet.
is there a way to express the number of tasks a resource will be scheduled? No, I have to think about it, it's not obvious.
@dreinon See commit 60a8f1124569098449222964ec3e1ab9f3f8eec9 for the number of tasks a resource is assigned
I don't know if an indicator is the best way to proceed, it might also be a property of any Resource. The benefit of an indicator is that it is computed only when requested (i.e. only if the indicator is defined). Compute this data in all cases could increase the computation time whereas it's not always needed
@dreinon See commit 60a8f11 for the number of tasks a resource is assigned
I implemented this using the following code:
from z3 import Sum
Sum([end-start for start, end in worker.get_busy_intervals()])
Which isn't the number of tasks but actually the workload of the resource. I think this would work but I haven't tried it as an objective yet.
I don't know if an indicator is the best way to proceed, it might also be a property of any Resource. The benefit of an indicator is that it is computed only when requested (i.e. only if the indicator is defined). Compute this data in all cases could increase the computation time whereas it's not always needed
I understand.
@dreinon I cannot duplicate the issue given the code snippet.
is there a way to express the number of tasks a resource will be scheduled? No, I have to think about it, it's not obvious.
Sorry, here's the code snippet which you'll be able to reproduce the issue with:
from z3 import And, If
import processscheduler as ps
problem = ps.SchedulingProblem('example_problem', horizon = 20)
worker = ps.Worker('example_worker')
task_1 = ps.FixedDurationTask('task1', 1, optional=True)
task_2 = ps.FixedDurationTask('task2', 1, optional=True)
task_1.add_required_resource(worker)
task_2.add_required_resource(worker)
worker_tasks = worker.get_busy_intervals()
interval_to_fit_in = [0, 10] # For example
filtered_tasks = list(filter(lambda task: If(And(task[0] >= interval_to_fit_in[0], task[1] <= interval_to_fit_in[1]), 1, 0), worker_tasks))
@dreinon ok I understand what you're trying to do. The filtered tasks list cannot be built using the python filter
method because the lambda function does not return a boolean. You could eventually proceed that way after the solver has found a solution, because you can evaluate all z3 Boolean sorts to python bools. If you need an array to be part of the mathematical formulation of the scheduling problem, you need to use a z3 Array (https://ericpony.github.io/z3py-tutorial/advanced-examples.htm), not a python list. Using Arrays is not straight forward, so far I managed to get done without them.
Right, I read about z3 arrays but I don't think they provide what I am expecting. I also read that there are boolean, int and real vectors which list comprehension can be used with, but I don't know about list comprehension filtering.
You could eventually proceed that way after the solver has found a solution, because you can evaluate all z3 Boolean sorts to python bools
Good to know, but I need to have an expression that lets me say: the tasks that will be scheduled between interval 0 and 10 (for instance), because I need to use these tasks to build a sum that will be added to the objective.
Maybe what I want to do isn't possible. Thanks @tpaviot!
I think this "get tasks that will be scheduled in a time interval" issue needs a specific ticket
I wrote a score formula for scheduler results which involves:
It would be ideal if I could implement the formula itself as an objective in terms that z3 solver understands, so the solver would now exactly what we are trying to achieve.
With these, my objective is to:
I would like to know if this is possible and if it is, how to proceed. Thanks!