-
Notifications
You must be signed in to change notification settings - Fork 0
/
z3_sudoku.py
107 lines (89 loc) · 2.59 KB
/
z3_sudoku.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
from z3 import *
puzzle2 = [
[2, 6, 0, 0, 1, 0, 0, 5, 0],
[8, 0, 0, 0, 6, 0, 4, 0, 0],
[0, 0, 0, 0, 2, 0, 3, 0, 0],
[5, 0, 0, 0, 0, 9, 7, 0, 0],
[0, 0, 7, 0, 0, 8, 0, 3, 0],
[0, 3, 2, 0, 0, 0, 0, 0, 0],
[7, 0, 0, 0, 8, 0, 0, 0, 1],
[6, 0, 0, 0, 0, 4, 5, 0, 0],
[0, 0, 0, 0, 0, 0, 0, 0, 0]
]
puzzle_easy = [[3, 0, 6, 5, 0, 8, 4, 0, 0],
[5, 2, 0, 0, 0, 0, 0, 0, 0],
[0, 8, 7, 0, 0, 0, 0, 3, 1],
[0, 0, 3, 0, 1, 0, 0, 8, 0],
[9, 0, 0, 8, 6, 3, 0, 0, 5],
[0, 5, 0, 0, 9, 0, 6, 0, 0],
[1, 3, 0, 0, 0, 0, 2, 5, 0],
[0, 0, 0, 0, 0, 0, 0, 7, 4],
[0, 0, 5, 2, 0, 6, 3, 0, 0]]
puzzle = [ #grid evil
[0, 0, 8, 0, 0, 5, 0, 0, 3],
[0, 6, 0, 0, 8, 0, 0, 2, 0],
[2, 0, 0, 9, 0, 0, 1, 0, 0],
[3, 0, 0, 8, 0, 0, 7, 0, 0],
[0, 5, 0, 0, 1, 0, 0, 3, 0],
[0, 0, 7, 0, 0, 4, 0, 0, 2],
[0, 0, 4, 0, 0, 7, 0, 0, 6],
[0, 1, 0, 0, 6, 0, 0, 4, 0],
[6, 0, 0, 3, 0, 0, 5, 0, 0]
]
puzzle = [ #grid evil
[0, 0, 8, 0, 0, 5, 0, 0, 3],
[0, 6, 0, 0, 8, 0, 0, 2, 0],
[2, 0, 0, 9, 0, 0, 1, 0, 0],
[3, 0, 0, 8, 0, 0, 7, 0, 0],
[0, 5, 0, 0, 1, 0, 0, 3, 0],
[0, 0, 7, 0, 0, 4, 0, 0, 2],
[0, 0, 4, 0, 0, 7, 0, 0, 6],
[0, 1, 0, 0, 6, 0, 0, 4, 0],
[6, 0, 0, 3, 0, 0, 5, 0, 0]
]
def print_grid(grid, model=None):
for r in range(9):
if r % 3 == 0 and r != 0:
print('-'*21)
row = ''
for c in range(9):
if c % 3 == 0 and c != 0:
row += '| '
value = model.evaluate(grid[r][c]) if model else grid[r][c]
row += f'{value} '
print(row)
def add_puzzle_constraints(solver, grid, puzzle):
for r in range(9):
for c in range(9):
if puzzle[r][c] != 0:
solver.add(grid[r][c] == puzzle[r][c])
#create a solver instance
s = Solver()
grid = [
[ Int(f'cell-{i}-{j}') for j in range(9) ]
for i in range(9)
]
#each cell contains a value in {1, ..., 9}
for r in range(9):
for c in range(9):
cell = grid[r][c]
s.add(1 <= cell, cell <= 9)
#each row contains a digit at most once
for r in range(9):
s.add(Distinct(grid[r]))
#each column contains a digit at most once
for c in range(9):
s.add(Distinct([grid[r][c] for r in range(9)]))
#each 3x3 square contains a digit at most once
for r in range(0, 9, 3):
for c in range(0, 9, 3):
s.add(Distinct([
grid[r + i][c + j]
for i in range(3) for j in range(3)
]))
add_puzzle_constraints(s, grid, puzzle)
if s.check() == sat:
m = s.model()
print_grid(grid, m)
else:
print("The puzzle cannot be solved.")