You can also mine Bitcoin with SAT solvers. And if the difficulty is high enough, it will be more efficient than the current brute force methods methods

https://jheusser.github.io/2013/02/03/satcoin.html

> Bitcoin Difficulty and Assumptions

> A very intriguing, and perhaps unintuitive property of the algorithm proposed is that with increasing bitcoin difficulty, or equally lower target, the search could become more efficient, at least in theory. This is because we can assume more about the structure of a valid hash -- a lower target means more leading zeros which are assumed to be zero in the SAT-based algorithm.

> If this is true and is a substantial effect then this is an important issue since the rate of the money supply is regulated with the difficulty. The higher the difficulty, the less likely it is that an individual block has a valid nonce. However, conventional mining algorithms always have to perform the same amount of work (i.e. try 4 billion nonce values) to reject a block. On the other hand, "Satcoin" miners will get progressively faster which could lead to imbalances in the controlled supply. These are all just speculations and depend on many factors, first and foremost how well the SAT-based approach can be improved and whether the probability of finding a valid nonce does not dwarf the efficiency gain of the algorithm.

https://www.quora.com/Are-SAT-solvers-faster-than-linear-sea...

https://github.com/jheusser/satcoin an implementation