This is different than a SAT solver approach in my view,

What I'm proposing is coming up with equations that represent doing the double SHA256 symbolically.   Each equation will have no more logical operations than the double hash itself (sans the symbolic carry bits from addition) and no more than 640 input variables corresponding to the input bits of the block header.

All of this can be computed offline.   Then it's about solving a system of 32 equations with 32 unknowns to derive the correct nonce.  I propose this can be done faster than trying to hash the full nonce range on the CPU, maybe faster than doing it on a GPU;  Wolfram Mathematica for example can do it in a few seconds depending on the equation complexity.