> My first attempt when solving this puzzle was to encode the constraints as an SMT optimization problem, and using Z3 to find the solution. This is why choosi

> My first attempt when solving this puzzle was to encode the constraints as an SMT optimization problem, and using Z3 to find the solution. This is why choosing the right tool for the job matters. Z3 is hilariously overkill for such a problem (not to undermine how interesting and useful Z3 is, and not to accuse the author of doing anything wrong). Z3 is only one class of solver; a finite domain constraint solver is much more suited to these sorts of tasks. https://gist.github.com/Qix-/3580f268e2725848971703e74f6b26b2 https://gist.github.com/Qix-/3580f268e2725848971703e74f6b26b... $ time node sudoku.js 1 2 7 6 8 5 4 3 9 5 9 4 1 3 7 8 2 6 8 3 6 4 2 9 5 7 1 3 6 1 8 5 4 2 9 7 7 4 5 2 9 1 3 6 8 2 8 9 3 7 6 1 5 4 6 5 3 9 1 8 7 4 2 4 1 2 7 6 3 9 8 5 9 7 8 5 4 2 6 1 3 0:00.08elapsed