-
-
Save nickponline/9c91fe65fef5b58ae1b0 to your computer and use it in GitHub Desktop.
# 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("") |
Cool! Thanks for the observation @GregoryMorse, I've updated the gist.
Cool! Thanks for the observation @GregoryMorse, I've updated the gist.
Hi Nick, you forgot to put {} instead of [] for a set instead of a list to do the elimination.
Here is a better fix to get down to 3240 constraints:
37: cnf = cnf + exactly_one([ transform(i, j, s) for j in xrange(N) ])
38: cnf = cnf + exactly_one([ transform(j, i, s) for j in xrange(N) ])
48: cnf = cnf + exactly_one(v)
just change them from exactly_one(…) to [] e.g.
cnf = cnf + [[ transform(i, j, s) for j in xrange(N) ]]
cnf = cnf + [[ transform(j, i, s) for j in xrange(N) ]]
cnf = cnf + [v]
Now you don't need any sets and frozensets and should have 3240 minimized constraints and it will work faster and more efficiently. exactly_one is only needed for preventing duplicate cell values. Since the rest are inclusive restraints - they are not redundant. Not sure if even further conditions can be eliminated.
Ah was using Python 2 at that point, updated to Python 3.
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.
Its also highly questionable that:
exclusive - must not have 2 values in any cell
81 * (2 choose 9)=2916 or n^2*n(n-1)/2
conditions are necessary. As the not having more than 2 values would break the other constraints on not having the same value in cells which see each other. I have already tested and it works fine without this constraint. It only needs to know that some value 1-9 is there the inclusive rule. Which excludes 2916 rules and really reduces this dramatically to a smaller amount of boolean constraints.
In fact it is even better. You can use the 2916 rules to avoid duplicates -OR- you can exclude based on the pairs of cells which is 7290 constraints.
So in fact eliminating the 7290 constraints since the inclusive constraints already imply them is possible. The minimum constraints is thus:
10530-7290=3240 constraints.