这是一篇关于数学新发现和 SAT 求解器的博客文章，主要内容如下：

• 引言（Introduction）：将介绍数学中的新发现——用单个单调子平铺平面的非周期性平铺，以及计算机科学中不太知名的算法家族 SAT 求解器，希望读者能了解相关知识并掌握 SAT 求解器这一工具，文章结构包括介绍“帽子”和主要结果、定义 SAT 求解器、使用 wasm 中的求解器解决数独问题等。
• 代码（Code）：相关代码可在GitHub找到，还有一些应用程序，如https://www.nhatcher.com/hats/、https://www.nhatcher.com/hats/sudoku.html、https://www.nhatcher.com/hats/sat.html等，使用了shnarazk的dpLR SAT 求解器并将其适配到 wasm 中。
• 帽子：令世界困惑的形状（The Hat: a shape perplexing the world）：2022 年 11 月，退休打印机技术员和业余数学家David Smith)发现了一种能以非周期性方式平铺整个无限平面的形状“帽子”，该发现引发广泛关注，非周期性平铺平面的故事由来已久，本文还将介绍用 SAT 求解器覆盖有限区域的方法。
• SAT 求解器，一种未被充分重视的工具（The SAT solver, an underappreciated tool.）：SAT 求解器是解决布尔代数问题的计算机程序，将问题转换为合取范式（CNF）后，通过给变量赋值，将每个子句表示为数组，输入到求解器中，求解器返回变量的真值情况，可能返回成功的解或“UNSAT”表示无解。
• wasm 中的 SAT 求解器（A SAT Solver in wasm）：介绍了使用spLR SAT 求解器并将其编译为WASM，在浏览器中运行，通过特定的数组格式与求解器交互。
• 间奏曲：使用 SAT 求解器解决数独（Intermezzo: Using a SAT solver to solve Sudokus）：以解决数独问题为例，介绍如何使用 SAT 求解器，定义变量表示数独中的数字位置，创建子句，通过简单代码生成数独的子句，虽然使用 SAT 求解器解决数独可能不是最有效的算法，但展示了其应用。
• 使用 SAT 求解器找到平铺问题的解决方案（Using a SAT solver to find solutions to the tiling problem）：Donald Knuth 在其书中提出用 SAT 求解器解决榻榻米平铺问题，Craig Kaplan 的论文也使用 SAT 求解器解决平铺问题，对于 David Smith 发现的“帽子”形状，将其顶点放置在正六边形网格的中心，通过创建子句将平铺问题转化为 SAT 求解器可处理的形式，还可以通过改变“帽子”的旋转和镜像来创建不同的平铺。
• 一路都是海龟（It’s turtles all the way down）：David Smith 发现另一种能以非周期性方式平铺平面的形状“海龟”，它与“帽子”来自同一家族，通过改变“帽子”的边长可以生成其他平铺形状，“帽子”和“海龟”可以组合平铺平面。
• 幽灵（The spectre）：“帽子”或“海龟”本身不能平铺整个平面，需要“反帽子”或“反海龟”，但“Tile(1, 1)”成员可以在不需要“anti-Tile(1, 1)”的情况下以非周期性方式平铺整个平面，称为“幽灵”，它具有一些不同于“帽子”和“海龟”的特性，通过定理 3.1 可以将“Tile(1, 1)”的平铺与“帽子”和“海龟”的平铺建立一一对应关系，通过在应用程序中手动添加瓷砖和使用 SAT 求解器可以创建有趣的平铺图案。
• 使用帽子应用程序（Using the Hats app）：介绍了帽子应用程序的工具栏、画布和状态栏等，可手动添加瓷砖，选择不同的瓷砖和颜色，使用 SAT 求解器填充剩余区域，还可以绘制“幽灵”等家族成员的平铺图案，注意绘制时要注意一些细节。
• 参考文献（References）：列出了相关的杂志、原始来源、教程和应用程序等的链接。