# Who owns the fish?

Using the fantastic Z3 for fun.
Z3
puzzles
Published

April 9, 2021

## The Situation

1. There are $$5$$ houses in five different colours.
2. In each house lives a person with a different nationality.
3. These five owners drink a certain type of beverage, smoke a certain brand of cigar and keep a certain pet.
4. No owners have the same pet, smoke the same brand of cigar or drink the same beverage.

The question is who owns the fish?

### Hints

1. The Brit lives in the red house.
2. The swede keeps dogs as pets.
3. The dane drinks tea.
4. The green house is on the left of the white house.
5. The green house owner drinks coffee.
6. The person who smokes pallmall rears birds.
7. The owner of the yellow house smokes dunhill.
8. The man living in the centre house drinks milk.
9. The Norwegian lives in the first house.
10. The man who smokes blends lives next to the one who keeps cats.
11. The man who keeps horses lives next to the man who smokes dunhill.
12. The owner who smokes bluemaster drinks beer.
13. The German smokes prince.
14. The Norwegian lives next to the blue house.
15. The man who smokes blends has a neighbour who drinks water.

## Computational Solution

The German owns the fish. Here is a possible assignment satisfying all the constraints:

House Nationality Colour Pets Cigars Beverages
1 Norweigan Green Bird Pallmall Coffee
2 German Blue Fish Prince Water
3 Brit Red Horse Blends Milk
4 Dane Yellow Cat Dunhill Tea
5 Swede White Dog Bluemaster Beer
from z3 import *

house, nat, col, pet, cig, bev = [0,1,2,3,4,5]
houses = {0:"House1", 1:"House2", 2:"House3", 3:"House4", 4:"House5"}

red, blue, green, yellow, white = [0,1,2,3,4]
colours = {red:"Red", blue: "Blue", green:"Green", yellow:"Yellow", white:"White"}

brit, swede, dane, german, norwegian = [0,1,2,3,4]
nationality = {brit:"Brit", swede:"Swede", dane:"Dane", german:"German", norwegian:"Norw"}

fish, cat, bird, dog, horse = [0,1,2,3,4]
pets = {fish:"Fish", cat:"Cat", bird:"Bird", dog:"Dog", horse:"Horse"}

pallmall, dunhill, bluemaster, blends, prince = [0,1,2,3,4]
cigars = {pallmall:"Pallmall", dunhill:"Dunhill", bluemaster:"Bluemaster", blends:"Blends", prince:"Prince"}

milk, tea, coffee, beer, water = [0,1,2,3,4]
bevs = {milk:"Milk", tea:"Tea", coffee:"Coffee", beer:"Beer", water:"Water"}

columns = {house:houses, nat:nationality, col:colours, pet:pets, cig:cigars, bev:bevs}

def Abs(x):
return If(x >=0, x, -x)

class AssignmentPuzzleSolver:
def __init__(self):
self.X = [[Int("x_%s_%s" % (i, j)) for j in range(6)]
for i in range(5)]
self.s = Solver()
self.s.add([And(0 <= self.X[i][j], self.X[i][j]<= 4)
for i in range(5) for j in range(6)])

def set_constraints(self):
cons = []

# there is no repetition along each dimension
cols_c = [Distinct([self.X[i][j] for i in range(5)]) for j in range(6)]
cons.append(And(cols_c))

# The brit lives in the red house
cons1 = Or([And(self.X[i][nat] == brit, self.X[i][col] == red)
for i in range(5)])
cons.append(cons1)

# The swede keeps dogs as pets
cons2 = Or([And(self.X[i][nat] == swede, self.X[i][pet] == dog)
for i in range(5)])
cons.append(cons2)

# The dane drinks tea
cons3 = Or([And(self.X[i][nat] == dane, self.X[i][bev] == tea)
for i in range(5)])
cons.append(cons3)

# The green house is on the left of the  white house
cons4 = []
for i in range(4):
for j in range(i+1,5):
cons4.append(And(self.X[i][col] == green, self.X[j][col] == white))
cons4 = Or(cons4)
cons.append(cons4)

# The green house owner drinks coffee
cons5 = Or([And(self.X[i][col] == green, self.X[i][bev] == coffee)
for i in range(5)])
cons.append(cons5)

# The person who smokes pallmall rears birds
cons6 = Or([And(self.X[i][cig] == pallmall, self.X[i][pet] == bird)
for i in range(5)])
cons.append(cons6)

# The owner of the yellow house smokes dunhill
cons7 = Or([And(self.X[i][col] == yellow, self.X[i][cig] == dunhill)
for i in range(5)])
cons.append(cons7)

# The man living in the centre house drinks milk
cons8 = Or([And(self.X[i][house] == 2, self.X[i][bev] == milk)
for i in range(5)])
cons.append(cons8)

# The Norwegian lives in the first house
cons9 = Or([And(self.X[i][nat] == norwegian, self.X[i][house] == 0)
for i in range(5)])
cons.append(cons9)

# The man who smokes blends lives next to the one who keeps cats
cons10 = []
for i in range(5):
for j in range(5):
if i != j:
cons10.append(And(self.X[i][cig] == blends, self.X[j][pet] == cat,
Abs(self.X[i][house]-self.X[j][house]) == 1))
cons10 = Or(cons10)
cons.append(cons10)

# The man who keeps horses lives next to the man who smokes dunhill
cons11 = []
for i in range(5):
for j in range(5):
if i != j:
cons11.append(And(self.X[i][pet] == horse, self.X[j][cig] == dunhill,
Abs(self.X[i][house]-self.X[j][house]) == 1))
cons11 = Or(cons11)
cons.append(cons11)

# The owner who smokes bluemaster drinks beer
cons12 = Or([And(self.X[i][cig] == bluemaster,self.X[i][bev] == beer)
for i in range(5)])
cons.append(cons12)

# The german smokes prince
cons13 = Or([And(self.X[i][nat] == german, self.X[i][cig] == prince)
for i in range(5)])
cons.append(cons13)

# The Norwegian lives next to the blue house
cons14 = Or([And(self.X[i][house] == 1, self.X[i][col] == blue)
for i in range(5)])
cons.append(cons14)

# The man who smokes blends has a neighbour who drinks water
cons15 = []
for i in range(5):
for j in range(5):
if i != j:
cons15.append(And(self.X[i][cig] == blends, self.X[j][bev] == water,
Abs(self.X[i][house]-self.X[j][house]) == 1))
cons15 = Or(cons15)
cons.append(cons15)

self.s.add(And(cons))

def output_solution(self):
m = self.s.model()
print("\t".join(["House","Nationality","Colour","Pets","Cigars","Beverages"]))
for i in range(5):
print("\t".join([columns[j][m.evaluate(self.X[i][j]).as_long()] for j in range(6)]))

def solve(self):
self.set_constraints()
if self.s.check() == sat:
self.output_solution()
else:
print(self.s)
print("Failed to solve.")

s = AssignmentPuzzleSolver()
s.solve()
Back to top