> 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?
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.
It must instead be the case that some hexagon centres do not coincide with any hat's marked vertex, and indeed this is the case -- I've marked out a few with red circles in the first image here: https://imgur.com/a/Kat6oXf
In the second image at that link I've marked two other vertices of a hat in green. It looks to me like the hexagon centres I circled in the first image are incident on one of the green vertices of each of 3 different hats, each contributing "120 degrees of coverage".
But you are absolutely right. The center of an hexagon may or may not coincide with the vetex of a marked hat.
In particular in the set of statements, for a given (m, n) all 12 these might be false:
There is Hat (or an anti-Hat) in vertex (m, n) with rotation 60×i (with i=0,..,5)
I'll update the text when I get a chance
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.
On one hand people are not going to be using SAT/SMT to solve problems on a dayly basis.
On the other hand these algorithms are a bit overlooked in CS books (not Knuth, of course). Compare, for instance with a FFT. In the livetime of an average programmer they might actually find it convenient to use SAT solvers here and there on a few occasions. Maybe just as much as a FFT.
Combinatorics is a hard subject and SAT shed light in many situations where better tailored algorithms might exist but might be difficult to come up with.
Maybe I'm biased
CliffStoll•7mo ago
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.
nhatcher•7mo ago
gus_massa•7mo ago
kurthr•7mo ago