## Exercise 1›:

Steel mill planification
Note: this problem has been taken from the Logic in Information Technology subject at Barcelona School of Informatics.

Solve the following exercise by means of a reduction to SAT:
• Determine if a steel mill can finish a set of tasks in $h$ hours. The steel mill can perform up to $3$ tasks at the same time, and disposes of $2$ furnaces and $1$ refrigerator. Each task consists of three phases: preparation ($1$ hour), smelting ($x$ hours), and cooling down ($5$ hours). Once a task has started, all the process must be performed without interruption. The smelting phase requires a furnace, whereas the cooling down phase requires a refrigerator. Note that the only thing that changes between tasks is the furnace time. Given a set of tasks with different furance times, find an arrangement, if possible, such that all tasks are finished in $h$ hours with the available resources.
The input of the exercise and the output with the solution (when the input is solvable) are as follows:
• h: int

The input consists of the number $h$ of hours allowed to finish all the tasks, and the list tasks with the smelting times (in hours) for each of the tasks.
• arrangement: array of int

The output is a list of numbers in $\{0,\ldots,h-1\}$, where the $i$’th number in the list is the starting hour of the $i$’th task. Note that it is not necessary to specify the assigned furance to each task: it is sufficient to assert that at any point of time, there are at most two tasks in the furnace phase.