Have you seen these harmless tiles around the site? Keep reading!
Introduction
This story begins in 2019 while I was doing my third year at the university, there was a subject called computing fundamentals, at that point, I only knew Big-O algorithm’s complexity from Algorithms and Data Structures classes. The subject was mainly theory of computation, from automata theory to computational complexity. Those classes were a truly wonderful experience from the beginning, not only by the clearly presented good ideas, also the format, I’ve always preferred blackboard over projector.
The assignments were practical exercices. Today’s story is based on the first one, it consisted on solving a slight variation of the Tiling Problem. This assignment was made in teams of 3 and there was a competition for the fastest implementation, the prize was an extra point for all the members of the winning team. I promise you that I will tell you who won, but first let me introduce you the Tiling Problem and Wang Tiles. :)
Wang Tiles and Tiling Problem
Wang Tiles, invented by Hao Wang in 1961, are squares that have a color on each side. The problem is deciding whether there exists a tiling of the plane given a set of tiles. There is one caveat, Wang Tiles can only placed in one position if adjacent tiles have the same color on the shared edge.
Valid placing of tiles filling a 2x5 rectangle
The plane is infinite, but at first glance the problem seems easy, one may be tempted to think that if it’s possible, there will be a recognizable pattern that allows to fill the plane using some sort of copies.
It turns out that this problem is hard, as hard as it can be, in fact, it’s undecidable. This means that in general it’s impossible to know if a set of tiles can be used to tile the whole plane. Not all sets of tiles that tile the plane, do it periodically or with patterns, for instance the following tiles can tile the plane, but the solution is aperiodic.
Smallest aperiodic set of tiles that can tile the plane discovered by Emmanuel Jeandel and Michael Rao
The assignment 📝
The version that we analyzed in the assignment was a bit different, the question was not if it’s possible to tile the whole plane, but if it is possible to tile a region of dimensions n x m. This little change makes the problem extremely easy, now it’s decidible as the number of combinations is finite. This problem is now in NP, given a solution it can be checked just looking at the edges of adjacent tiles.
The goal was to create a program that solves it and returns the solution if it exists.
Our approach and Competition 🏁
“When I wrote this, only God and I understood what I was doing. Now, God only knows.”
Our program was a complete bruteforce low-level mess of arrays and indices. The algorithm was pretty naive, it began adding tiles in order from the top left to the bottom right, row by row, until it reached a dead-end and no more tiles could be inserted, then it would backtrack to fix the conflict and try again with another tile. Our program was guaranteed to get the solution if the instance was feasible, as the fix of the conflict was done without discarding any solution. It was really fast, specially for feasible instances. We won the class competition 🥇 but I had a feeling that it could be done faster.
Clause by clause
Simplicity is a great virtue but it requires hard work to achieve it and education to appreciate it. And to make matters worse: complexity sells better. — Edsger W. Dijkstra
The course ended as everything in life, but the hours spent programming and debugging Wang Tiles’ problem made me appreciate the idea. However, I eventually abandoned the idea of improving the program because it was a mess. The following semester we did paradigms and programming languages, one task was to solve the Sudoku problem using Haskell and a reduction to SAT. The task was divided in two parts, the first was to represent sudoku as an SAT instance, and the second one was to implement a naive SAT solver to get the solution using Haskell. It worked! We had a sudoku solver, but it took a few seconds for the instances to be solved, which was a bit disappointing, as most online sites could do it on the fly.
I don’t remember exactly how I discovered MiniSAT, but I downloaded it and instead of using our SAT solver, I modified the program to output the clausules in CNF and fed them to Minisat. Minisat finished right away, it wasn’t my mistake, taking the output and converting the variables to the sudoku instance the solution was perfectly fine.
🤯
Is this an NP oracle?
Turns out that state-of-the-art SAT solvers are extremely fast and underused.
From Tiles to SAT and back
If the only tool you have is a hammer, it is tempting to treat everything as if it were a nail — Abraham Maslow
I automatically thought about the Tiles problem, the reduction we used for Sudoku could be adapted to work with the Tiles problem. Both consist on placing things in a grid under some constraints. The goal in Sudoku is to place numbers and in the Tiles to place tiles. The constraints are easy to adapt so the Tile’s rules are not broken.
The result was extremely SATisfying! The messy program was completely overtaken by MiniSAT. Not only from a runtime perspective, the solution is much nicer and allows, for intance, to fix a set of tiles just adding constraints. I’m sorry not to be able to put here the results, but I promise you it was orders of magnitude faster.
This is how I fell in love with SAT solvers.