Skip to content

Instantly share code, notes, and snippets.

@nickponline

nickponline/sat-solver.py Secret

Last active Dec 20, 2020
Embed
What would you like to do?
# Author: Nicholas Pilkington, 2015
# License: MIT
# 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("")
@ganeshutah

This comment has been minimized.

Copy link

@ganeshutah ganeshutah commented Jul 5, 2018

This is one of the neatest Sudoku codes I've seen - kudos!

@gengyu89

This comment has been minimized.

Copy link

@gengyu89 gengyu89 commented May 19, 2020

How did you obtain the number 11988 in the write up?

@GregoryMorse

This comment has been minimized.

Copy link

@GregoryMorse GregoryMorse commented Jun 13, 2020

How did you obtain the number 11988 in the write up?

should be len(cnf) at line 49...

@nickponline

This comment has been minimized.

Copy link
Owner Author

@nickponline nickponline commented Jun 14, 2020

Thanks

@GregoryMorse @gengyu89 yes that's correct.

@GregoryMorse

This comment has been minimized.

Copy link

@GregoryMorse GregoryMorse commented Jun 24, 2020

11988=9x9x37 (1 + (9)x(9-1)/2) x 4 (4 because 1 value per row, 1 value per row, 1 value per cell, 1 value per house) so this formula can be straightforwardly derived.
(1 + (9)x(9-1)/2) comes from 1 constraint and 1+2+3+4+5+6+7+8 exclusionary constraints.

@GregoryMorse

This comment has been minimized.

Copy link

@GregoryMorse GregoryMorse commented Jun 24, 2020

So the formula for any classic sudoku is: n*n*(1+n*(n-1)/2)*4 and this equals 2n^4-2n^3+4n^2

@GregoryMorse

This comment has been minimized.

Copy link

@GregoryMorse GregoryMorse commented Jun 24, 2020

It seems this can be reduced by considering that rows/houses and column/houses already 3x1 or 1x3 intersections, thus the constraints can be relaxed in terms of the house constraints. This would reduce the number of constraints enough to be worth optimizing...

@GregoryMorse

This comment has been minimized.

Copy link

@GregoryMorse GregoryMorse commented Jun 24, 2020

This can be fixed by making CNF a set of frozensets probably most simply or some additional logic when dealing with the house constraints. It can be converted back to a list of lists before SAT solving if the SAT solver wont accept sets/frozensets. Each cell sees not 24 (8x3) other cells but it in fact sees 8+8+4=20 other cells... Actually its worse than that without using sets/frozensets - the inclusive groupings are all constantly repeated when only 27x9 of them are needed, there are a very high number of duplicated unnecessary constraints. The actual number of constraints is much lower...

@GregoryMorse

This comment has been minimized.

Copy link

@GregoryMorse GregoryMorse commented Jun 24, 2020

Injected at line 49:

    print(len(cnf))
    print(len({frozenset(x) for x in cnf}))
11988
10530

So there are a lot of duplicated constraints in here and makes the formula above a worst case not an optimal one - there is cell visibility reflexivity as well to take into account. The minimum number of inclusive and negation constraints should be computable though.

I can confirm 10530 is the correct number and it can be mathematically proven:
inclusive - must have each value in each mutally exclusive region 27*9=243 or 3n^2
inclusive - must have a value of 1-9 in each cell 81 or n^2
exclusive - must not have 2 values in any cell 81 * (2 choose 9)=2916 or n^2*n(n-1)/2
exclusive - pairs of cells which see each other 81*(9-1+9-1+9+1-sqrt(9)-sqrt(9))/2*9=7290 or n^2*(n-1+n-1+n+1-sqrt(n)-sqrt(n))/2*n

so we have: 3n^2+n^2+n^2*n(n-1)/2+n^2*(n-1+n-1+n+1-sqrt(n)-sqrt(n))/2*n
which simplifies to 2n^4-n^3+4n^2-n^(7/2)

indeed 9^(7/2) is 2187 and 9^3=729 and 11988-2187+729=10530.

So 2187-729=1458 extraneous constraints are in the current solution and is not ideal. I hope this proof suffices.

@GregoryMorse

This comment has been minimized.

Copy link

@GregoryMorse GregoryMorse commented Jun 24, 2020

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.

@nickponline

This comment has been minimized.

Copy link
Owner Author

@nickponline nickponline commented Jun 24, 2020

Cool! Thanks for the observation @GregoryMorse, I've updated the gist.

@GregoryMorse

This comment has been minimized.

Copy link

@GregoryMorse GregoryMorse commented Jun 24, 2020

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.

@nickponline

This comment has been minimized.

Copy link
Owner Author

@nickponline nickponline commented Jun 24, 2020

Ah was using Python 2 at that point, updated to Python 3.

@GregoryMorse

This comment has been minimized.

Copy link

@GregoryMorse GregoryMorse commented Jun 24, 2020

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