One of the most fundamental problems in tiling theory is the domino problem: given a set of tiles and tiling rules, decide if there exists a way to tile the plane using copies of tiles and following their rules. The problem is known to be undecidable in general and even for sets of Wang tiles, which are unit square tiles wearing colours on their edges which can be assembled provided they share the same colour on their common edge, as proven by Berger in the 1960s. In this paper, we focus on Wang tilesets. We prove that the domino problem is decidable for robust tilesets, i.e. tilesets that either cannot tile the plane or can but, if so, satisfy some particular invariant provably. We establish that several famous tilesets considered in the literature are robust. We give arguments that this is true for all tilesets unless they are produced from non-robust Turing machines: a Turing machine is said to be non-robust if it does not halt and furthermore does so non-provably. As a side effect of our work, we provide a sound and relatively complete method for proving that a tileset can tile the plane. Our analysis also provides explanations for the observed similarities between proofs in the literature for various tilesets, as well as of phenomena that have been observed experimentally in the systematic study of tilesets using computer methods.

翻译：摘要：图块理论中最基本的问题之一是组合问题：给定一组图块及其拼接规则，判断是否存在一种方式，通过使用这些图块的副本并遵循其规则来铺满整个平面。该问题已知在一般情况下是不可判定的，即便对于王图块集（Wang tilesets）也是如此。王图块是单位正方形图块，其边缘带有颜色，仅当相邻图块共享相同颜色时才能拼接，这一性质由伯格（Berger）在20世纪60年代证明。本文聚焦于王图块集，证明了对于鲁棒图块集，组合问题是可判定的。鲁棒图块集是指要么无法铺满平面，要么能够铺满但满足某种可证明不变量的图块集。我们建立了几种文献中著名图块集的鲁棒性，并提出论证，认为所有图块集均具备此性质，除非它们由非鲁棒图灵机生成：若一台图灵机不停机且其不停机性质不可证明，则称其为非鲁棒的。作为本工作的副产品，我们提供了一种可靠且相对完备的方法，用于证明图块集能否铺满平面。我们的分析还解释了文献中不同图块集证明之间观察到的相似性，以及通过计算机方法系统研究图块集时实验观测到的现象。