Is AES solvable in this way? In other words, will the algorithm eventually complete, producing the correct key?
Almost yes. It will produce some correct key — there might be more than one.
(It should quite plausibly be unique given "enough" plaintext-ciphertext samples, but this need not be the case in general.)
Generally, computing the key in a known-plaintext scenario is in $\mathbf{NP}$, hence can by definition be reduced to any $\mathbf{NP}$-complete problem such as $\mathrm{SAT}$. If this is done correctly, solving the $\mathrm{SAT}$ instance is bound to produce a correct key — but fortunately, doing so is not at all practical to the best of our current knowledge.
(If it turned out that $\mathbf P=\mathbf{NP}$, this would potentially change that picture a bit, but in that case we are doomed anyway.)
Therefore the short answer is: Yes, but it doesn't help.