The Hat, the Spectre and SAT Solvers
Introduction
In this blog post you are going to read about two things:
A new flashy discovery in mathematics: aperiodic tilings of the plane with a single monotile
SAT solvers. A family of not so well known algorithms in computer science
Hopefully by the end of the post you will know a fair amount about the hat, the turtle and the spectres and have another powerful tool under your belt, SAT solvers.
Thus, you can see this post either as an exercise in recreational mathematics or as an invitation to SAT solvers.
The post is organized as follows. We first introduce the Hat and state the main result. Then we define what SAT solvers are. In section 3 we describe how we use the solver in wasm and apply it to the problem of solving a Sudoku problem as a warm up exercise in the next section. In section 5 we explain Craig Kaplan’s idea of how to use SAT solvers to tile finite regions of the plane and apply it to the Hat. Section 6 introduces the Turtle, a second monotile capable of tiling the plane aperiodically. With all those constructions we build the Spectre, from deformations of Hats and Turtles, a true chiral aperiodic monotile. In the last section we explain how to use the app
Code
You can find all the code discussed here in GitHub.
... continue reading