from z3 import *


# we create variables for every cell
b10 = Bool("b10")
b30 = Bool("b30")
b50 = Bool("b50")
b70 = Bool("b70")
b11 = Bool("b11")
b21 = Bool("b21")
b31 = Bool("b31")
b41 = Bool("b41")
b51 = Bool("b51")
b61 = Bool("b61")
b71 = Bool("b71")
b81 = Bool("b81")
b02 = Bool("b02")
b12 = Bool("b12")
b32 = Bool("b32")
b42 = Bool("b42")
b62 = Bool("b62")
b72 = Bool("b72")
b82 = Bool("b82")
b92 = Bool("b92")
b03 = Bool("b03")
b13 = Bool("b13")
b23 = Bool("b23")
b33 = Bool("b33")
b53 = Bool("b53")
b63 = Bool("b63")
b93 = Bool("b93")
b34 = Bool("b34")
b44 = Bool("b44")
b54 = Bool("b54")
b64 = Bool("b64")
b84 = Bool("b84")
b05 = Bool("b05")
b15 = Bool("b15")
b25 = Bool("b25")
b35 = Bool("b35")
b55 = Bool("b55")
b75 = Bool("b75")
b95 = Bool("b95")
b06 = Bool("b06")
b16 = Bool("b16")
b26 = Bool("b26")
b46 = Bool("b46")
b56 = Bool("b56")
b76 = Bool("b76")
b96 = Bool("b96")
b17 = Bool("b17")
b27 = Bool("b27")
b47 = Bool("b47")
b57 = Bool("b57")
b77 = Bool("b77")
b87 = Bool("b87")
b97 = Bool("b97")
b08 = Bool("b08")
b28 = Bool("b28")
b48 = Bool("b48")
b58 = Bool("b58")
b78 = Bool("b78")
b88 = Bool("b88")
b09 = Bool("b09")
b19 = Bool("b19")
b29 = Bool("b29")
b39 = Bool("b39")
b49 = Bool("b49")
b59 = Bool("b59")
b69 = Bool("b69")
b89 = Bool("b89")


# we create a formula which says that we have a valid solution
s = Solver()
# the number 1 at (0,0)
s.add(AtLeast(b10, b11, 1))
s.add(AtMost(b10, b11, 1))
# the number 1 at (2,0)
s.add(AtLeast(b10, b30, b11, b21, b31, 1))
s.add(AtMost(b10, b30, b11, b21, b31, 1))
# the number 1 at (4,0)
s.add(AtLeast(b30, b50, b31, b41, b51, 1))
s.add(AtMost(b30, b50, b31, b41, b51, 1))
# the number 2 at (6,0)
s.add(AtLeast(b50, b70, b51, b61, b71, 2))
s.add(AtMost(b50, b70, b51, b61, b71, 2))
# the number 1 at (8,0)
s.add(AtLeast(b70, b71, b81, 1))
s.add(AtMost(b70, b71, b81, 1))
# the number 1 at (9,0)
s.add(AtLeast(b81, 1))
s.add(AtMost(b81, 1))
# the number 1 at (0,1)
s.add(AtLeast(b10, b11, b02, b12, 1))
s.add(AtMost(b10, b11, b02, b12, 1))
# the number 1 at (9,1)
s.add(AtLeast(b81, b82, b92, 1))
s.add(AtMost(b81, b82, b92, 1))
# the number 3 at (2,2)
s.add(AtLeast(b11, b21, b31, b12, b32, b13, b23, b33, 3))
s.add(AtMost(b11, b21, b31, b12, b32, b13, b23, b33, 3))
# the number 2 at (5,2)
s.add(AtLeast(b41, b51, b61, b42, b62, b53, b63, 2))
s.add(AtMost(b41, b51, b61, b42, b62, b53, b63, 2))
# the number 1 at (4,3)
s.add(AtLeast(b32, b42, b33, b53, b34, b44, b54, 1))
s.add(AtMost(b32, b42, b33, b53, b34, b44, b54, 1))
# the number 3 at (7,3)
s.add(AtLeast(b62, b72, b82, b63, b64, b84, 3))
s.add(AtMost(b62, b72, b82, b63, b64, b84, 3))
# the number 3 at (8,3)
s.add(AtLeast(b72, b82, b92, b93, b84, 3))
s.add(AtMost(b72, b82, b92, b93, b84, 3))
# the number 1 at (0,4)
s.add(AtLeast(b03, b13, b05, b15, 1))
s.add(AtMost(b03, b13, b05, b15, 1))
# the number 1 at (1,4)
s.add(AtLeast(b03, b13, b23, b05, b15, b25, 1))
s.add(AtMost(b03, b13, b23, b05, b15, b25, 1))
# the number 1 at (2,4)
s.add(AtLeast(b13, b23, b33, b34, b15, b25, b35, 1))
s.add(AtMost(b13, b23, b33, b34, b15, b25, b35, 1))
# the number 2 at (7,4)
s.add(AtLeast(b63, b64, b84, b75, 2))
s.add(AtMost(b63, b64, b84, b75, 2))
# the number 3 at (9,4)
s.add(AtLeast(b93, b84, b95, 3))
s.add(AtMost(b93, b84, b95, 3))
# the number 0 at (4,5)
s.add(AtLeast(b34, b44, b54, b35, b55, b46, b56, 0))
s.add(AtMost(b34, b44, b54, b35, b55, b46, b56, 0))
# the number 1 at (6,5)
s.add(AtLeast(b54, b64, b55, b75, b56, b76, 1))
s.add(AtMost(b54, b64, b55, b75, b56, b76, 1))
# the number 3 at (8,5)
s.add(AtLeast(b84, b75, b95, b76, b96, 3))
s.add(AtMost(b84, b75, b95, b76, b96, 3))
# the number 1 at (3,6)
s.add(AtLeast(b25, b35, b26, b46, b27, b47, 1))
s.add(AtMost(b25, b35, b26, b46, b27, b47, 1))
# the number 2 at (6,6)
s.add(AtLeast(b55, b75, b56, b76, b57, b77, 2))
s.add(AtMost(b55, b75, b56, b76, b57, b77, 2))
# the number 4 at (8,6)
s.add(AtLeast(b75, b95, b76, b96, b77, b87, b97, 4))
s.add(AtMost(b75, b95, b76, b96, b77, b87, b97, 4))
# the number 0 at (0,7)
s.add(AtLeast(b06, b16, b17, b08, 0))
s.add(AtMost(b06, b16, b17, b08, 0))
# the number 3 at (3,7)
s.add(AtLeast(b26, b46, b27, b47, b28, b48, 3))
s.add(AtMost(b26, b46, b27, b47, b28, b48, 3))
# the number 4 at (6,7)
s.add(AtLeast(b56, b76, b57, b77, b58, b78, 4))
s.add(AtMost(b56, b76, b57, b77, b58, b78, 4))
# the number 3 at (1,8)
s.add(AtLeast(b17, b27, b08, b28, b09, b19, b29, 3))
s.add(AtMost(b17, b27, b08, b28, b09, b19, b29, 3))
# the number 2 at (3,8)
s.add(AtLeast(b27, b47, b28, b48, b29, b39, b49, 2))
s.add(AtMost(b27, b47, b28, b48, b29, b39, b49, 2))
# the number 4 at (6,8)
s.add(AtLeast(b57, b77, b58, b78, b59, b69, 4))
s.add(AtMost(b57, b77, b58, b78, b59, b69, 4))
# the number 2 at (9,8)
s.add(AtLeast(b87, b97, b88, b89, 2))
s.add(AtMost(b87, b97, b88, b89, 2))
# the number 2 at (7,9)
s.add(AtLeast(b78, b88, b69, b89, 2))
s.add(AtMost(b78, b88, b69, b89, 2))
# the number 0 at (9,9)
s.add(AtLeast(b88, b89, 0))
s.add(AtMost(b88, b89, 0))
if s.check() == sat:
  print(s.model())
  
# the solution returned is below

[b12 = False,
 b13 = True,
 b42 = False,
 b62 = False,
 b15 = False,
 b32 = True,
 b58 = True,
 b10 = False,
 b09 = True,
 b21 = False,
 b53 = False,
 b48 = True,
 b47 = False,
 b19 = True,
 b33 = False,
 b63 = True,
 b30 = False,
 b27 = False,
 b96 = False,
 b41 = False,
 b23 = False,
 b28 = True,
 b61 = True,
 b39 = False,
 b51 = False,
 b05 = False,
 b25 = False,
 b49 = False,
 b29 = False,
 b50 = True,
 b57 = True,
 b11 = True,
 b31 = False,
 b03 = False,
 b02 = False,
 b26 = True,
 b59 = False,
 b77 = False,
 b64 = False,
 b76 = True,
 b75 = False,
 b71 = False,
 b97 = True,
 b69 = True,
 b92 = False,
 b89 = False,
 b08 = False,
 b17 = False,
 b16 = False,
 b56 = False,
 b46 = False,
 b55 = False,
 b35 = False,
 b54 = False,
 b44 = False,
 b95 = True,
 b84 = True,
 b88 = False,
 b78 = True,
 b87 = True,
 b06 = False,
 b34 = False,
 b93 = True,
 b72 = True,
 b82 = False,
 b81 = True,
 b70 = False]