Решение задачи замощения с помощью SAT солвера на примере пентамино

Однажды попалась мне игра пентамино, где было необходимо уложить 13 фигурок в квадрат 8 на 8. После некоторого периода времени, втечение которого я безуспешно пытался решить эту задачу, я решил, что необходимо написать программу, которая бы делала это за меня. Для этого необходимо было выбрать алгоритм решения. Первое, что приходит на ум — это обычный алгоритм ветвей и границ, когда фигурки укладываются одна за другой примыкая друг к другу (алгоритм с танцующими ссылками здесь не подходит, поскольку фигурки разные). Для ускорения этого алгоритма обычно используются различные эвристики, например, предпочтение отдается ветвлению с наименьшим количеством вариантов. Можно придумать и реализовать и другие эвристики в этом алгоритме, но тут я подумал, что множество различных ухищрений для ускорения решения подобных задач уже реализовано в SAT солверах. Поэтому, необходимо перевести задачу на соответствующий математический язык и воспользоваться каким-либа SAT солвером. О том, как это было реализовано и какие получились результаты можно почитать под катом.

В начале хочу напомнить, что из себя представляет игра пентамино. Это квадратное 8х8 поле, которое надо замостить 13-ю фигурами — 12-ю загогулинами, котороые состоят из 5 квадратиков и одной фигуры 2х2:

Здесь стоит сказать, что такое задача выполнимости булевых формул (Boolean satisfiability problem) или задача SAT. В общем виде ее можно сформулировать как нахожнение таких значений булевых переменных при которых заданное выражение становится истинным. Вообще говоря, это NP полная задача, однако существует множество приемов, которые помогают эффективно ее решить. Для этого разработано много специальных приложений, называемых SAT солверами. Я буду пользоваться SAT солвером по имени minisat. Для решения этой задачи необходимо переписать входное выражение в конъюнктивной нормальной форме, то есть в виде произведения логических сумм переменных. Каждая скобка в конъюнктивной нормальной форме здесь называется клозом (clause), который является логическим «или» некоторых литералов, то есть булевых переменных или их отричаний. Например:

(x1 V not x3)(x2 V x4)(x2 V x3 V not X4)

Мне было необходимо перевести задачу замощения в задачу SAT. Возьмем какую-нибудь фигуру из пентамино и уложим ее в игровое поле всеми возможными способами, включая сдвиги, повороты и отражения. Каждой такой позиции фигуры сопоставим булеву переменную и будем считать, что если у нас в окончательном решении эта фигура будет присутствовать в данной конкретной позиции, то переменная будет равна true, а если не будет, то false. Проделаем это для всех фигур.

Теперь составим формулу, описывающую нашу задачу, то есть фактически наложим ограничения на наши переменные. Первое, что необходимо сделать, это гарантировать, что все клетки нашего игрового поля будут покрыты хотя бы одной фигурой. Для этого для каждой клетке из 64 найдем все фигуры и позиции этих фигур, которые покрывают данную клетку и составим клоз из переменных, которые присвоены этим позициям фигур. Второе, что необходимо сделать — это исключить пересечения фигур. Это можно сделать в двойном цикле, просто перебирая все возможные позиции всех фигур и определяя, есть ли у пары общие клетки. Если есть, значит они пересекаются и необходимо добавить клоз вида (not x_i V not x_j), где x_i — переменная присвоеная первой позиции, а x_j — второй позиции. Этот клоз истинен тогда, когда x_i и x_j не равны одновременно единице, то есть исключает пересечения. И, наконец, третье, что необходимо учесть — это то, что кажная фигура может присутствовать на игровом поле только один раз. Для этого также в двойном цикле проходим по всем позициям каждой фигуры и для каждой пары позиций одной и той же фигуры делаем клоз, похожий на предыдущий и состоящий из двух отрицаний. То есть при появлении двух одинаковых фигур (но в разных позициях) один из таких клозов даст false и, соответственно, исключит такое решение.

Это все была теория, а теперь перейдем к практике. Прсвоим каждой фигуре номер от 1 до d, чтобы отличать ее от других и удобно выводить на печать. Затем создадим матрицу игрового поля и закодируем соответствующие клетки игрового поля как занятые/не занятые фигурой:

. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. 1 1 . . . . .
1 1 . . . . . .
. 1 . . . . . .

. . . . . . . .
. . . . . . . .
. . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .

. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
d d . . . . . .
d d . . . . . .


Теперь для каждой фигуры необходимо найти все возможные позиции на игровом поле путем сдвигов, поворотов и отражений. Начнем с поворотов и отражений. Всего существует 8 возможных преобразований поворотов и отражений, включая одно тривиальное преобразование, оставляющее фигуру нетронутой. Для этих преобразований я создаю 8 соответствующих матриц, как показано ниже. После поворота или отражения фигура может выйти за пределы игрового поля, поэтому необходимо вернуть ее обратно на игровое поле. Следует также учесть, что некоторые фигуры после преобразования могут переходить сами в себя и такие случаи надо исключить. Уникальные варианты я складываю в класс Orientation. В итоге получается следующий код:

    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;
    }

Этот код применяется к каждой из фигур, а затем, полученные уникальные Orientation сдвигаются по оси x и y создавая все возможные позиции кажной фигуры. В результате имеем следующее количество различных позиций для каждой из фигур:

---------- 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


Затем присваиваем каждой возможной позиции булеву переменную и создаем формулу, как это было описано выше. После этого вызываем minisat непосредственно из приложения, который возвращает решение — набор наших переменных с присвоенными значениями true или false. Зная, каким позициям были присвоены эти переменные, печатаем решение:

b b b b 3 3 3 3
d d b c 8 8 8 3
d d 1 c c c 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 a a a 9 9 6 2
7 7 a 9 9 6 6 6


Что дальше

Естественно, что останавливаться на этом было бы не так интересно. Поэтому, первый вопрос, который у меня возник, был такой — «а сколько всего существует различных решений, которые не отличаются тривиальными поворотами и отражениями игрового поля ?». Для этого в SAT солвере существует режим, который позволяет добавлять клозы не теряя при этом существующую информацию, что существенно ускоряет процесс по сравнению с тем, как если бы решение искалось с чистого листа. Следующее решение может быть найдено путем добавления клоза, который содержит отрицания всех переменных, присутствующих в предыдущем решении. После добавления этой процедуры и сравнения нового решения с предыдущими с учетом поворотов и отражений игрового поля, я получил 1364 различных вариантов.

Еще одним интересным расширением, которое я реализовал было исследование различных других форм игрового поля и фигур. И, наконец, очень интересным было исследование трехмерных игровых полей. Но это уже тема для другой статьи.

Автор: Андрей Плеханов

Источник