Lorin Hochstein

Ramblings about software, research and other things

“Who owns the fish” in Alloy

with one comment

Hacker News linked to a logic puzzle with the following constraints:

There are five houses in five different colors starting from left to right. In each house lives a person of a different nationality. These owners all drink a certain type of beverage, smoke a certain brand of cigarette and keep a certain type of pet. No two owners have the same pet, smoke the same brand 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’s owner drinks coffee
  6. The person who smokes Pall Mall 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 person who smokes Marlboro lives next to the one who keeps cats
  11. The person who keeps horses lives next to the person who smokes Dunhill
  12. The person who smokes Winfield drinks beer
  13. The German smokes Rothmans
  14. The Norwegian lives next to the blue house
  15. The person who smokes Marlboro has a neighbor who drinks water

Alloy is very well-suited to solving this type of problem, so I gave it a go. Here’s what my Alloy model looks like:

open util/ordering[House]

sig House {
 color: one Color
}

abstract sig Person {
 occupies: one House,
 drinks: one Beverage,
 smokes: one Cigarette,
 keeps: one Pet
}
one sig Brit, Swede, Dane, Norwegian, German extends Person {}

abstract sig Color {}
one sig White, Yellow, Blue, Red, Green extends Color {}

abstract sig Beverage {}
one sig Tea, Coffee, Milk, Beer, Water extends Beverage {}

abstract sig Pet {}
one sig Birds, Cats, Dogs, Horses, Fish extends Pet {}

abstract sig Cigarette {}
one sig PallMall, Dunhill, Marlboro, Winfield, Rothmans extends Cigarette {}

fact allRelationsAreOneToOne {
 color.~color in iden
 occupies.~occupies in iden
 drinks.~drinks in iden
 smokes.~smokes in iden
 keeps.~keeps in iden
}

pred problemConstraints {

 // The Brit lives in the red house
 Red in Brit.occupies.color

 //The Swede keeps dogs as pets
 Dogs in Swede.keeps

 // The Dane drinks tea
 Tea in Dane.drinks

 // The green house is on the left of the white house
 Green in prev[color.White].color

 // The green house's owner drinks coffee
 Coffee in (occupies.(color.Green)).drinks

 // The person who smokes Pall Mall rears birds
 Birds in (smokes.PallMall).keeps

 // The owner of the yellow house smokes Dunhill
 Dunhill in (occupies.(color.Yellow)).smokes

 // The man living in the centre house drinks milk
 (drinks.Milk).occupies in first[].next.next

 // The Norwegian lives in the first house
 Norwegian in occupies.first[]

 // The person who smokes Marlboro lives next to the one who keeps cats
 (smokes.Marlboro).occupies in (keeps.Cats).occupies.(next + prev)

 // The person who keeps horses lives next to the person who smokes Dunhill
 (keeps.Horses).occupies in (smokes.Dunhill).occupies.(next + prev)

 // The person who smokes Winfield drinks beer
 Beer in (smokes.Winfield).drinks

 // The German smokes Rothmans
 German in smokes.Rothmans

 // The Norwegian lives next to the blue house
 Blue in Norwegian.occupies.(next+prev).color

 // The person who smokes Marlboro has a neigbor who drinks water
 (drinks.Water).occupies in (smokes.Marlboro).occupies.(next+prev)

}

run problemConstraints for exactly 5 House

Alloy’s “Magic Layout” did a surprisingly good job at displaying the results. I had to manually rearrange the output so the houses would be displayed in the correct order, but otherwise no fiddling was required. Here’s what it looks like:

alloy-fish

I also put it up on Github.

Advertisements

Written by Lorin

May 12, 2014 at 8:53 pm

Posted in software

One Response

Subscribe to comments with RSS.

  1. […] that are amenable to model checking. A few weeks ago in this blog, I wrote about solving a logic puzzle with Alloy. Today’s post is about solving a different logic puzzle. I found this one from the Alloy […]


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: