Is AES solvable by reducing to SAT? Consider a known plaintext attack on AES — just so we have an actual system of equalities that we can feed to a SAT solver.

Is AES solvable in this way? In other words, will the algorithm eventually complete, producing the correct key?

After reading through these set of slides, I assume the answer is yes, but that it is computationally even more costly than brute force, making it impractical.
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.