Solving the problem of tiling using SAT Solver on the example of pentamino
Once I got the game pentamino, where it was necessary to put 13 figures in a square 8 by 8. After a certain period of time, during which I unsuccessfully tried to solve this problem, I decided that it was necessary to write a program that would do it for me. To do this, it was necessary to choose the solution algorithm. The first thing that comes to mind is the usual algorithm of branches and borders, when the figures fit one after another adjacent to each other (the algorithm with the dancing links is not suitable here, because the figures are different). To speed up this algorithm, various heuristics are usually used, for example, preference is given to branching with the least number of options. It is possible to invent and implement other heuristics in this algorithm, but then I thought that many different tricks to speed up the solution of such problems have already been implemented in SAT solvers. Therefore, it is necessary to translate the problem into the appropriate mathematical language and use some SAT solver. How it was implemented and what results turned out it is possible to read under a cat.
In the beginning I want to remind you what the game of pentamino is. This is a square 8x8 field, which must be tiled with 13 figures - 12 squiggles, which consist of 5 squares and one 2x2 figure:
Here it is worth saying what is the problem of the satisfiability of Boolean formulas (the Boolean satisfiability problem) or the problem of the SAT. In general terms, it can be formulated as the finding of such values of Boolean variables for which a given expression becomes true. Generally speaking, NP is a complete task, but there are many techniques that help to solve it effectively. For this, many special applications have been developed, called SAT solvers. I will use the SAT solver by the name of minisat. To solve this problem, it is necessary to rewrite the input expression in conjunctive normal form, that is, as a product of logical sums of variables. Each bracket in conjunctive normal form is called a clause here, which is the logical “or” of some literals, that is, Boolean variables or their denials. For example:
(x1 v not x3) (x2 v x4) (x2 v x3 v not x4)
I needed to translate the tiling task into the SAT task. Take a piece of pentamino and put it in the playing field in all possible ways, including shifts, turns and reflections. Each such position of the figure is comparable to a Boolean variable and we will assume that if we have this figure present in this particular position in the final decision, the variable will be true, and if it will not, then false. We do this for all shapes.
Now we will make a formula describing our task, that is, we will actually impose restrictions on our variables. The first thing to do is to ensure that all the cells of our playing field will be covered with at least one figure. To do this, for each cell of 64, we find all the figures and positions of these figures that cover a given cell and make a clot of the variables that are assigned to these positions of the figures. The second thing to do is to eliminate the intersection of the figures. This can be done in a double cycle, simply by going through all the possible positions of all the figures and determining whether the pair has common cells. If there is, then they intersect and it is necessary to add a clause of the form (not x_i V not x_j), where x_i is the variable assigning the first position and x_j the second position. This clause is true when x_i and x_j are not simultaneously equal to one, that is, it excludes intersections. And finally, the third thing that needs to be taken into account is that each figure can be present on the playing field only once. To do this, we also go through all positions of each figure in a double cycle and for each pair of positions of the same figure we make a clause similar to the previous one and consisting of two negations. That is, when two identical figures appear (but in different positions), one of such clauses will give false and, accordingly, will exclude such a solution.
It was all theory, and now let's move on to practice. Give each shape a number from 1 to d to distinguish it from others and is convenient to print. Then we will create a matrix of the playing field and encode the corresponding cells of the playing field as occupied / not occupied by the figure:
Now for each piece it is necessary to find all possible positions on the playing field by means of shifts, turns and reflections. Let's start with turns and reflections. There are a total of 8 possible transformations of turns and reflections, including one trivial transformation that leaves the shape intact. For these transformations, I create 8 corresponding matrices, as shown below. After turning or reflecting a figure can go beyond the playing field, therefore it is necessary to return it back to the playing field. It should also be noted that after transformation some figures may turn into themselves and such cases should be excluded. Unique options I add to the Orientation class. The result is the following code:
This code is applied to each of the figures, and then, the resulting unique Orientation are shifted along the x and y axes creating all possible positions of each figure. As a result, we have the following number of different positions for each of the figures:
Then we assign a Boolean variable to each possible position and create a formula as described above. After that, we call minisat directly from the application, which returns a solution - a set of our variables with assigned values of true or false. Knowing which positions were assigned these variables, we print the solution:
Naturally, it would not be so interesting to dwell on this. Therefore, the first question I had was this: “But how many different solutions exist that do not differ in trivial turns and reflections of the playing field?”. To do this, there is a mode in the SAT Solver that allows you to add clauses without losing existing information, which significantly speeds up the process compared to if a solution was sought from scratch. The next solution can be found by adding a clause that contains the negatives of all the variables present in the previous solution. After adding this procedure and comparing the new solution with the previous ones, taking into account the turns and reflections of the playing field, I received 1364 different options.
Another interesting extension that I implemented was the study of various other forms of the playing field and figures. And, finally, the study of three-dimensional playing fields was very interesting. But this is a topic for another article.
After adding an additional condition: for each piece of one clause - in the playing field there must be at least one position of this piece, the calculation has become much faster. In addition, one bug was fixed, as a result of which the number of all possible unique options is 16146.
In the beginning I want to remind you what the game of pentamino is. This is a square 8x8 field, which must be tiled with 13 figures - 12 squiggles, which consist of 5 squares and one 2x2 figure:
Here it is worth saying what is the problem of the satisfiability of Boolean formulas (the Boolean satisfiability problem) or the problem of the SAT. In general terms, it can be formulated as the finding of such values of Boolean variables for which a given expression becomes true. Generally speaking, NP is a complete task, but there are many techniques that help to solve it effectively. For this, many special applications have been developed, called SAT solvers. I will use the SAT solver by the name of minisat. To solve this problem, it is necessary to rewrite the input expression in conjunctive normal form, that is, as a product of logical sums of variables. Each bracket in conjunctive normal form is called a clause here, which is the logical “or” of some literals, that is, Boolean variables or their denials. For example:
(x1 v not x3) (x2 v x4) (x2 v x3 v not x4)
I needed to translate the tiling task into the SAT task. Take a piece of pentamino and put it in the playing field in all possible ways, including shifts, turns and reflections. Each such position of the figure is comparable to a Boolean variable and we will assume that if we have this figure present in this particular position in the final decision, the variable will be true, and if it will not, then false. We do this for all shapes.
Now we will make a formula describing our task, that is, we will actually impose restrictions on our variables. The first thing to do is to ensure that all the cells of our playing field will be covered with at least one figure. To do this, for each cell of 64, we find all the figures and positions of these figures that cover a given cell and make a clot of the variables that are assigned to these positions of the figures. The second thing to do is to eliminate the intersection of the figures. This can be done in a double cycle, simply by going through all the possible positions of all the figures and determining whether the pair has common cells. If there is, then they intersect and it is necessary to add a clause of the form (not x_i V not x_j), where x_i is the variable assigning the first position and x_j the second position. This clause is true when x_i and x_j are not simultaneously equal to one, that is, it excludes intersections. And finally, the third thing that needs to be taken into account is that each figure can be present on the playing field only once. To do this, we also go through all positions of each figure in a double cycle and for each pair of positions of the same figure we make a clause similar to the previous one and consisting of two negations. That is, when two identical figures appear (but in different positions), one of such clauses will give false and, accordingly, will exclude such a solution.
It was all theory, and now let's move on to practice. Give each shape a number from 1 to d to distinguish it from others and is convenient to print. Then we will create a matrix of the playing field and encode the corresponding cells of the playing field as occupied / not occupied by the figure:
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. 1 1 . . . . .
1 1 . . . . . .
. 1 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
3 . . . . . . .
3 . . . . . . .
3 . . . . . . .
3 3 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
4 . . . . . . .
4 . . . . . . .
4 4 . . . . . .
. 4 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
5 5 . . . . . .
5 5 . . . . . .
5 . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
6 6 6 . . . . .
. 6 . . . . . .
. 6 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
7 . 7 . . . . .
7 7 7 . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
8 . . . . . . .
8 . . . . . . .
8 8 8 . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . 9 . . . . .
. 9 9 . . . . .
9 9 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. a . . . . . .
aaa . . . . .
. a . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
b . . . . . . .
bb . . . . . .
b . . . . . . .
b . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. cc . . . . .
. c . . . . . .
cc . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
dd . . . . . .
dd . . . . . .
Now for each piece it is necessary to find all possible positions on the playing field by means of shifts, turns and reflections. Let's start with turns and reflections. There are a total of 8 possible transformations of turns and reflections, including one trivial transformation that leaves the shape intact. For these transformations, I create 8 corresponding matrices, as shown below. After turning or reflecting a figure can go beyond the playing field, therefore it is necessary to return it back to the playing field. It should also be noted that after transformation some figures may turn into themselves and such cases should be excluded. Unique options I add to the Orientation class. The result is the following code:
int dimension_ = 2; const unsigned int MATRIX_SIZE = dimension_ * dimension_; int * matrix = new int[ MATRIX_SIZE ]; for( unsigned int i = 0; i < MATRIX_SIZE; i++ ) { matrix[ i ] = 0; } for( unsigned int i = 0; i < dimension_; i++ ) { int * matrix1 = new int[ MATRIX_SIZE ]; std::copy( matrix, matrix + MATRIX_SIZE, matrix1 ); matrix1[ i ] = 1; for( unsigned int j = dimension_; j < 2 * dimension_; j++ ) { if( !matrix1[ j - dimension_ ] ) { int * matrix2 = new int[ MATRIX_SIZE ]; std::copy( matrix1, matrix1 + MATRIX_SIZE, matrix2 ); matrix2[ j ] = 1; unsigned int NUMBER = 1 << dimension_; for( unsigned int l = 0; l < NUMBER; l++ ) { int * matrix3 = new int[ MATRIX_SIZE ]; std::copy( matrix2, matrix2 + MATRIX_SIZE, matrix3 ); if( l & 1 ) { for( unsigned int l1 = 0; l1 < dimension_; l1++ ) { matrix3[ l1 ] = -matrix3[ l1 ]; } } if( l & 2 ) { for( unsigned int l1 = dimension_; l1 < 2 * dimension_; l1++ ) { matrix3[ l1 ] = -matrix3[ l1 ]; } } Orientation * orientation = new Orientation( figure ); for( std::vector<Point *>::const_iterator h = figure->points().begin(); h != figure->points().end(); ++h ) { const Point * p = *h; int x = 0; for( unsigned int i1 = 0; i1 < dimension_; i1++ ) { x = x + p->coord( i1 ) * matrix3[ i1 ]; } int y = 0; for( unsigned int i1 = 0; i1 < dimension_; i1++ ) { y = y + p->coord( i1 ) * matrix3[ dimension_ + i1 ]; } Point p1( x, y ); orientation->createPoint( p1.coord( 0 ), p1.coord( 1 ) ); } orientation->moveToOrigin(); if( isUnique( orientations, orientation ) ) { orientations.push_back( orientation ); } else { delete orientation; } delete [] matrix3; } delete [] matrix2; } } delete [] matrix1; }
This code is applied to each of the figures, and then, the resulting unique Orientation are shifted along the x and y axes creating all possible positions of each figure. As a result, we have the following number of different positions for each of the figures:
---------- Figure 1
Count = 288
---------- Figure 2
Count = 64
---------- Figure 3
Count = 280
---------- Figure 4
Count = 280
---------- Figure 5
Count = 336
---------- Figure 6
Count = 144
---------- Figure 7
Count = 168
---------- Figure 8
Count = 144
---------- Figure 9
Count = 144
---------- Figure a
Count = 36
---------- Figure b
Count = 280
---------- Figure c
Count = 144
---------- Figure d
Count = 49
Then we assign a Boolean variable to each possible position and create a formula as described above. After that, we call minisat directly from the application, which returns a solution - a set of our variables with assigned values of true or false. Knowing which positions were assigned these variables, we print the solution:
bbbb 3 3 3 3
ddbc 8 8 8 3
dd 1 ccc 8 2
5 5 1 1 1 c 8 2
5 5 5 1 4 4 4 2
7 7 a 4 4 9 6 2
7 aaa 9 9 6 2
7 7 a 9 9 6 6 6
What's next
Naturally, it would not be so interesting to dwell on this. Therefore, the first question I had was this: “But how many different solutions exist that do not differ in trivial turns and reflections of the playing field?”. To do this, there is a mode in the SAT Solver that allows you to add clauses without losing existing information, which significantly speeds up the process compared to if a solution was sought from scratch. The next solution can be found by adding a clause that contains the negatives of all the variables present in the previous solution. After adding this procedure and comparing the new solution with the previous ones, taking into account the turns and reflections of the playing field, I received 1364 different options.
Another interesting extension that I implemented was the study of various other forms of the playing field and figures. And, finally, the study of three-dimensional playing fields was very interesting. But this is a topic for another article.
Update
After adding an additional condition: for each piece of one clause - in the playing field there must be at least one position of this piece, the calculation has become much faster. In addition, one bug was fixed, as a result of which the number of all possible unique options is 16146.
All Articles