## Using Glucose SAT solver to find a tiling of a rectangle by polyominoes

27 mai 2021 | Mise à jour: 20 juin 2022 | Catégories: sage, math | View Comments

In his Dancing links article, Donald Knuth considered the problem of packing 45 Y pentaminoes into a 15 x 15 square. We can redo this computation in SageMath using some implementation of his dancing links algorithm.

Dancing links takes 1.24 seconds to find a solution:

sage: from sage.combinat.tiling import Polyomino, TilingSolver sage: y = Polyomino([(0,0),(1,0),(2,0),(3,0),(2,1)]) sage: T = TilingSolver([y], box=(15, 15), reusable=True, reflection=True) sage: %time solution = next(T.solve()) CPU times: user 1.23 s, sys: 11.9 ms, total: 1.24 s Wall time: 1.24 s

The first solution found is:

sage: sum(T.row_to_polyomino(row_number).show2d() for row_number in solution)

What is nice about dancing links algorithm is that it can list all solutions to a problem. For example, it takes less than 3 minutes to find all solutions of tiling a 15 x 15 rectangle with the Y polyomino:

sage: %time T.number_of_solutions() CPU times: user 2min 46s, sys: 3.46 ms, total: 2min 46s Wall time: 2min 46s 1696

It takes more time (38s) to find a first solution of a larger 20 x 20 rectangle:

sage: T = TilingSolver([y], box=(20,20), reusable=True, reflection=True) sage: %time solution = next(T.solve()) CPU times: user 38.2 s, sys: 7.88 ms, total: 38.2 s Wall time: 38.2 s

The polyomino tiling problem is reduced to an instance of the universal cover problem which is represented by a sparse matrix of 0 and 1:

sage: dlx = T.dlx_solver() sage: dlx Dancing links solver for 400 columns and 2584 rows

We observe that finding a solution to this problem takes the same amount of
time. This is normal since it is exactly what is used behind the scene when
calling `next(T.solve())` above:

sage: %time sol = dlx.one_solution(ncpus=1) CPU times: user 38.6 s, sys: 48 ms, total: 38.6 s Wall time: 38.5 s

One way to improve the time it takes it to split the problem into parts and use many processors to work on each subproblems. Here a random column is used to split the problem which may affect the time it takes. Sometimes a good column is chosen and it works great as below, but sometimes it does not:

sage: %time sol = dlx.one_solution(ncpus=2) CPU times: user 941 µs, sys: 32 ms, total: 32.9 ms Wall time: 1.41 s

The reduction from dancing links instance to SAT instance #29338 and to MILP instance #29955 was merged into SageMath 9.2 during the last year. A discussion with Franco Saliola motivated me to implement these translations since he was also searching for faster way to solve dancing links problems. Indeed some problems are solved faster with other kind of solver, so it is good to make some comparisons between solvers.

Therefore, with a recent enough version of SageMath, we can now try to find a tiling with other kinds of solvers. Following my experience with tilings by Wang tiles, I know that Glucose SAT solver is quite efficient to solve tilings of the plane. This is why I test this one below. Glucose is now an optional package to SageMath which can be installed with:

sage -i glucose

Update (June 20th, 2022): It seems `sage -i glucose` no longer works. The new
procedure is to use `./configure --enable-glucose` when installation is made
from source. See the question Unable to install glucose SAT solver with
Sage on ask.sagemath.org for more information.

Glucose finds the solution of a 20 x 20 rectangle in 1.5 seconds:

sage: %time sol = dlx.one_solution_using_sat_solver('glucose') CPU times: user 306 ms, sys: 12.1 ms, total: 319 ms Wall time: 1.51 s

The rows of the solution found by Glucose are:

sage: sol [0, 15, 19, 38, 74, 245, 270, 310, 320, 327, 332, 366, 419, 557, 582, 613, 660, 665, 686, 699, 707, 760, 772, 774, 781, 802, 814, 816, 847, 855, 876, 905, 1025, 1070, 1081, 1092, 1148, 1165, 1249, 1273, 1283, 1299, 1354, 1516, 1549, 1599, 1609, 1627, 1633, 1650, 1717, 1728, 1739, 1773, 1795, 1891, 1908, 1918, 1995, 2004, 2016, 2029, 2037, 2090, 2102, 2104, 2111, 2132, 2144, 2146, 2185, 2235, 2301, 2460, 2472, 2498, 2538, 2548, 2573, 2583]

Each row correspond to a Y polyomino embedded in the plane in a certain position:

sage: sum(T.row_to_polyomino(row_number).show2d() for row_number in sol)

Glucose-Syrup (a parallelized version of Glucose) takes about the same time (1 second) to find a tiling of a 20 x 20 rectangle:

sage: T = TilingSolver([y], box=(20, 20), reusable=True, reflection=True) sage: dlx = T.dlx_solver() sage: dlx Dancing links solver for 400 columns and 2584 rows sage: %time sol = dlx.one_solution_using_sat_solver('glucose-syrup') CPU times: user 285 ms, sys: 20 ms, total: 305 ms Wall time: 1.09 s

Searching for a tiling of a 30 x 30 rectangle, Glucose takes 40s and
Glucose-Syrup takes 16s while dancing links algorithm takes much longer
(`next(T.solve())` which is using dancing links algorithm does not halt in
less than 5 minutes):

sage: T = TilingSolver([y], box=(30,30), reusable=True, reflection=True) sage: dlx = T.dlx_solver() sage: dlx Dancing links solver for 900 columns and 6264 rows sage: %time sol = dlx.one_solution_using_sat_solver('glucose') CPU times: user 708 ms, sys: 36 ms, total: 744 ms Wall time: 40.5 s sage: %time sol = dlx.one_solution_using_sat_solver('glucose-syrup') CPU times: user 754 ms, sys: 39.1 ms, total: 793 ms Wall time: 16.1 s

Searching for a tiling of a 35 x 35 rectangle, Glucose takes 2min 5s and Glucose-Syrup takes 1min 16s:

sage: T = TilingSolver([y], box=(35, 35), reusable=True, reflection=True) sage: dlx = T.dlx_solver() sage: dlx Dancing links solver for 1225 columns and 8704 rows sage: %time sol = dlx.one_solution_using_sat_solver('glucose') CPU times: user 1.07 s, sys: 47.9 ms, total: 1.12 s Wall time: 2min 5s sage: %time sol = dlx.one_solution_using_sat_solver('glucose-syrup') CPU times: user 1.06 s, sys: 24 ms, total: 1.09 s Wall time: 1min 16s

Here are the info of the computer used for the above timings (a 4 years old laptop runing Ubuntu 20.04):

$ lscpu Architecture : x86_64 Mode(s) opératoire(s) des processeurs : 32-bit, 64-bit Boutisme : Little Endian Address size : 39 bits physical, 48 bits virtual Processeur(s) : 8 Liste de processeur(s) en ligne : 0-7 Thread(s) par coeur : 2 Coeur(s) par socket : 4 Socket(s) : 1 Noeud(s) NUMA : 1 Identifiant constructeur : GenuineIntel Famille de processeur : 6 Modèle : 158 Nom de modèle : Intel(R) Core(TM) i7-7820HQ CPU @ 2.90GHz Révision : 9 Vitesse du processeur en MHz : 3549.025 Vitesse maximale du processeur en MHz : 3900,0000 Vitesse minimale du processeur en MHz : 800,0000 BogoMIPS : 5799.77 Virtualisation : VT-x Cache L1d : 128 KiB Cache L1i : 128 KiB Cache L2 : 1 MiB Cache L3 : 8 MiB Noeud NUMA 0 de processeur(s) : 0-7

To finish, I should mention that the implementation of dancing links made in SageMath is not the best one. Indeed, according to what Franco Saliola told me, the dancing links code written by Donald Knuth himself and available on his website (franco added some makefile to compile it more easily) is faster. It would be interesting to confirm this and if possible improves the implementation made in SageMath.