3 ms·
> 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 f
by throwawaylinux 3y ago
> 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 3y agoAlso, 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..