Let nonce be 32 boolean inputs, representing numbers from 0..2^32-1.

Let other_bits and difficulty be a collection of constant boolean inputs, in the following expression.

Let f(other_bits, nonce, diff) be the boolean logic circuit used in Bitcoin mining, for a recent candidate block.

Roughly speaking, f combines nonce with other_bits to make a bit string, performs SHA-256 on the bit string, then SHA-256 on that, and then checks if the leading diff number of bits are zero.

Folding in the constants, f reduces to a boolean logic circuit with 32 inputs and 1 output, g(nonce) = result.

The SAT problem: Does there exist a value of nonce for which g(nonce) = 1?

If you can solve this quickly, you just sped up Bitcoin mining by a factor 2^32 iterations, which is a lot. You can take this further as well.

I don't know of any SAT solver heuristic which really helps with this.

It's all about the difficulty vs the size of the instance.

That puts it in the hardest class of instances for its size (subject to available knowledge), because all instances can be solved by brute force.

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.

How current is your information ?

I think I've seen random instances in some of the more recent SAT competitions with only a few thousand variables that have not been solved. That said in theory there should be 100 variable instances that are too hard to solve but I haven't seen any really hard instances that small.

One paper was about creating random sat instances where the probability of unsat ist 50/50 and as it turned out: none of those instances was hard.

You can always craft hard instances to defeat a specific heuristic. But crafting one that is hard for all of them is the problem.