The Domino Problem Is Decidable for Robust Tilesets

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. The problem is known to be undecidable in general. 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 by provably satisfying some particular invariant. We establish that several famous tilesets considered in the literature are robust. We give arguments 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, relatively complete method for proving that a tileset can tile the plane. Our analysis also provides explanations for the 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.