## The Situation

- There are \(5\) houses in five different colours.
- In each house lives a person with a different nationality.
- These five owners drink a certain type of beverage, smoke a certain brand of cigar and keep a certain pet.
- 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

- The Brit lives in the red house.
- The swede keeps dogs as pets.
- The dane drinks tea.
- The green house is on the left of the white house.
- The green house owner drinks coffee.
- The person who smokes pallmall rears birds.
- The owner of the yellow house smokes dunhill.
- The man living in the centre house drinks milk.
- The Norwegian lives in the first house.
- The man who smokes blends lives next to the one who keeps cats.
- The man who keeps horses lives next to the man who smokes dunhill.
- The owner who smokes bluemaster drinks beer.
- The German smokes prince.
- The Norwegian lives next to the blue house.
- 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 *
= [0,1,2,3,4,5]
house, nat, col, pet, cig, bev = {0:"House1", 1:"House2", 2:"House3", 3:"House4", 4:"House5"}
houses
= [0,1,2,3,4]
red, blue, green, yellow, white = {red:"Red", blue: "Blue", green:"Green", yellow:"Yellow", white:"White"}
colours
= [0,1,2,3,4]
brit, swede, dane, german, norwegian = {brit:"Brit", swede:"Swede", dane:"Dane", german:"German", norwegian:"Norw"}
nationality
= [0,1,2,3,4]
fish, cat, bird, dog, horse = {fish:"Fish", cat:"Cat", bird:"Bird", dog:"Dog", horse:"Horse"}
pets
= [0,1,2,3,4]
pallmall, dunhill, bluemaster, blends, prince = {pallmall:"Pallmall", dunhill:"Dunhill", bluemaster:"Bluemaster", blends:"Blends", prince:"Prince"}
cigars
= [0,1,2,3,4]
milk, tea, coffee, beer, water = {milk:"Milk", tea:"Tea", coffee:"Coffee", beer:"Beer", water:"Water"}
bevs
= {house:houses, nat:nationality, col:colours, pet:pets, cig:cigars, bev:bevs}
columns
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
= [Distinct([self.X[i][j] for i in range(5)]) for j in range(6)]
cols_c
cons.append(And(cols_c))
# The brit lives in the red house
= Or([And(self.X[i][nat] == brit, self.X[i][col] == red)
cons1 for i in range(5)])
cons.append(cons1)
# The swede keeps dogs as pets
= Or([And(self.X[i][nat] == swede, self.X[i][pet] == dog)
cons2 for i in range(5)])
cons.append(cons2)
# The dane drinks tea
= Or([And(self.X[i][nat] == dane, self.X[i][bev] == tea)
cons3 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):
self.X[i][col] == green, self.X[j][col] == white))
cons4.append(And(= Or(cons4)
cons4
cons.append(cons4)
# The green house owner drinks coffee
= Or([And(self.X[i][col] == green, self.X[i][bev] == coffee)
cons5 for i in range(5)])
cons.append(cons5)
# The person who smokes pallmall rears birds
= Or([And(self.X[i][cig] == pallmall, self.X[i][pet] == bird)
cons6 for i in range(5)])
cons.append(cons6)
# The owner of the yellow house smokes dunhill
= Or([And(self.X[i][col] == yellow, self.X[i][cig] == dunhill)
cons7 for i in range(5)])
cons.append(cons7)
# The man living in the centre house drinks milk
= Or([And(self.X[i][house] == 2, self.X[i][bev] == milk)
cons8 for i in range(5)])
cons.append(cons8)
# The Norwegian lives in the first house
= Or([And(self.X[i][nat] == norwegian, self.X[i][house] == 0)
cons9 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:
self.X[i][cig] == blends, self.X[j][pet] == cat,
cons10.append(And(self.X[i][house]-self.X[j][house]) == 1))
Abs(= Or(cons10)
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:
self.X[i][pet] == horse, self.X[j][cig] == dunhill,
cons11.append(And(self.X[i][house]-self.X[j][house]) == 1))
Abs(= Or(cons11)
cons11
cons.append(cons11)
# The owner who smokes bluemaster drinks beer
= Or([And(self.X[i][cig] == bluemaster,self.X[i][bev] == beer)
cons12 for i in range(5)])
cons.append(cons12)
# The german smokes prince
= Or([And(self.X[i][nat] == german, self.X[i][cig] == prince)
cons13 for i in range(5)])
cons.append(cons13)
# The Norwegian lives next to the blue house
= Or([And(self.X[i][house] == 1, self.X[i][col] == blue)
cons14 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:
self.X[i][cig] == blends, self.X[j][bev] == water,
cons15.append(And(self.X[i][house]-self.X[j][house]) == 1))
Abs(= Or(cons15)
cons15
cons.append(cons15)
self.s.add(And(cons))
def output_solution(self):
= self.s.model()
m 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.")
= AssignmentPuzzleSolver()
s s.solve()
```