4 ms·

Jim's blog post about his discovery is also delightful to read: https://hedraweb.wordpress.com/2023/03/23/its-a-shape-jim-but-not-as-we-know-it/ https://hedrawe

Jim's blog post about his discovery is also delightful to read: https://hedraweb.wordpress.com/2023/03/23/its-a-shape-jim-but-not-as-we-know-it/ https://hedraweb.wordpress.com/2023/03/23/its-a-shape-jim-bu... His offhand mention of "Craig's SAT Solver" opened a rabbit hole for me. I put together a blog post on how to draw the tiling without knowing the recursive structure by just feeding the shape into z3: https://www.hgreer.com/HatTile/ https://www.hgreer.com/HatTile/

NooneAtAll3 3y ago
> using a SAT solver (in this case, Z3) isn't z3 SMT solver, not SAT?
- nhatcher 3y ago
  Z3 has both, but the tool they are using is the SAT solver.
nhatcher 3y ago
Hi @QuadmasterXLII, you linked my blog in yours! Thanks, I feel honored! I found your blog halfway going through my own rabbit whole. I think had I seen it before embarking into the project I would have just use yours. That being said it is been a fun ride. It's interesting that we both got triggered by "Craig's SAT solver". Thanks again, Nicolás