SAT-solving a grid of tiles

[Tom Sirgedas]

radius 3

radius 5

radius 7

radius 8

6-coloring a square grid with the exclusion set shown in the upper-right. This is using glucose as the SAT solver.
It's interesting to see patterns emerge without any guidance: tiles, stripes of 3 tiles repeating, hexagonal layout for individual colors.

[jaan3...@gmail.com]

Is there no solution for larger picture disk area? Will it be smaller if you will continue to increase the pixel resolution (radius of exclusion ring)?

[jaan3...@gmail.com]

How could you explain the instability of regular 4-colored zone (red-green-blue-violett) for your radius 3 exclusion zone? It seems it could be expanded on whole plane.

[jaan3...@gmail.com]

What if you will use hexagonal grid and true hexagonal exclusion zones (you have already a nice programm for them) instead of square grid and approximate zones? Required number of colors will increase, of course. But maybe it will give something. Or is it a nonsense? 

[Tom Sirgedas]

I'm sure it could go larger, but the SAT solver takes longer. The pictures already correspond to enormous graphs, but I think there are many solutions for them to stumble into, which helps the solver return an answer reasonably quickly.

I tried using a grid diameter of 51, and an exclusion radius of 10. This ran for 16 hours without a reply.

[Tom Sirgedas]

How could you explain the instability of regular 4-colored zone (red-green-blue-violett) for your radius 3 exclusion zone? It seems it could be expanded on whole plane.

Yeah, I think it could be expanded to the whole plane, too. Glucose found a valid solution. It doesn't care about regularity.

[Tom Sirgedas]

What if you will use hexagonal grid and true hexagonal exclusion zones (you have already a nice programm for them) instead of square grid and approximate zones? Required number of colors will increase, of course. But maybe it will give something. Or is it a nonsense? 

Yeah, then any solutions would be actual solutions. Maybe I'll try it. But, the grid sizes I can explore will be small, unless I allow for 7-coloring or 8-coloring or whatever glucose can easily find a solution for. When the solution doesn't exist or is rare, but there are a lot of reasonable possibilities to explore, I think the SAT solver spends its time exploring a lot of dead ends. If there's no solution, the SAT solver won't reply until it's ruled out all possibilities.

[Tom Sirgedas]

radius 5

I searched with a wrap-around grid, and also forced the top-left 5x3 squares to all be the same color (to make search faster). Here are two results.

[Tom Sirgedas]

radius 8

radius 10

[Tom Sirgedas]

radius 11

[jaan3...@gmail.com]

All pictures are interesting. One can see here everything from Pritikin's to Aubrey's pentagons. But I cannot see here something more. What was the goal?

[Tom Sirgedas]

I was thinking of how an algorithm could search for promising tiling patterns. It's a hard problem, but I knew I could set up an approximation on a square grid, so I did! Maybe the solver would find a novel tiling pattern, or some useful insight. Anyways, I'm fascinated by what the solver comes up with, so I thought I'd share. 

[jaan3...@gmail.com]

OK. But your exclusion zones are far from original ones. If we take some small disk with diameter 1/r, then the thickness of exclusion ring will be 2/r. So you could try to double the thickness of your rings (using the same square grid approximation).

[jaan3...@gmail.com]

Hm, I'm wrong again. I thought about hexagons with their ring thickness doubling effect.

[jaan3...@gmail.com]

But squares should lead to some ring thickness "doubling" too.

[jaan3...@gmail.com]

I mean that without ring thickening you will get weak patterns. Example is radius 3, where 4 colors are enough.

[Tom Sirgedas]

Yeah, you're right. I'm now trying to find some results with a thicker exclusion ring, for a small disk.

[Tom Sirgedas]

radius 7.5

If you add the blue dots to the exclusion disc, then no solution is possible for even a small disk (diameter ~24)