Satisfiability Problem · SAT solvers

Lesson 9

Nikolai Chukhin · Alexander S. Kulikov

Programming problem. A person wants to install parquet flooring in his house, but there are two difficulties: first, he insists that the parquet tiles must be in the shape of a Z-tetromino, and second, the floor in his house has a very whimsical shape: the walls are uneven, there are columns, pipes, etc. This person tried for a long time to figure out whether it is possible to tile the floor the way he wants but couldn't find the solution. Determine a tiling plan if it exists, or report that such tiling is not possible.

  • Input format.  The shape of the floor is given as an \(n \times n\) square, from which \(m\) cells have been removed.
    The first line contains two numbers separated by a space \(n \leq 40\) and \(m \leq n^{2}\). In the following \(m\) lines, the coordinates \(i, j \in \{0, …, n-1\}\) of each removed cell are given separated by a space.

  • Output format.  If no tiling exists, the output should contain only the word NO. If it exists, the first line of the output should contain the word YES, and the following \((n^{2} - m) / 4\) lines should describe the tetrominoes, one per line.
    The tetrominoes are encoded by three numbers \(i, j, k\) separated by a space, where \(i, j\) are the coordinates of the cell marked with an asterisk in the picture below, and \(k\) is the type of tetromino indicated above it.

5 points
Public samples
Public sample 1
Input
3 5
0 2
1 0
2 0
2 1
2 2
Expected output
YES
0 0 3