During the last year, I have written a Python module to deal with Wang tiles containing about 4K lines of code including doctests and documentation.
It can be installed like this:
sage -pip install slabbe
It can be used like this:
sage: from slabbe import WangTileSet sage: tiles = [(2,4,2,1), (2,2,2,0), (1,1,3,1), (1,2,3,2), (3,1,3,3), ....: (0,1,3,1), (0,0,0,1), (3,1,0,2), (0,2,1,2), (1,2,1,4), (3,3,1,2)] sage: T0 = WangTileSet([map(str,t) for t in tiles]) sage: T0.tikz(ncolumns=11).pdf()
The module on wang tiles contains a class WangTileSolver which contains three reductions of the Wang tiling problem the first using MILP solvers, the second using SAT solvers and the third using Knuth's dancing links.
Here is one example of a tiling found using the dancing links reduction:
sage: %time tiling = T0.solver(10,10).solve(solver='dancing_links') CPU times: user 36 ms, sys: 12 ms, total: 48 ms Wall time: 65.5 ms sage: tiling.tikz().pdf()
All these reductions now allow me to compare the efficiency of various types of solvers restricted to the Wang tiling type of problems. Here is the list of solvers that I often use.
| Solver | Description |
|---|---|
| 'Gurobi' | MILP solver |
| 'GLPK' | MILP solver |
| 'PPL' | MILP solver |
| 'LP' | a SAT solver using a reduction to LP |
| 'cryptominisat' | SAT solver |
| 'picosat' | SAT solver |
| 'glucose' | SAT solver |
| 'dancing_links' | Knuth's algorihm |
In this recent work on the substitutive structure of Jeandel-Rao tilings, I introduced various Wang tile sets \(T_i\) for \(i\in\{0,1,\dots,12\}\). In this blog post, we will concentrate on the 11 Wang tile set \(T_0\) introduced by Jeandel and Rao as well as \(T_2\) containing 20 tiles and \(T_3\) containing 24 tiles.
Tiling a n x n square
The most natural question to ask is to find valid Wang tilings of \(n\times n\) square with given Wang tiles. Below is the time spent by each mentionned solvers to find a valid tiling of a \(n\times n\) square in less than 10 seconds for each of the three wang tile sets \(T_0\), \(T_2\) and \(T_3\).
/Files/2018/T0_square_tilings.svg /Files/2018/T2_square_tilings.svg /Files/2018/T3_square_tilings.svgWe remark that MILP solvers are slower. Dancing links can solve 20x20 squares with Jeandel Rao tiles \(T_0\) and SAT solvers are performing very well with Glucose being the best as it can find a 55x55 tiling with Jeandel-Rao tiles \(T_0\) in less than 10 seconds.
Finding all dominoes allowing a surrounding of given radius
One thing that is often needed in my research is to enumerate all horizontal and vertical dominoes that allow a given surrounding radius. This is a difficult question in general as deciding if a given tile set admits a tiling of the infinite plane is undecidable. But in some cases, the information we get from the dominoes admitting a surrounding of radius 1, 2, 3 or 4 is enough to conclude that the tiling can be desubstituted for instance. This is why we need to answer this question as fast as possible.
Below is the comparison in the time taken by each solver to compute all vertical and horizontal dominoes allowing a surrounding of radius 1, 2 and 3 (in less than 1000 seconds for each execution).
/Files/2018/T0_dominoes_surrounding.svg /Files/2018/T2_dominoes_surrounding.svg /Files/2018/T3_dominoes_surrounding.svgWhat is surprising at first is that the solvers that performed well in the first \(n\times n\) square experience are not the best in the second experiment computing valid dominoes. Dancing links and the MILP solver Gurobi are now the best algorithms to compute all dominoes. They are followed by picosat and cryptominisat and then glucose.
The source code of the above comparisons
The source code of the above comparison can be found in this Jupyter notebook. Note that it depends on the use of Glucose as a Sage optional package (#26361) and on the most recent development version of slabbe optional Sage Package.
