无限方格图的填装色数为 15

填装 $k$-着色是标准图 $k$-着色概念的一种自然变体，其中顶点被赋予来自 $\{1, \ldots, k\}$ 的数字，且任意两个被赋予共同颜色 $c \in \{1, \ldots, k\}$ 的顶点之间的距离必须大于 $c$（而在标准图着色中该距离为 $1$）。尽管有一系列渐进的工作，自 2002 年提出以来，确定无限方格图的填装色数一直是一个开放问题。我们终结了这一探索，证明该数为 15。我们将针对此问题的最佳已知方法提升了约两个数量级，从而取得该结果。提升性能最重要的技术是一种新颖且出奇有效的命题编码。此外，我们开发了一种新的对称性破缺方法。由于这两种新技术比该问题的现有技术更为复杂，需要一种经过验证的方法来信任它们。我们将这两种技术包含在一个不可满足性证明中，将可信核心缩减至直接编码的正确性。