Problem solving

Solving a scheduling problem involves the SchedulingSolver class.

Define the solver

A SchedulingSolver instance takes a SchedulingProblem instance:

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.

Solve

Just call the solve() method. This method returns a Solution instance.

solution = solver.solve()

Running the solve() method returns can either fail or succeed, according to the 4 following cases:

  1. 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.

  1. The problem cannot be solved for an unknown reason (the satisfiability of the set of constraints cannot be computed). The solve() method returns False.

  2. The solver takes too long to complete and exceeds the allowed max_time. The solve() method returns False.

  3. The solver successes in finding a schedule that satisfies all the constraints. The solve() method returns the solution as a JSON dictionary.

Note

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.

Note

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

If the 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

Call the 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 Task or Resource (default).

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

Call the 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')