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

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

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

    image

    Здесь стоит сказать, что такое задача выполнимости булевых формул (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 . . . . . . .

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

    . . . . . . . .
    . . . . . . . .
    . . . . . . . .
    . . . . . . . .
    b . . . . . . .
    b b . . . . . .
    b . . . . . . .
    b . . . . . . .

    . . . . . . . .
    . . . . . . . .
    . . . . . . . .
    . . . . . . . .
    . . . . . . . .
    . c c . . . . .
    . c . . . . . .
    c c . . . . . .

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

    image

    Что дальше


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

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

    Update



    После добавления дополнительного условия: для каждой фигуры одного клоза — в игровом поле должна быть хотя бы одна позиция этой фигуры, расчет стал значительно быстрее. Кроме того, исправлена одна ошибка, вследствии чего количество всех возможных уникальных вариантов равно 16146.
    Поделиться публикацией
    Никаких подозрительных скриптов, только релевантные баннеры. Не релевантные? Пиши на: adv@tmtm.ru с темой «Полундра»

    Зачем оно вам?
    Реклама
    Комментарии 22
    • 0
      это интересно, непонятно только
      1) какой SAT солвер вы использовали?
      2) сколько времени решало?
      • +1

        SAT solver — minisat (есть в статье)
        Решает быстро, точные цифры приведу чуть позже.

      • 0

        На нахождение одного варианта ушло меньше 10 секунд:


        processor: 0
        vendor_id: GenuineIntel
        cpu family: 6
        model: 42
        model name: Intel® Core(TM) i7-2600K CPU @ 3.40GHz


        real 0m9.585s
        user 0m9.548s
        sys 0m0.024s

      • +1

        Возможно, не до конца понял, но, по-моему, 3 изначальных правила (все клетки нашего игрового поля будут покрыты хотя бы одной фигурой, исключить пересечения фигур, кажная фигура может присутствовать на игровом поле только один раз) избыточны: можно, например, 2 и 3 только оставить. Или 1 и 3.

        • +1
          Откровенно говоря маловато формул. Клоз — дизъюнкт.
          • 0

            Нет, недостаточно. Фигура (загогулина) появляется много раз в виде сдвигов, поворотов и отражений. Поэтому, чтобы исключить две или более копии, надо все условия. Иначе, например, можно все поле заполнить фигурой 2х2.

            • 0

              Но ведь этот случай покрывается правилом 3? А правила 1 и 2 становятся эквивалентны друг другу, если удовлетворено 3. Разве нет?

              • 0

                Нет. Первое правило служит для того, чтобы каждая клетка была покрыта хотя бы чем-то (но не гарантирует, что только чем-то одним), второе правило говорит, что то, что покрывает клетки не должно пересекаться (но не гарантирует, что все клетки будут покрыты), и третье правило гарантирует, что в множестве загогулин может существовать только одна загогулина каждого типа (но не гарантирует, что все клетки будут покрыты и что то, чем они покрыты не имеют пересечений).

                • +1
                  Думаю, AntonSt имеет в виду, что если на поле ровно по одному варианту каждой фигуры (3), они не пересекаются (2) и не выходят за границы поля (исходя из особенностей их построения), то они должны покрыть ровно все клетки (поскольку количество покрываемых ими клеток в точности равно размеру поля). Аналогично можно прийти от (1,3) к (2) — фигуры просто не смогут пересекаться, поскольку лишних клеток для образования пересечений у них не останется. Чем-то напоминает принцип Дирихле.
                  • +1

                    Хмм… Пожалуй соглашусь. Надо будет попробовать.

                    • 0

                      Попробовал. Результаты следующие на моем компьютере:


                      processor: 0
                      vendor_id: GenuineIntel
                      cpu family: 6
                      model: 42
                      model name: Intel® Core(TM) i7-2600K CPU @ 3.40GHz


                      Методика, описанная в статье:
                      real 0m9.585s
                      user 0m9.548s
                      sys 0m0.024s


                      Если убрать ограничение на заполнение каждой клетки (1) — не работает (выдает пустое поле).


                      Если убрать условие пересечения (2), работает очень долго, не смог дождаться результата.

                      • 0

                        Понятно, почему не работает вариант при исключении заполнения каждой клетки (1) — булева функция выполняется для 2 и 3 если нет ни одной загогулины на поле.
                        Чтобы это опять работало, надо ставить дополнительное условие, чтобы на поле была хотя бы одна фигура для каждого типа.

            • 0
              Не очень понял, 1364 это количество уникальных вариантов решения?
              • 0

                Да.

                • 0
                  Судя по формулировке задачи для minisat, 1364 это с учетом поворотов и отражений. То есть поворот решения — другое решение. Правильно?
                  • 0
                    Упс, там было написано, что сравнение было отдельно. Сорри.
              • 0
                Немного оффтопа про кпдв: Пентамино конечно красивое, деревянное, но зачем эти сочленения в геометрически целых фигурах? Прямо путают общий контур фигурок. Нет, что бы сделать каждую деталь из одного кусочка древесины, думаю не для силовых нагрузок фигурки рассчитаны, можно было и поперёк волокон древесины некоторые элементы сделать
                • 0
                  пентамино ручной работы — это не тот масштаб и цена.
                  А так — нарезали простых брусков, потом склеили их в фигурки.
                  • 0
                    Даже если говорить о ручной работе… Когда я в детстве делал кубики сома, я просто взял 27 детских кубиков без наклеек (как раз продавался такой набор) и склеил их эпоксидкой. Поверьте, это проще чем вырезать фигурные детали. На кубиках были выжжены какие-то буквы, но с ними даже прикольнее. Когда через пять лет пара кубиков расклеилась, не стал морочиться с эпоксидкой. Просто прибил их гвоздями. Картинка на КДПВ, это головоломка к журналу «Занимательные головоломки». Они на этом типа бизнес делают. Серьёзно хотите, убедить их в том, что делать надо качественнее (и дороже)?
                    • 0
                      Вот так это выглядит

                      В сборе

                  Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.