zebra puzzle; z3 based solution.

zebra.py

#zebra puzzle.
#
#There are five houses.
#The Englishman lives in the red house.
#The Spaniard owns the dog.
#Coffee is drunk in the green house.
#The Ukrainian drinks tea.
#The green house is immediately to the right of the ivory house.
#The Old Gold smoker owns snails.
#Kools are smoked in the yellow house.
#Milk is drunk in the middle house.
#The Norwegian lives in the first house.
#The man who smokes Chesterfields lives in the house next to the man with the fox.
#Kools are smoked in the house next to the house where the horse is kept.
#The Lucky Strike smoker drinks orange juice.
#The Japanese smokes Parliaments.
#The Norwegian lives next to the blue house.

# Who drinks water? Who owns the Zebra?

from z3 import (Distinct, And, Or, Solver, Int, sat)

# Each name in each of the lists below corresponds to a house number (between 1 and 5).
nationalities = "englishman japanese ukrainian norwegian spaniard".split()
pets = "dog snails horse fox zebra".split()
drinks = "coffee  milk  oj  tea  water".split()
colors = "blue red yellow green ivory".split()
smokes = "oldgolds kools parliaments chesterfields luckystrikes".split()

s = Solver()

# For each var, create a z3 Int (valued 1 to 5), and also create a
# global variable of that name to help specify constraints easily.
for v in (nationalities + pets + drinks + colors + smokes):
    z = Int(v)
    s.add(And(z >= 1, z <= 5))
    globals()[v] = z  # naughty. 

s.add(Distinct(englishman,japanese,ukrainian,norwegian,spaniard))
s.add(Distinct(dog,snails,horse,fox,zebra))
s.add(Distinct(coffee,milk,oj,tea, water))
s.add(Distinct(blue,red,yellow,green,ivory))
s.add(Distinct(oldgolds,kools,parliaments,chesterfields,luckystrikes))

# The Englishman lives in the red house.
# Interpreted as "the house number of the englishman is the smae as that of the red house"
# The Distinct expressions above ensure that no two nationalities own the same pet, or
# live in the same colored house etc.
s.add(englishman == red) 

#The Spaniard owns the dog. 
s.add(spaniard == dog)

#Coffee is drunk in the green house.
s.add(coffee == green)

#The Ukrainian drinks tea.
s.add(ukrainian == tea)

#The green house is immediately to the right of the ivory house.
s.add(green == ivory + 1)

#The Old Gold smoker owns snails.
s.add(oldgolds == snails)

#Kools are smoked in the yellow house.
s.add(kools == yellow)

#Milk is drunk in the middle house.
s.add(milk == 3)

#The Norwegian lives in the first house.
s.add(norwegian == 1)

#The man who smokes Chesterfields lives in the house next to the man with the fox.
s.add(Or(chesterfields == fox - 1, chesterfields == fox + 1))

#Kools are smoked in the house next to the house where the horse is kept.
s.add(Or(kools == horse + 1, kools == horse - 1))

#The Lucky Strike smoker drinks orange juice.
s.add(luckystrikes == oj)

#The Japanese smokes Parliaments.
s.add(japanese == parliaments)

#The Norwegian lives next to the blue house.
s.add(Or(norwegian == blue + 1, norwegian == blue - 1))

def houseNum(m, var): # value of the z3 int with name given by 'var', in the model 'm'
    return m.eval(Int(var)).as_long()
    
if s.check() == sat:
    m = s.model()
    fmt = "%-13s " * 5
    print fmt%tuple(range(1,6))

    for lst in (nationalities, colors, pets, drinks, smokes):
        # sort list by house numbers
        lst.sort(key=lambda v: houseNum(m,v))
        print fmt%tuple(lst)
else:
    print "No solution found"