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

I don't think it's the Ch function itself (and the rest of the compression function) that causes problems for the SAT solver. I think it's the combination of the compression function and the message schedule that does it. If the message schedule had just been free variables (or simple repetitions of the message), I'm pretty sure the SAT solver would be able to unwind the compression function just fine.

The problem is the interaction between the message schedule and the compression function; once you commit to a value in some round of the compression function, you actually impose a set of constraints on the message schedule for all the other rounds simultaneously. So in a way, committing to a value in some round of the compression function means you're also indirectly influencing the possible values in every other round too. It creates this weird sort of dependency between the rounds which wouldn't exist if you only had a long series of Ch functions.

Is that actually true or did I just bs myself?

I was curios if anyone here is mining bitcoins and if it's worth their time.

"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."

This is actually pretty misleading. There might be fewer variables, but that's irrelevant. Yes, there are actually fewer variables in the actual file you feed to the SAT solver because you can assume they are 0 and propagate that to the other constraints involving those variables. But think about it -- you're only going to get rid of a couple of hundred variables at most, in a problem with ~250,000 variables. So you're only really reducing the full search space by an incredibly small percentage.

In practice, the running time of the SAT solver increases exponentially with the number of zeros you assume in the hash, just like it does for a regular brute force trying all combinations of inputs.

The conclusion I draw from this is that not all variables contribute equally to the difficulty of a problem (for a SAT solver). This is actually why SAT solvers can be efficient for some problems in the first place, even for problems with hundreds of thousands of variables; the SAT solver (a smart brute force, as opposed to a naive brute force) is able to exploit the fact that many problems you feed to it are not intrinsically hard.

In the extreme case, where we require no zeros, the problem is trivial (just hash any old data), and any good SAT solver will finish fairly quickly (perhaps with a little guidance). If we require all zeros, we are effectively asking the solver to break SHA2, which no SAT solver is going to do well at at present, or the forseeable future.

While assigning variables does decrease the worst-case complexity, no number of zeroes can be brute forced by exhaustive search before the heat death of the universe, and assigning zeroes makes finding solutions harder in a search problem which is still massive.