A SAT solver might very well have optimizations that make it end up running in 2^200 on average instead of what brute force would give. The problem is, since t

A SAT solver might very well have optimizations that make it end up running in 2^200 on average instead of what brute force would give. The problem is, since the instance is so large, we don't know what happens. No one has ever ran one to completion. So no, it's not in the hardest class of instances for its size. Its difficulty is unknown.