SAT solving – An alternative to brute force Bitcoin mining (2013)

SAT solving SHA256 is a dead end - I was researching this for the purpose of Bitcoin mining (before this article came out), along with many others, for profit.<p>SAT solving typically relies on reducing a function down to boolean expressions where clauses are minimally connected with AND operations (a.k.a. Conjunctive Normal Form).<p>The math basis for this is that in GF2 (Galois Field 2 - a number system with only 2 values):<p><pre><code> AND is equivalent to Multiply (1 * 1 = 1; 1 * 0 = 0, etc.) XOR is equivalent to Addition (1 + 1 = 0; 0 + 1 = 1, etc.) </code></pre> This is useful because we can re-express a boolean function as multiplication and addition for complexity analysis.<p>The difficulty comes when you mix AND and XORs; take the Ch function within SHA256 -<p><pre><code> Ch(E, F, G) == (E &amp; F) | (~E &amp; G) </code></pre> Which can be rewritten as:<p><pre><code> Ch(E, F, G) == (((F ^ G) &amp; E) ^ F) </code></pre> Rewritten in GF2 it is equivalent to:<p><pre><code> Ch(E, F, G) == ((F + G) * E) + F </code></pre> Because of distributive laws, we know there is zero way to simplify this further.<p>Its trivial to see that to work backwards, you have to &quot;consider&quot; way more input combinations for every known output. Even if the output is 0 (which you want when Bitcoin mining), you have this problem where there are 4 possible input combinations.<p>Now unroll the entire SHA256d function Bitcoin uses and you realize the effort to work backwards is far more than the effort to brute-force the input keyspace. This explosion in complexity comes from the fact that the whole function feeds forward, so there is little that can be done to &quot;resolve out&quot; intermediate values as there are no cyclic value dependencies.<p>SHA256d is effectively a giant rat&#x27;s nest of multiplies and adds, all stacked on top of each other, that cannot be reduced, due to distributive laws.

This is an old article. This one is also very interesting by the same author: <a href="https://jheusser.github.io/2013/12/30/satcoin-code.html" rel="nofollow">https:&#x2F;&#x2F;jheusser.github.io&#x2F;2013&#x2F;12&#x2F;30&#x2F;satcoin-code.html</a><p>Proof of concept of the SAT solving idea.

&gt;Initial tests showed that block 218430 with considerably higher difficulty is solved more efficiently than the genesis block 0 for a given nonce range.<p>This is very misleading. 99.99999999% of the work of finding a valid block is finding the right block header to mine on. You have 2^32 possible nonces, and your odds of finding a block are 1 in 2^67.<p>By giving his program the block in advance, he&#x27;s taking a shortcut.<p>An algorithm that could quickly decide whether a block header contained a valid solution would be very valuable indeed.

The part I find most interesting is that (if I understand it correctly), bruteforce gets harder as SAT solving gets easier. That is - the more zeros are required, the fewer variables are in the SAT problem. The less zeros are required, the higher chance of bruteforcing a correct result.<p>(edit: actually not fewer variables, but... I&#x27;m not sure what the correct term is, but the tree of operations gets smaller, because more results have to be fixed)

While SAT, and their cousin SMT, solvers are useful in the analysis of symmetric cryptographic primitives, they quickly become useless once the complexity of the problem hits a certain threshold. They are best employed to analyze contained parts of the primitive.<p>It can be wise to use a SAT solver to find a preimage of, e.g., SHA-256 reduced to 10 rounds. But it will be hopeless on the full function, unless it is severely broken.

In general, if one could find preimages using SAT it wIn general, if one could find preimages using SAT it would be done for cryptanalytic purposes would be done for cryptanalytic purposes. SAT is also not likely to admit a hardware (ASIC, etc) solution, so it would be much more difficult to massively parallelize and to keep cost per hash low.