For strange people like myself, a headline like The 17x17 challenge. Worth $289.00. This is not a joke." is like waving a red rag in front of a bull!
17x17 and 18x18 colourings have been found!
Having recently encountered binary decision diagrams (BDDs) via Knuth's Computer Musings, I thought they might be a good approach as they tend to be useful for combinatorial problems. Knuth calculates various large numbers such as the number of possible knight's tours for various board sizes.
I wrote a program to construct a BDD for an arbitrary nxm board. Unfortunately, I quickly ran out of memory for relatively small boards, and had to rent time on a 32GB Amazon EC2 cloud computer to compute the number of colourings for the 5x4. I also ran into issues with the BDD libraries not coping well with more than 400 million nodes.
I eventually found a better variable ordering that allowed me to solve the 5x5 using a peak of around 24GB of RAM in 1hr40m, but 17x17 still seems beyond reach as each new square seems to roughly double the number of nodes.
Having said that, the numbers calculated so far would be very useful for verifying a closed-form expression, if it exists.
Since we know that the number of possible rectangles in an nxn grid is 1/4 n2(n-1)2, we can get a rough idea of what the number of solutions looks like if we take the factorial of the number of possible rectangles and subtract it from the total number of possible 4-colourings i.e. O(4n2 - n4!). Here is a plot of this function. You can see that the number grows almost exponentially, and then suddenly and sharply drops off to below zero.
This agrees with what we know already i.e. that there are no solutions for 19x19 and above, but that the number of solutions grows quickly for smaller nxm, so it probably drops off sharply at some point.
I was excited to find that no-one else seemed to have calculated these numbers before, so I was able to make my first contribution to the OEIS!
I've spent some time trying to analyse the 3x3 solutions by hand (2x2 is trivial: 44 - 4 solutions, because there are only 4 colourings containing a monochromatic rectangle). I was hoping to find some simplification when analysing the 3x3 that could be extended for arbitrary nxm.
There are 9 possible rectangles in the 3x3 grid, so it's possible to analyse each one in turn. The total number of solutions should be 4nm - R, where R is the number of unique colourings containing monochromatic rectangles. The uniqueness is the tricky part, of course!
I found it confusing to even calculate this by hand, so I wrote a small program to compute the number of non-overlapping colourings for each monochromatic rectangle.
The first few rectangles are simple but it gets more and more difficult to figure out exactly which previous rectangles overlap the current one and how that affects the number of colourings.
I'm still hopeful that a closed-form expression can be found, or even a non-closed-form expression that's more efficient to compute than constructing the full BDD. Then we'll have a definitive answer for whether the 17x17 is colourable or not. Of course, it seems like the experts would have already tried to find such an expression, but maybe they didn't have the numbers above to guide them!