Earlier quoted context omitted.
The problem isn't what you think it is, otherwise the solution would be trivial: alternate one pair of colors on even rows, and then alternate another pair on odd rows. That satisfies the four color theorem. This problem differs in two ways. First, we're not looking for all of the vertices to be different colors. We're looking for them to not all be the same color. This is easier to do. Second, he's not trying to col…
I see now! I completely missed this part: "Second, he's not trying to color a simple planar graph. He means every rectangle on the grid -- for example, a 7 x 8 rectangle in the middle somewhere. This is much, much harder to do." Otherwise the problem seemed trivial. On the other hand... how many possible 17x17 4-colored grids are there? Can this be brute forced?
4^(17*17) ~= 10^173.. a bit too many to brute force, but I'm sure you could narrow the number down a lot with simple heuristics (though it would still be too large to brute force).