run: "python sudoku.py problem.sud"

problem.sud

.27.3....
1......7.
.83.7.24.
.71..5...
.3.....8.
...9..12.
.15.2.49.
.4......8
....1.56.

sudoku.py

import sys
from z3 import *

# Create solver
s = Solver()

# Create Z3 integer variables for matrix cells
cells = [[Int("z_%s_%s" % (i+1, j+1)) for j in range(9) ] for i in range(9) ]

# Cell constraints
for y in range(9):
    for x in range(9):
        s.add(1 <= cells[x][y])
	s.add(cells[x][y] <= 9)

# Column constraints
for x in range(9):
    s.add(Distinct(cells[x]))

# Row constraints
for y in range(9):
    s.add(Distinct([cells[x][y] for x in range(9)]))

# Group constraints
for x in range(3):
    for y in range(3):
	s.add(Distinct([cells[3*x+i][3*y+j] for i in range(3) for j in range(3)]))

# Parse sudoku problem instance and add more constraints
for y, line in enumerate(open(sys.argv[1], "rU").read().split("\n")):
    for x, value in enumerate(line):
        if value != ".":
            s.add(cells[x][y] == value)

# Check if constraints have been satisfied
if s.check() == sat:
    m = s.model()
    for y in range(9):
        print "".join([str(m.evaluate(cells[x][y])) for x in range(9) ])
else:
    print "No solution."