Comment by nickysielicki

Here's a solver in python with z3: https://gist.github.com/sielicki/fd86d68733133f654128519b3c4...

(note, most of the code coming from here, I just slopped together the additional constraints, https://ericpony.github.io/z3py-tutorial/guide-examples.htm )

    $ time python3 game.py
    [[4, 8, 3, 7, 2, 6, 1, 5, 9],
     [7, 2, 6, 1, 5, 9, 4, 8, 3],
     [1, 5, 9, 4, 8, 3, 7, 2, 6],
     [8, 3, 7, 2, 6, 1, 5, 9, 4],
     [2, 6, 1, 5, 9, 4, 8, 3, 7],
     [5, 9, 4, 8, 3, 7, 2, 6, 1],
     [3, 7, 2, 6, 1, 5, 9, 4, 8],
     [6, 1, 5, 9, 4, 8, 3, 7, 2],
     [9, 4, 8, 3, 7, 2, 6, 1, 5]]
    python3 game.py  7.47s user 0.15s system 97% cpu 7.801 total