問題
3×3のブロックに区切られた 9×9の正方形の枠内に1〜9までの数字を入れる。 (Wikipedia:数独)
回答
example_sudoku.py
from z3 import *
problem = [
[0, 0, 0, 0, 0, 0, 0, 0, 0],
[0, 4, 3, 0, 0, 0, 6, 7, 0],
[5, 0, 0, 4, 0, 2, 0, 0, 8],
[8, 0, 0, 0, 6, 0, 0, 0, 1],
[2, 0, 0, 0, 0, 0, 0, 0, 5],
[0, 5, 0, 0, 0, 0, 0, 4, 0],
[0, 0, 6, 0, 0, 0, 7, 0, 0],
[0, 0, 0, 5, 0, 1, 0, 0, 0],
[0, 0, 0, 0, 8, 0, 0, 0, 0]
]
X = [[Int("x_%s_%s" % (i, j))for j in range(9)] for i in range(9)]
s = Solver()
s.add([And(1 <= X[i][j], X[i][j] <= 9) for i in range(9) for j in range(9)])
for i in range(9):
for j in range(9):
if problem[i][j] != 0:
s.add(X[i][j] == problem[i][j])
s.add([Distinct([X[i][j] for i in range(9)]) for j in range(9)])
s.add([Distinct([X[i][j] for j in range(9)]) for i in range(9)])
s.add([Distinct([X[i+3*a][j+3*b] for i in range(3)
for j in range(3)]) for a in range(3) for b in range(3)])
print(s.check())
m = s.model()
for i in range(9):
tmp = []
for j in range(9):
tmp.append(m[X[i][j]])
print(tmp)
出力
sat
[7, 2, 8, 9, 3, 6, 5, 1, 4]
[9, 4, 3, 1, 5, 8, 6, 7, 2]
[5, 6, 1, 4, 7, 2, 9, 3, 8]
[8, 3, 4, 7, 6, 5, 2, 9, 1]
[2, 1, 7, 8, 4, 9, 3, 6, 5]
[6, 5, 9, 2, 1, 3, 8, 4, 7]
[1, 8, 6, 3, 2, 4, 7, 5, 9]
[3, 7, 2, 5, 9, 1, 4, 8, 6]
[4, 9, 5, 6, 8, 7, 1, 2, 3]
解説
縦横３×３の範囲の数字がすべて異なるので、Distinctを使用する。