When you say "clause", do you mean a disjunction of literals in propositional logic? Because if so, I don't understand what you mean. Clauses don't have inputs. And when you say "resolve away", do you mean applying the resolution rule?
I would like to respectfully disagree. I think you're simplifying the reason too much.
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.
It is true in an absolute, mathematical sense that the search space gets smaller when you fix a variable to a particular value.
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.
"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.