The Hat, the Spectre and SAT Solvers (2024)
11 comments
·June 13, 2025CliffStoll
kurthr
Interestingly, when firing your own, you could also make Supertiles from combinatorial collections of Penrose or other aperiodic tiles.
gus_massa
Do you have some photos? It may be a nice post.
nhatcher
Hey, thanks! Good luck with your Penrose tiles. I wish I had the time myself :)
blobcode
I feel like SAT solvers and the like are getting a lot more attention on HN recently (for example https://news.ycombinator.com/item?id=44259476) - justifiably so! I think that they're a great tool that's often criminally underused in industry for a whole subset of problems.
staunton
> a whole subset of problems
Like what?
In my experience, 95% of the times I'm considering applying SAT/SMT to a problem, I should actually think about it for another day (perhaps while throwing a SAT solver at it, if that seems fun) and will invariably find that the problem I'm trying to solve is actually something else... In the remaining 5% of problems, there's usually a solution you can download (which maybe uses SMT under the hood).
Sure enough, SMT is really cool and extremely powerful where it's applicable.
LegionMammal978
It's occasionally helped me with the NP-hard problem of "finding a regular language consistent with a set of samples that also satisfies some structural constraints". But more often, the minimal DFA (when it exists) has a few dozen too many states, and the solver gets trapped in the exponential pit of despair, which hasn't really endeared me to the approach. I've yet to actually run into a class of problems where things like SAT or ILP are wildly successful while all other approaches fail.
akoboldfrying
Interesting article! I'm stuck on the following claim about tiling Hats though:
> In each center of an hexagon you can have any of the 12 possibilities:
> Any of the 6 rotations of the Hat
> Any of the 6 rotations of the anti-Hat
For this claim to hold, it must be the case that a Hat (or anti-Hat) occupies the same area as a hexagon. But they don't: a hexagon is made of 6 kites, while a Hat is made of 8. So, some hexagons must contain no corresponding (anti-)Hat -- specifically, for every 8 hexagons, there must be 6 (anti-)Hats.
This seems to complicate the SAT formulation. But could the fix be as simple as adding a 13th possibility, "No hat at this hexagon centre occupies more than half of its kites"? Or are additional constraints needed?
nhatcher
Oof, that is poorly written. I'll update the text.
Notice how every hat has a special "marked" vertex. It is the red dot in this image:
https://www.nhatcher.com/images/hats/hat-marked.png
This is what I mean by "at the center ofthe hexagon you have the hat". What should say is "the center of the hexagon coincides with the marked vertex of a hat". Hope that makes more sense.
null
curtisszmania
[dead]
Terrific article by Nicolas Hatcher! Aperiodic tilings are fun to make from paper, wood, and ceramics. I've cut tiles from ceramic field tiles.
No surprise that concave cuts in ceramics are a high stress, so Kite and Dart tiles don't work very well (the dart is likely to crack). Same is true for the Turtle, Hat, and Spectre.
Rhombus tiles are everywhere convex, and the P3 Rhombus tiles are easy to cut in a diamond saw (or even a snap-cutter). With a diamond band-saw, it's possible to make Penrose rhombs with curved (parabolic) edges.
But cutting tiles from stock field tiles produces sharp surface edges -- you don't want these as bathroom floor tiles. Also, you waste a lot of the field tile as scrap. To get "friendly" tile shoulders, I'm experimenting with making Penrose tiles directly from high-fired porcelain clay.