Simple sudoku solver using z3

sudoku.py

# -*- coding: utf-8 -*-

# Tested on z3 4.4.0, Python 2.7.9
#
# $ time python sudoku.py
# 5 3 4 6 7 8 9 1 2
# 6 7 2 1 9 5 3 4 8
# 1 9 8 3 4 2 5 6 7
# 8 5 9 7 6 1 4 2 3
# 4 2 6 8 5 3 7 9 1
# 7 1 3 9 2 4 8 5 6
# 9 6 1 5 3 7 2 8 4
# 2 8 7 4 1 9 6 3 5
# 3 4 5 2 8 6 1 7 9
# python sudoku.py  0.18s user 0.03s system 96% cpu 0.222 total


import z3
import math


var = []
var_as_map = {}

sol = z3.Solver()

for x in range(9):
    for y in range(9):
        v = z3.BitVec('v_%d' % (x*9+y), 9)
        sol.add(v & (v-1) == 0)

        var.append(v)
        var_as_map[x, y] = v

for i in range(9):
    sol.add(reduce(lambda a, b: a | b,
        [var_as_map[i, y] for y in range(9)]) == 0b111111111)
    sol.add(reduce(lambda a, b: a | b,
        [var_as_map[x, i] for x in range(9)]) == 0b111111111)

for x in range(3):
    for y in range(3):
        # print [(x*3+(i//3), y*3+(i%3)) for i in range(9)]
        sol.add(reduce(lambda a, b: a | b,
            [var_as_map[x*3+(i//3), y*3+(i%3)] for i in range(9)]) == 0b111111111)


def preinit(x, y, value):
    sol.add(var_as_map[x, y] == 2 ** (value - 1))

sample = [
    5, 3, 0, 0, 7, 0, 0, 0, 0,
    6, 0, 0, 1, 9, 5, 0, 0, 0,
    0, 9, 8, 0, 0, 0, 0, 6, 0,
    8, 0, 0, 0, 6, 0, 0, 0, 3,
    4, 0, 0, 8, 0, 3, 0, 0, 1,
    7, 0, 0, 0, 2, 0, 0, 0, 6,
    0, 6, 0, 0, 0, 0, 2, 8, 0,
    0, 0, 0, 4, 1, 9, 0, 0, 5,
    0, 0, 0, 0, 8, 0, 0, 7, 9
]

for idx, val in enumerate(sample):
    if val != 0:
        preinit(idx // 9, idx % 9, val)

if sol.check() == z3.sat:
    model = sol.model()

    for x in range(9):
        line = []
        for y in range(9):
            v = int(str(model[var_as_map[x, y]]))
            line.append(str(int(math.log(v, 2)) + 1))

        print (' '.join(line))

reduce is missing, to be found in functools