(edit: actually not fewer variables, but... I'm not sure what the correct term is, but the tree of operations gets smaller, because more results have to be fixed)
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.
"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.
However, by fixing a variable (and effectively removing it), you are also removing potential solutions from that search space.
In a sense, you could view the difficulty of a SAT problem as the fraction of valid solutions in the whole search space. By fixing a variable, you are decreasing both the number of valid solutions and the size of the total search space. But the fraction could end up being either greater or smaller, depending on the variable and the value you set it to.