Solve n-queens with pycosat.

n_queens.py

# Solve n-queens problem with picosat
import pycosat
import numpy
import itertools

def get_cnf(N):
    cnf = []

    # * convert to object because pycosat expects 'int's
    # * add 1 because 0 is reserved in pycosat
    vars = (numpy.arange(N*N).reshape(N, N) + 1).astype('object')

    # At least one queen per row
    cnf += vars.tolist()

    # At most one queen per row and column
    for i in xrange(N):
        cnf += itertools.combinations(-vars[i,:], 2)
        cnf += itertools.combinations(-vars.T[i,:], 2)

    # At most one queen per diagonal
    for i in xrange(-N, N):
        cnf += itertools.combinations(-vars.diagonal(i), 2)
        cnf += itertools.combinations(-vars[:,::-1].diagonal(i), 2)

    # pycosat wants a list of lists (tuples won't work)
    return [list(x) for x in cnf]


# Compare to wikipedia output http://en.wikipedia.org/wiki/Eight_queens_puzzle
n_solutions = [len(list(pycosat.itersolve(get_cnf(i)))) for i in xrange(1, 10)]
assert n_solutions == [1, 0, 0, 2, 10, 4, 40, 92, 352]