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
  tasks: array of 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.