# Modeling tiling problems as SAT problems

I read that tiling problems can be modeled as satisfiability problems (2-SAT?), but the author did not explain how. Is this true? What would be an example?

By a "tiling problem" I mean you have a matrix and have to fill it up according to some constraint. For example, you might have to fill the matrix with a particular shape, or the values in the matrix have to adhere to some constraint. For example, imagine a partially filled matrix and the rule is that you have to fill it with values that are one more or one less than the adjoining values, or something like that.

• Where did you read this? What did the authors say to support their statement? Commented Apr 15, 2017 at 8:23
• In addition to Raphael's comments, the definition of "tiling problem" could be made more precise. Can we use an unlimited number of copies of the shape? Is there just one shape or multiple? (I don't see what filling cells with numbers has to do with tiling.) It might help to know what the problem is before trying to find algorithms for it.
– D.W.
Commented Apr 15, 2017 at 10:03
• @D.W. The question is not about a specific problem. It is about a concept. It doesn't matter what example of a tiling problem the answerer chooses. I just want to understand the application of SAT to tiling. If the answerer wants to include an example, then they are free to use any tiling problem they choose as the example problem. Commented Apr 15, 2017 at 12:35

## 2 Answers

One example of a tiling problem that was successfully attacked by reducing it to a SAT instance was rectangular grid coloring. In "Extremely Complex 4-Colored Rectangle-Free Grids: Solution of Open Multiple-Valued Problems" the authors describe how they tackled 17x17, 17x18, and 18x18 grid colorings using a SAT solver plus some previous knowledge of grid coloring theory to pare down the search space.

It's possible that you're talking about Wang tiles. Imagine that you have to fill up a matrix with tiles that cannot be rotated. Each side of each tile is a given color. If two tiles are placed next to each other (share an edge), they must have the same color along that edge.

While the color vs number aspect is not important, this differs from your requirement in that each side has a different color (whereas you are talking about only a single number per spot). So far as I can tell, this difference is fundamentally important.

If you want to obtain NP-hardness, I believe you need further constraints (such as having colors along the border of the matrix). However, with this slight extension, it seems that this can fairly easily be proven by extending the undecideability result for Wang tiles; this mathoverflow answer discusses this a bit.