This paper proposes an alternative mining algorithm which does not perform a brute force search but instead attacks this problem using a number of tools used in the program verification domain to find bugs or prove properties of programs.

Namely, a model checker backed by a SAT solver are used to find the correct nonce or prove the absence of a valid nonce. In contrast to brute force, which actually executes and computes many hashes, my approach is only symbolically executing the hash function with added constraints which are inherent in the bitcoin mining process.

The author of this paper introduced a novel algorithm to solve the bitcoin mining problem without using (explicit) brute force. Instead, the nonce search is encoded as a decision problem and solved by a SAT solver in such a way that a satisfiable instance contains a valid nonce. The key ingredients in the algorithm are a non-deterministic nonce and the ability to take advantage of the known structure of a valid hash using assume statements.

A couple of benchmarks demonstrated that already with simple parameter tuning dramatic speed ups can be achieved. Additionally, the writer explored the contentious claim that the algorithm might become more efficient with increasing bitcoin difficulty. Initial tests showed that block 218430 with considerably higher difficulty is solved more efficiently than the genesis block 0 for a given nonce range.