[junon]

> 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-/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

[gus_massa]

The article is not super clear, but the problem in the article has an additional requests, to maximize the GCD of the rows interpreted as "9" digits numbers, in your case:

GCD(127685439, 594137826, 836429571, ...) = 9

but the author finds one GCD with 8 digits.

Also, for this reason it's important in this version to keep the "0" as "0" instead of mapping it to "1".