Last active
December 6, 2023 18:47
-
-
Save nickponline/9c91fe65fef5b58ae1b0 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
# Author: Nicholas Pilkington, 2015 | |
# Blog Post: https://nickp.svbtle.com/sudoku-satsolver | |
import pycosat | |
N = 9 | |
M = 3 | |
def exactly_one(variables): | |
cnf = [ variables ] | |
n = len(variables) | |
for i in range(n): | |
for j in range(i+1, n): | |
v1 = variables[i] | |
v2 = variables[j] | |
cnf.append([-v1, -v2]) | |
return cnf | |
def transform(i, j, k): | |
return i*N*N + j*N + k + 1 | |
def inverse_transform(v): | |
v, k = divmod(v-1, N) | |
v, j = divmod(v, N) | |
v, i = divmod(v, N) | |
return i, j, k | |
if __name__ == '__main__': | |
cnf = [] | |
# Cell, row and column constraints | |
for i in range(N): | |
for s in range(N): | |
cnf = cnf + exactly_one([ transform(i, j, s) for j in range(N) ]) | |
cnf = cnf + exactly_one([ transform(j, i, s) for j in range(N) ]) | |
for j in range(N): | |
cnf = cnf + exactly_one([ transform(i, j, k) for k in range(N) ]) | |
# Sub-matrix constraints | |
for k in range(N): | |
for x in range(M): | |
for y in range(M): | |
v = [ transform(y*M + i, x*M + j, k) for i in range(M) for j in range(M)] | |
cnf = cnf + exactly_one(v) | |
# See contribution from @GregoryMorse below | |
cnf = { frozenset(x) for x in cnf } | |
cnf = list(cnf) | |
# A 16-constraint Sudoku | |
constraints = [ | |
(0, 3, 7), | |
(1, 0, 1), | |
(2, 3, 4), | |
(2, 4, 3), | |
(2, 6, 2), | |
(3, 8, 6), | |
(4, 3, 5), | |
(4, 5, 9), | |
(5, 6, 4), | |
(5, 7, 1), | |
(5, 8, 8), | |
(6, 4, 8), | |
(6, 5, 1), | |
(7, 2, 2), | |
(7, 7, 5), | |
(8, 1, 4), | |
(8, 6, 3), | |
] | |
cnf = cnf + [[transform(z[0], z[1], z[2])-1] for z in constraints] | |
for solution in pycosat.itersolve(cnf): | |
X = [ inverse_transform(v) for v in solution if v > 0] | |
for i, cell in enumerate(sorted(X, key=lambda h: h[0] * N*N + h[1] * N)): | |
print(cell[2]+1, end=" ") | |
if (i+1) % N == 0: print("") |
I think Python 2 used the set([…]) notation maybe did not have the {} shorthand syntax which can be a dictionary if empty, or a set if individual values instead of key:value values.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Ah was using Python 2 at that point, updated to Python 3.