Rating:
In order to solve this challenge I used the library z3py. This library is usually used to verify math theorems and allows you to find solution to problems.
The original documentation contains an example with the sudoku that I used and modified to solve the challenge.
```
# Based on the example at: https://ericpony.github.io/z3py-tutorial/guide-examples.htm
from z3 import *
# 9x9 matrix of integer variables
X = [[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 = [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 = [Distinct(X[i]) for i in range(9)]
# each column contains a digit at most once
cols_c = [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 = [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
# sudoku instance, we use '0' for empty cells
instance = ((0, 0, 0, 0, 0, 0, 0, 0, 1),
(0, 1, 2, 0, 0, 0, 0, 0, 0),
(0, 0, 0, 0, 0, 0, 2, 0, 0),
(0, 0, 0, 0, 0, 0, 0, 0, 2),
(0, 2, 0, 0, 0, 0, 0, 0, 0),
(0, 0, 0, 0, 0, 0, 0, 0, 0),
(0, 0, 0, 0, 0, 0, 1, 2, 0),
(1, 0, 0, 0, 0, 2, 0, 0, 0),
(0, 0, 0, 1, 0, 0, 0, 0, 0))
instance_c = [If(instance[i][j] == 0,
True,
X[i][j] == instance[i][j])
for i in range(9) for j in range(9)]
s = Solver()
# Extra conditions
s.add(X[0][4] + X[3][6] + X[8][4] + X[6][7] + X[1][2] + X[0][4] == 19)
s.add(X[8][6] + X[3][8] + X[1][5] + X[0][7] + X[0][2] + X[2][3] == 27)
s.add(X[2][6] + X[7][8] + X[8][6] + X[1][1] + X[7][7] + X[6][2] == 31)
s.add(X[1][8] + X[1][7] + X[2][0] + X[7][3] + X[7][3] == 23)
s.add(X[8][5] + X[0][4] + X[8][2] + X[1][7] + X[2][2] == 20)
s.add(X[5][4] + X[1][7] + X[5][7] + X[8][6] + X[5][0] == 33)
s.add(X[2][0] + X[8][3] + X[2][1] + X[8][0] + X[0][3] == 20)
s.add(X[5][7] + X[2][0] + X[5][5] + X[3][2] + X[1][5] == 25)
s.add(X[8][1] + X[8][2] + X[5][1] + X[4][8] == 15)
s.add(X[8][6] + X[7][7] + X[2][1] + X[3][8] == 26)
s.add(X[3][2] + X[8][7] + X[0][3] + X[8][5] == 27)
s.add(X[0][1] + X[0][7] + X[3][6] + X[4][3] == 21)
s.add(sudoku_c + instance_c)
if s.check() == sat:
m = s.model()
r = [[m.evaluate(X[i][j]) for j in range(9)]
for i in range(9)]
print_matrix(r)
else:
print("failed to solve")
# Result
# [
# [8, 6, 4, 7, 2, 9, 5, 3, 1],
# [9, 1, 2, 4, 5, 3, 7, 6, 8],
# [3, 7, 5, 6, 1, 8, 2, 4, 9],
# [6, 4, 9, 8, 7, 5, 3, 1, 2],
# [7, 2, 1, 9, 3, 6, 8, 5, 4],
# [5, 3, 8, 2, 4, 1, 6, 9, 7],
# [4, 8, 6, 5, 9, 7, 1, 2, 3],
# [1, 9, 7, 3, 6, 2, 4, 8, 5],
# [2, 5, 3, 1, 8, 4, 9, 7, 6]
# ]
#
# 86472953189247356794813521457639
```