Created
May 20, 2020 10:56
-
-
Save sielicki/fd86d68733133f654128519b3c4e12c2 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/usr/bin/env python3 | |
| import z3 | |
| import pprint | |
| # 9x9 matrix of integer variables | |
| X = [ [ z3.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 = [ z3.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 = [ z3.Distinct(X[i]) for i in range(9) ] | |
| # each column contains a digit at most once | |
| cols_c = [ z3.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 = [ z3.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 | |
| #### additional for "miracle" sudoku | |
| ortho_adjacent = [] | |
| for i in range(9): | |
| for j in range(9): | |
| if j+1 < 9: | |
| ortho_adjacent.append(z3.And(X[i][j] != X[i][j+1] + 1)) | |
| if i+1 < 9: | |
| ortho_adjacent.append(z3.And(X[i][j] != X[i+1][j] + 1)) | |
| if j-1 >= 0: | |
| ortho_adjacent.append(z3.And(X[i][j] != X[i][j-1] + 1)) | |
| if i-1 >= 0: | |
| ortho_adjacent.append(z3.And(X[i][j] != X[i-1][j] + 1)) | |
| knights = [] | |
| for i in range(9): | |
| for j in range(9): | |
| if j+2 < 9: | |
| if i+1 < 9: | |
| knights.append(z3.And(X[i][j] != X[i+1][j+2])) | |
| if i-1 >= 0: | |
| knights.append(z3.And(X[i][j] != X[i-1][j+2])) | |
| if j-2 >= 0: | |
| if i+1 < 9: | |
| knights.append(z3.And(X[i][j] != X[i+1][j-2])) | |
| if i-1 >= 0: | |
| knights.append(z3.And(X[i][j] != X[i-1][j-2])) | |
| if i+2 < 9: | |
| if j+1 < 9: | |
| knights.append(z3.And(X[i][j] != X[i+2][j+1])) | |
| if j-1 >= 0: | |
| knights.append(z3.And(X[i][j] != X[i+2][j-1])) | |
| if i-2 >= 0: | |
| if j+1 < 9: | |
| knights.append(z3.And(X[i][j] != X[i-2][j+1])) | |
| if j-1 >= 0: | |
| knights.append(z3.And(X[i][j] != X[i-2][j-1])) | |
| kings = [] | |
| for i in range(9): | |
| for j in range(9): | |
| if i-1 >= 0: | |
| kings.append(z3.And(X[i][j] != X[i-1][j])) | |
| if i+1 < 9: | |
| kings.append(z3.And(X[i][j] != X[i+1][j])) | |
| if j-1 >= 0: | |
| kings.append(z3.And(X[i][j] != X[i][j-1])) | |
| if j+1 < 9: | |
| kings.append(z3.And(X[i][j] != X[i][j+1])) | |
| if i-1 >= 0 and j-1 >= 0: | |
| kings.append(z3.And(X[i][j] != X[i-1][j-1])) | |
| if i-1 >= 0 and j+1 < 9: | |
| kings.append(z3.And(X[i][j] != X[i-1][j+1])) | |
| if i+1 < 9 and j-1 >= 0: | |
| kings.append(z3.And(X[i][j] != X[i+1][j-1])) | |
| if i+1 < 9 and j+1 < 9: | |
| kings.append(z3.And(X[i][j] != X[i+1][j+1])) | |
| sudoku_c += knights | |
| sudoku_c += ortho_adjacent | |
| sudoku_c += kings | |
| #### | |
| # sudoku instance, we use '0' for empty cells | |
| instance = ((0,0,0,0,0,0,0,0,0), | |
| (0,0,0,0,0,0,0,0,0), | |
| (0,0,0,0,0,0,0,0,0), | |
| (0,0,0,0,0,0,0,0,0), | |
| (0,0,1,0,0,0,0,0,0), | |
| (0,0,0,0,0,0,2,0,0), | |
| (0,0,0,0,0,0,0,0,0), | |
| (0,0,0,0,0,0,0,0,0), | |
| (0,0,0,0,0,0,0,0,0)) | |
| instance_c = [ z3.If(instance[i][j] == 0, | |
| True, | |
| X[i][j] == instance[i][j]) | |
| for i in range(9) for j in range(9) ] | |
| s = z3.Solver() | |
| s.add(sudoku_c + instance_c) | |
| if s.check() == z3.sat: | |
| m = s.model() | |
| r = [ [ m.evaluate(X[i][j]) for j in range(9) ] | |
| for i in range(9) ] | |
| pprint.pprint(r) | |
| else: | |
| print("failed to solve") |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment