If I get really bored one weekend I might get a Spectrum off eBay (rubber keyed version, naturally) and see if I can write a solver in Sinclair basic. Would be interesting to see how long it would take to solve these problems.
On a similar note I wonder what the smallest possible program file size would be, in bytes. I suppose as you say it would depend on whether you just do it by brute force or by more clever methods - but then you could look at the product of time taken and file size as a measure of efficiency, smaller being better.
You could then divide this by the number of transistors in your device and have to competition to see who gets the lowest score! Anyone up for a challenge?