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 hours.
The steel mill can perform up to tasks at the same time, and disposes of
furnaces and refrigerator.
Each task consists of three phases:
preparation ( hour), smelting ( hours), and
cooling down ( 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 hours
with the available resources.
The input of the exercise and the output with the solution (when the input is
solvable) are as follows: