论文标题
使用移位模式避免单色矩形
Avoiding Monochromatic Rectangles Using Shift Patterns
论文作者
论文摘要
拉姆西理论涉及避免某些模式。当构建一个避免一种模式的实例时，可以观察到其他模式出现。例如，在避免算术进程（van der waerden数字）时会出现重复，而在避免$ a+b = c $（schur数字）的单色溶液时会出现反射。在避免单色矩形的同时，我们在涂上彩色时，利用观察到的图案。像拉姆齐理论中的许多问题一样，这个问题具有迅速增长的搜索空间，使计算机搜索变得困难。 Steinbach等。通过执行旋转对称性，获得了18乘18个网格的溶液。但是，这种对称不适合5种颜色。 在本文中，我们将将此问题编码为命题逻辑，并强制执行所谓的内部对称性，从而确保令人满意，以指导SAT解决。我们首先观察具有2种和3种颜色的模式，其中“移位模式”可以很容易地概括且有效地编码。使用这种模式，我们获得了18 x 18网格的新解，该解决方案对已知溶液是非同构的。我们进一步分析模式并获得必要的条件，以进一步修剪搜索空间。最后，我们试图找到5色的26 x 26网格，以及在换档模式上进一步的开放问题。
Ramsey Theory deals with avoiding certain patterns. When constructing an instance that avoids one pattern, it is observed that other patterns emerge. For example, repetition emerges when avoiding arithmetic progression (Van der Waerden numbers), while reflection emerges when avoiding monochromatic solutions of $a+b=c$ (Schur numbers). We exploit observed patterns when coloring a grid while avoiding monochromatic rectangles. Like many problems in Ramsey Theory, this problem has a rapidly growing search space that makes computer search difficult. Steinbach et al. obtained a solution of an 18 by 18 grid with 4 colors by enforcing a rotation symmetry. However, that symmetry is not suitable for 5 colors. In this article, we will encode this problem into propositional logic and enforce so-called internal symmetries, which preserves satisfiability, to guide SAT-solving. We first observe patterns with 2 and 3 colors, among which the "shift pattern" can be easily generalized and efficiently encoded. Using this pattern, we obtain a new solution of the 18 by 18 grid that is non-isomorphic to the known solution. We further analyze the pattern and obtain necessary conditions to further trim down the search space. We conclude with our attempts on finding a 5-coloring of a 26 by 26 grid, as well as further open problems on the shift pattern.
