Solving a scheduling problem involves the
Define the solver¶
SchedulingSolver instance takes a
solver = SchedulingSolver(scheduling_problem_instance)
It takes the following optional arguments:
debug: False by default, if set to True will output many useful information.
max_time: in seconds, the maximal time allowed to find a solution. Default is 60s.
parallel: boolean False by default, if True force the solver to be executed in multithreaded mode. It might be quicker. It might not.
random_values: a boolean, default to
False. If set to
True, enable a builtin generator to set random initial values. By setting this attribute to
True, one expects the solver to give a different solution each time it is called.
logics: a string, None by default. Can be set to any of the supported z3 logics, “QF_IDL”, “QF_LIA”, etc. see https://smtlib.cs.uiowa.edu/logics.shtml. By default (logics set to None), the solver tries to find the best logics, but there can be significant improvements by setting a specific logics (“QF_IDL” or “QF_UFIDL” seems to give the best performances).
verbosity: an integer, 0 by default. 1 or 2 increases the solver verbosity. TO be used in a debugging or inspection purpose.
Just call the
solve() method. This method returns a
solution = solver.solve()
solve() method returns can either fail or succeed, according to the 4 following cases:
The problem cannot be solved because some constraints are contradictory. It is called “Unsatisfiable”. The
solve()method returns False. For example:
TaskStartAt(cook_the_chicken, 2) TaskStartAt(cook_the_chicken, 3)
It is obvious that these constraints cannot be both satisfied.
The problem cannot be solved for an unknown reason (the satisfiability of the set of constraints cannot be computed). The
solve()method returns False.
The solver takes too long to complete and exceeds the allowed
solve()method returns False.
The solver successes in finding a schedule that satisfies all the constraints. The
solve()method returns the solution as a JSON dictionary.
If the solver fails to give a solution, increase the
max_time (case 3) or remove some constraints (cases 1 and 2).
Find another solution¶
The solver may schedule:
one solution among many, in the case where there is no optimization,
the best possible schedule in case of an optimization issue.
In both cases, you may need to check a different schedule that fits all the constraints. Use the
find_another_solution() method and pass the variable you would want the solver to look for another solution.
Before requesting another solution, the
solve() method has first to be executed, i.e. there should already be a current solution.
You can pass any variable to the
find_another_solution() method: a task start, a task end, a task duration, a resource productivity etc.
For example, there are 5 different ways to schedule a FixedDurationTask with a duration=2 in an horizon of 6. The default solution returned by the solver is:
problem = ps.SchedulingProblem('FindAnotherSolution', horizon=6) solutions = task_1 = ps.FixedDurationTask('task1', duration=2) problem.add_task(task_1) solver = ps.SchedulingSolver(problem) solution = solver.solve() print("Solution for task_1.start:", task_1.scheduled_start)
Solution for task_1.start: 0
Then, we can request for another solution:
solution = solver.find_another_solution(task_1.start) if solution is not None: print("New solution for task_1.start:", solution.tasks[task_1.name].start)
Solution for task_1.start: 1
You can recursively call
find_another_solution() to find all possible solutions, until the solver fails to return a new one.
Run in debug mode¶
debug attribute is set to True, the z3 solver is run with the unsat_core option. This will result in a much longer computation time, but this will help identifying the constraints that conflict. Because of this higher consumption of resources, the
debug flag should be used only if the solver fails to find a solution.
Render to a Gantt chart¶
render_gantt_matplotlib() to render the solution as a Gantt chart. The time line is from 0 to
horizon value, you can choose to render either
solution = solver.solve() if solution is not None: solution.render_gantt_matplotlib() # default render_mode is 'Resource' # a second gantt chart, in 'Task' mode solution.render_gantt_matplotlib(render_mode='Task')
render_gantt_plotly() to render the solution as a Gantt chart using plotly.
Take care that plotly rendering needs real timepoints (set at least
delta_time at the problem creation).
solution = solver.solve() if solution is not None: # default render_mode is 'Resource' solution.render_gantt_plotly(sort="Start", html_filename="index.html") # a second gantt chart, in 'Task' mode solution.render_gantt_plotly(render_mode='Task')