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

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)
/Files/2021/y_polymino_15_by_15.png

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)
/Files/2021/tiling_20_by_20_with_y_polyomino_glucose.png

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.

blog comments powered by Disqus