adopted from https://ericpony.github.io/z3py-tutorial/guide-examples.htm

game.py

#!/usr/bin/env python3
import z3
import pprint

# 9x9 matrix of integer variables
X = [ [ z3.Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
      for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ z3.And(1 <= X[i][j], X[i][j] <= 9)
             for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ z3.Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ z3.Distinct([ X[i][j] for i in range(9) ])
             for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ z3.Distinct([ X[3*i0 + i][3*j0 + j]
                        for i in range(3) for j in range(3) ])
             for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

#### additional for "miracle" sudoku
ortho_adjacent = []
for i in range(9):
    for j in range(9):
        if j+1 < 9:
            ortho_adjacent.append(z3.And(X[i][j] != X[i][j+1] + 1))
        if i+1 < 9:
            ortho_adjacent.append(z3.And(X[i][j] != X[i+1][j] + 1))
        if j-1 >= 0:
            ortho_adjacent.append(z3.And(X[i][j] != X[i][j-1] + 1))
        if i-1 >= 0:
            ortho_adjacent.append(z3.And(X[i][j] != X[i-1][j] + 1))


knights = []
for i in range(9):
    for j in range(9):
        if j+2 < 9:
            if i+1 < 9:
                knights.append(z3.And(X[i][j] != X[i+1][j+2]))
            if i-1 >= 0:
                knights.append(z3.And(X[i][j] != X[i-1][j+2]))
        if j-2 >= 0:
            if i+1 < 9:
                knights.append(z3.And(X[i][j] != X[i+1][j-2]))
            if i-1 >= 0:
                knights.append(z3.And(X[i][j] != X[i-1][j-2]))
        if i+2 < 9:
            if j+1 < 9:
                knights.append(z3.And(X[i][j] != X[i+2][j+1]))
            if j-1 >= 0:
                knights.append(z3.And(X[i][j] != X[i+2][j-1]))
        if i-2 >= 0:
            if j+1 < 9:
                knights.append(z3.And(X[i][j] != X[i-2][j+1]))
            if j-1 >= 0:
                knights.append(z3.And(X[i][j] != X[i-2][j-1]))

kings = []
for i in range(9):
    for j in range(9):
        if i-1 >= 0:
            kings.append(z3.And(X[i][j] != X[i-1][j]))
        if i+1 < 9:
            kings.append(z3.And(X[i][j] != X[i+1][j]))
        if j-1 >= 0:
            kings.append(z3.And(X[i][j] != X[i][j-1]))
        if j+1 < 9:
            kings.append(z3.And(X[i][j] != X[i][j+1]))
        if i-1 >= 0 and j-1 >= 0:
            kings.append(z3.And(X[i][j] != X[i-1][j-1]))
        if i-1 >= 0 and j+1 < 9:
            kings.append(z3.And(X[i][j] != X[i-1][j+1]))
        if i+1 < 9 and j-1 >= 0:
            kings.append(z3.And(X[i][j] != X[i+1][j-1]))
        if i+1 < 9 and j+1 < 9:
            kings.append(z3.And(X[i][j] != X[i+1][j+1]))



sudoku_c += knights
sudoku_c += ortho_adjacent
sudoku_c += kings
####

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,0,0,0,0,0),
            (0,0,0,0,0,0,0,0,0),
            (0,0,0,0,0,0,0,0,0),
            (0,0,0,0,0,0,0,0,0),
            (0,0,1,0,0,0,0,0,0),
            (0,0,0,0,0,0,2,0,0),
            (0,0,0,0,0,0,0,0,0),
            (0,0,0,0,0,0,0,0,0),
            (0,0,0,0,0,0,0,0,0))

instance_c = [ z3.If(instance[i][j] == 0,
                  True,
                  X[i][j] == instance[i][j])
               for i in range(9) for j in range(9) ]

s = z3.Solver()
s.add(sudoku_c + instance_c)
if s.check() == z3.sat:
    m = s.model()
    r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
          for i in range(9) ]
    pprint.pprint(r)
else:
    print("failed to solve")