That is surprising.

Can you point me to a concrete reference about the 50x50 number?

Modern SAT solvers should be able to handle that, maybe with a few problem specific tweaks.

That's a bit too simply put, unfortunately. You could do that with an `e^{n/50}` solution. That wouldn't really be unexpected.