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