sat-solver.py

# 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.