[throwawaylinux]

> However, it apparently can write a program using the Z3 SAT solver to find a solution.

Not that it's unimpressive in general that a LLM can write a program from a prompt like that, but for this particular juxtaposition it doesn't seem like it's especially interesting or impressive that it can write such a program. A SAT program is basically just re-stating the the rules in a particular form. It doesn't even have to be able to apply those rules. The solver does the hard work.

[kaba0]

Also, if it has enough training data to know how to write such a SAT solver problem, it has surely seen sudoku exercises as part of that data set..