The Hat, the Spectre and SAT Solvers (2024) | Hacker News Reader

The Hat, the Spectre and SAT Solvers (2024)

nhatcher.com

108 pointstodsacerdoti12 comments

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.

Hey, thanks! Good luck with your Penrose tiles. I wish I had the time myself :)

Do you have some photos? It may be a nice post.

Interestingly, when firing your own, you could also make Supertiles from combinatorial collections of Penrose or other aperiodic tiles.

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.

> 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.

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.

You are not wrong. But I can wear both hats (no pun intended, I think).

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

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?

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.

Thanks for responding, but this doesn't address the issue. It still cannot be the case that some hat's marked vertex coincides with each hexagon centre -- since that would imply that (in a region large enough that boundary effects can be ignored) there are at least as many hats as there are hexagons, and since hats and hexagons each tile the plane, this would imply that a hat has size less than or equal to the size of a hexagon, which is not true. (As an aside, observing that the marked vertex has an internal angle of over 180 degrees for the hat lets us additionally conclude that at most one hat's marked vertex coincides with each hexagon centre, meaning that if your claim were true then any large enough region would be covered by exactly the same number of hats as hexagons (and they would be forced to have exactly the same size), but this doesn't help make the original claim hold.)

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".

Oh, I don't think I understood you at all the first time around.

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

Reply on news.ycombinator.com