Calcudoku
Calcudoku is just like Sudoku - you must enter numbers into a grid in such a way so that no number is repeated in any row or column. But Calcudoku puzzles have an added mathematical component! Each grid is split up into smaller sections of 2 or more squares, and each of those sections has an arithmetic equation attached to it (either addition, subtraction, multiplication or division). You must complete the grid so that the numbers is each section equal the mathematical formula assigned to it.
Hard Calcudoku puzzle
Here is a hard Calcudoku puzzle 
Solution using Z3
from z3 import Solver, And, Int, Distinct, sat, If
from functools import reduce
import operator
def Max(x):
return reduce(lambda a, b: If(a > b, a, b), x)
def cd_div(v, *x):
m = Max(x)
m /= reduce(operator.mul, (If(i != m, i, 1) for i in x))
return m == v
def cd_sub(v, *x):
m = Max(x)
m -= sum(If(i != m, i, 0) for i in x)
return m == v
def print_grid(mod, x, rows, cols):
for i in range(rows):
print(" ".join([str(mod.eval(x[i][j])) for j in range(cols)]))
# This is the encoding of the puzzle
def hardest_calcudoku(X):
return [
X[0][0] + X[0][1] + X[0][2] + X[1][0] + X[2][0] == 21,
X[0][3] * X[0][4] * X[0][5] * X[1][4] == 60,
X[0][6] + X[0][7] + X[0][8] + X[1][8] + X[2][8] == 25,
cd_sub(6, X[1][1], X[1][2]),
X[1][3] + X[2][3] == 11,
cd_sub(4, X[1][5], X[2][5]),
X[1][6] + X[1][7] == 13,
X[2][1] + X[3][1] == 8,
X[2][2] == 8,
X[2][4] == 2,
X[2][6] == 9,
X[2][7] + X[3][7] == 11,
X[3][0] + X[4][0] + X[5][0] + X[4][1] == 24,
X[3][2] + X[3][3] == 13,
X[3][4] + X[4][4] + X[5][4] + X[4][5] + X[4][3]== 25,
cd_sub(3, X[3][5], X[3][6]),
X[3][8] + X[4][8] + X[5][8] + X[4][7] == 17,
X[4][2] == 2,
X[4][6] == 3,
cd_sub(1, X[5][1], X[6][1]),
X[5][2] + X[5][3] == 13,
cd_sub(1, X[5][5], X[5][6]),
X[5][7] + X[6][7] == 11,
X[6][0] + X[7][0] + X[8][0] + X[8][1] + X[8][2] == 26,
X[6][2] == 1,
X[6][3] * X[7][3] == 16,
X[6][4] == 6,
X[6][5] + X[7][5] == 12,
X[6][6] == 7,
X[6][8] + X[7][8] + X[8][8] + X[8][7] + X[8][6] == 25,
cd_sub(1, X[7][1], X[7][2]),
X[7][4] * X[8][4] * X[8][3] * X[8][5] == 378,
X[7][6] * X[7][7] == 3,
]
def solveCalcudoku(puzzle, n):
X = [[Int("x_%s_%s" % (i+1, j+1)) for j in range(n)] for i in range(n)]
# each cell contains a value in {1, ..., 9}
cells_c = [And(1 <= X[i][j], X[i][j] <= n) for i in range(n)
for j in range(n)]
# each row contains a digit at most once
rows_c = [Distinct(X[i]) for i in range(n)]
# each column contains a digit at most once
cols_c = [Distinct([X[i][j] for i in range(n)]) for j in range(n)]
calcudoku_c = cells_c + rows_c + cols_c + list(map(And, puzzle(X)))
s = Solver()
s.add(calcudoku_c)
if s.check() == sat:
m = s.model()
print("Here is the solution")
print_grid(m, X, n, n)
else:
print("Failed to solve the puzzle")
solveCalcudoku(hardest_calcudoku, 9)
Here is the solution
9 2 7 3 5 1 4 6 8
2 9 3 6 4 7 5 8 1
1 7 8 5 2 3 9 4 6
6 1 9 4 8 5 2 7 3
7 8 2 1 9 6 3 5 4
3 4 6 7 1 9 8 2 5
5 3 1 8 6 4 7 9 2
4 6 5 2 7 8 1 3 9
8 5 4 9 3 2 6 1 7