当数学遇上计算机科学，往往会激荡出令人耳目一新的研究成果。2023年，一位业余数学爱好者大卫·史密斯发现了一种名为“哈特”（Hat）的单形瓷砖，其一项令人震惊的性质是能够以非周期方式铺满整个无限平面。这一突破性的发现不仅引发学术界的关注，也迅速在网络上走红，成为众多科学传播平台如Veritasium、Numberphile以及《纽约时报》等竞相报道的热点话题。非周期铺瓷问题本身有着深厚的历史，寻根溯源可以追溯到罗杰·彭罗斯爵士和马丁·加德纳的经典工作，彭罗斯曾发现了以两种特殊瓷砖——飞镖（Dart）和风筝（Kite）组成的非周期铺瓷。他们的研究奠定了现代铺瓷理论的重要基础，而哈特的发现则实现了多年来“单一瓷砖非周期铺满平面”的梦想，堪称“爱因斯坦铺瓷问题”的里程碑。哈特瓷砖是由八个“风筝形”小块拼接而成，这种结构使它具有独特的几何对称性和旋转变换特性。
与传统的多块瓷砖非周期铺瓷不同，哈特只需一种形状（包括其镜像的“反哈特”）即可实现这一非周期展开。由于其顶点坐落于规则的六边形蜂窝格点上，哈特瓷砖的研究不仅限于几何学领域，更涉及组合数学和计算机算法问题。如何有效地在有限区域内铺满哈特瓷砖，成为理论与实践结合的挑战。正是在此，SAT求解器——一种解决布尔可满足性问题的强大计算工具——显示出独特的应用潜力。SAT求解器可以处理成千上万个变量和数百万条件的逻辑公式，其技术核心在于将复杂的布尔表达式转化为标准的合取范式（CNF）后进行求解。通过适当编码铺瓷问题的规则，例如每个蜂窝格点只能放置一种瓷砖变换版本，两瓷砖间不能重叠且必须覆盖所有的局部单元，SAT求解器能够自动搜索出符合条件的瓷砖排列方案。
本文作者尼古拉斯·哈彻利用强大且开源的splr SAT求解器，通过WebAssembly技术将其运行于浏览器中，实现了对哈特及其变形瓷砖的交互式探索。他进一步通过示例向读者展示了如何将经典的数独问题转化为SAT问题并求解，为理解SAT求解器应用提供生动体验。真正将SAT求解器应用于铺瓷领域的关键改革，是通过将哈特的拓扑结构和几何约束精确编码进变量与子句之中，紧密结合数学理论与算法工程。SAT求解器的高效性能不仅让有限区域的铺瓷求解成为可能，而且为后续研究诸如Heesch数（在铺瓷中形状可被包围的最大层数）提供了计算支持。哈特的研究并未止步于其自身，探索团队发现了其家族形态中的又一成员——“乌龟”（Turtle）。乌龟瓷砖与哈特类似，同样能够实现非周期铺满，但其边长比例不同。
更有趣的是，哈特和乌龟是同一系列的多变形瓷砖家族中的代表，称为Tile(a, b)系列，其中a和b分别决定了瓷砖边的长度。相关研究展示了Tile(1, √3)对应哈特，Tile(√3, 1)是乌龟。这个家族的漂亮之处在于，可以将哈特与乌龟混合搭配完成整个平面的非周期铺瓷，拓展了铺瓷形状和规律的多样性。这些瓷砖的变换和组合，不仅丰富了铺瓷艺术，也为理论研究带来了新的视角。进一步推进铺瓷理论的是“幽灵”（Spectre）单形的出现。该瓷砖最初被称为Tile(1,1)，其独特之处在于，它是一种真正的单形，实现了非周期铺瓷，而不需要其镜像反单形的参与。
幽灵单形突破了哈特和乌龟瓷砖依赖蜂窝格点定位的限制，其不再构成正六边形网格中的多风筝形组合，而更多地具有复杂的边界形态。幽灵的结构体现出拓扑和组合学上的精妙对偶关系，其与哈特-乌龟体系之间存在双射的组合等价性，反映了铺瓷图案的深层对称关系。换言之，任何由幽灵铺满的区域都可以通过变形映射对应到由哈特和乌龟铺满的组合图案，进而借助SAT求解器间接处理幽灵单形的铺瓷问题。幽灵单形的研究不仅解决了“单形非周期铺瓷”的长久难题，也促进了数学、计算机科学与艺术的融合创新。研究团队基于严谨的几何变换和调和分析，探讨了幽灵及其镜像反单形的周期性与非周期性条件，揭示了非周期铺瓷的生成机理。对于广大爱好者和科研人员，作者设计并开放了基于浏览器的互动App，支持用户在六角格点网格上放置各种组合的哈特、反哈特、乌龟、反乌龟及幽灵瓷砖。
应用还集成了SAT求解器，能自动完成大规模区域的非周期铺瓷，供研究、教学与娱乐互动使用。用户可以通过键盘快捷键实现新增、旋转及切换瓷砖类型，实时观察铺瓷结果。软件充分利用了现代计算机的高效计算力，支持百万级子句的布尔逻辑求解，实测在主流笔记本或手机上即可快速响应。铺瓷问题以SAT形式表达的成功，不仅扩展了数学领域的应用边界，也验证了SAT求解器这一工具在广泛领域的适用性。通过合理建模，SAT求解器可以帮助解决诸如数独、拼图、硬件验证以及复杂图形铺设等多种难题，是编程与数学爱好者不可或缺的利器。总结而言，哈特、乌龟和幽灵的铺瓷故事，以其深厚的数学背景和前沿的计算机技术交汇为轴心，构建了一个关于非周期几何拼贴的壮丽图景。
通过巧妙地利用SAT求解器，科学家得以在有限范围内探索铺瓷模式的可能性，验证复杂结构的存在性，为数学征程添上浓墨重彩的一笔。未来，随着算法优化和计算能力的提升，这一领域必将持续涌现新的惊喜，也期待更多学者与爱好者参与其中，推动非周期铺瓷这门古老又年轻的学科不断前行。
