2 ms·
A hard SAT problem: Let nonce be 32 boolean inputs, representing numbers from 0..2^32-1. Let other_bits and difficulty be a collection of constant boolean inp
by jlokier 6y ago
A hard SAT problem:
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.
- nightcracker 6y agoThis SAT instance is huge, which makes it hard. But you haven't shown that it is a harder SAT instance than a random one of its size. It's all about the difficulty vs the size of the instance.
- jlokier 6y agoTo the best of my knowledge, the example has no known heuristics for finding a solution that are significantly faster than brute force. 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.
- nightcracker 6y agoA 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.