Solve the following exercise by means of a reduction to
SAT:
The input of the exercise and the output with the solution (when the input is
solvable) are as follows:

n: int
m: int
shapes: array of int
bitmasks: array of array of array of array of int
The input contains the number $n$ of rows and $m$ of columns of the playing
board. The list shapes contains a sequence of numbers
in $\{0,\ldots,6\}$, where the $i$’th position contains the shape identifier
of the $i$’th shape to place in the board.
The bitmasks variable is not really part of the input of the problem
and can be ignored. Nevertheless, it is provided for convenience, as in some
cases it might ease the description of the reduction. It always contains the
following information. For each shape identifier i, bitmasks[i]
is a list of the possible “rotated shapes” corresponding to the shape
i, where each “rotated shape” is a minimalsize 2dimensional matrix
of $0$’s (meaning free space) and $1$’s (meaning filled space). For instance,
bitmasks[4] is a list with the following two “rotated shapes”:
[[0 1 1] [[1 0]
1 1 0]] [1 1]
[0 1]]
Note that the last row of both matrixes corresponds to the bottom of the shape,
whereas row $0$ corresponds to its top (which follows the same convention of the
playing board).

board: array of array of int
The output consists of the state of the board once all the pieces have been
placed. It must be an $n\times m$ matrix containing the piece found at each
cell (the ground row is board[n1] and the top row is board[0]).
A piece is identified by its index in the shapes list (starting
at $0$), whereas an empty cell is identified with a $1$.
For instance, for input
n = 3
m = 10
shapes = [6 5 4 3 2 0]
a valid solution would be:
5 5 5 5 2 · · · 4 4
0 0 1 1 2 2 3 · · 4
0 0 · 1 1 2 3 3 3 4
where each dot should actually be a
$1$.
Note that a board as this one:
3 3 3 3 ·
· 2 2 2 ·
· · · 2 ·
0 4 4 1 ·
0 · 4 1 ·
0 0 4 1 1
is valid, because the shape with index
$4$ does not have any shape with lower
index
directly above it, even though it is clear that it would be
impossible to place it there. On the other hand, the situation of this
other board:
0 0 0 1 ·
· 0 1 1 1
is not valid, as the shape with index
$1$ has the shape with index
$0$ directly
above it.