Solve the following exercise by means of a reduction to SAT:

• Determine if a sequence of tetris shapes can fit in the playing board, i.e., if the shapes fit in a matrix of $n > 0$ rows and $m > 0$ columns. The different shapes are identified by a number as follows:

            X
            X        X        X         X       X         X
            X        XX       X         X       XX       XX       XX
            X        X        XX       XX        X       X        XX
  
    ID  =   0        1        2        3        4        5        6
  

  Shapes can be placed anywhere in the board, with the following restrictions:
  • Shapes cannot overlap.
  • Shapes must be supported, i.e., they must have at least one block in the ground row (index $n-1$) or directly above another shape.
  • Shapes must be placed in order, i.e., a shape cannot appear directly above another shape that appears later in the list.
  • Shapes can be rotated.
  • A row completely filled does not disappear.

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 minimal-size 2-dimensional 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[n-1] 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.